Block Encoding

Exercise BE-001

intermediate · concept · test_public

local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.

Assumptions and conventions

U unitary on the stated finite tensor product
alpha>0 is a real scale; epsilon>=0; column-vector convention

Auxiliary register pinned to the all-zero value selects the clean block
Exact case is the epsilon=0 instance of the approximate operator-norm bound

Question

Let U be a unitary on n system qubits and a auxiliary qubits. For a strictly positive real alpha, define B=(<0^a| tensor I)U(|0^a> tensor I). State what it means for U to encode a system operator A exactly or with induced-operator-norm error at most epsilon>=0. Give the matrix dimensions and derive the scalar entry condition equivalent to exact encoding. Explain why division by alpha needs its stated premise.

Hint: mathematical route

Defines the block-encoding projected-block contract: A = alpha*(<0^a| tensor I)U(|0^a> tensor I) exactly, operator-norm epsilon bound approximately, with explicit dimensions.

The candidate's unitary has dimension fixed by system+auxiliary qubits, and the extracted block is the auxiliary-zero submatrix.
The exact contract A = alpha*block is the epsilon=0 case of the stored operator-norm approximation bound.

Reference solution

U has dimension2^(n+a) square. B and A have dimension2^n square. Exact encoding means A=alpha B; approximate encoding means ||A-alpha B||<=epsilon in the induced Euclidean operator norm. Exact equality is equivalent to each clean entry U((0,i),(0,j))=A(i,j)/alpha because alpha>0, hence nonzero. The norm error is zero exactly for equal operators. Positivity is a scale convention, while nonzero is the logical premise needed for division; at alpha=0 the undivided equation reduces to A=0 and does not determine B, so the divided equivalent statement is not defined. The scale is not assumed optimal, and no efficient implementation follows from the existence of U.

Assessment rubric

Correct total and system block dimensions (1 weight)
Exact equality and induced norm error with explicit scale convention (1 weight)
Nonzero alpha required; correct alpha=0 boundary (1 weight)

Graph-grounded prerequisites

These are support/source anchors, not an automatically extracted theorem-dependency proof.

Download the shared core registry

Lean view and evidence boundary

No aligned Lean view has been admitted for this native core in this textbook checkpoint. This is not a claim that the underlying mathematics lacks a formal proof. Contributions must preserve this exact target contract and split.

Read the Lean track and existing diagnostic warmups

Sources and provenance

QuantumBlockEncoding/BlockEncoding.lean
structure OperatorBlockEncodingCandidate (lines 103-116); structure ApproximateOperatorBlockEncodingCandidate with approximationBound comment '||A - alpha * ((<0^a| tensor I) U (|0^a> tensor I))|| <= epsilon' (lines 136-153)
Source SHA-256: fe06f75a29822e28ccdbfedfb0b0e87f90872620fae7aed359085fad8fae64b4 · MIT (repository LICENSE)
QuantumBlockEncoding/CircuitSemantics.lean
def signalSystemBlockProjection with doc 'The block (<signalIdx| tensor I) M (|signalIdx> tensor I)' (lines 741-772)
Source SHA-256: 761ac3a98ea5a82ad5030e280e3810821081d10cec3d0a0a1d3c2add3fcd4666 · MIT (repository LICENSE)

Contract: a3257c6b614b55274079564a7777fe8ae590dfc4af23168d27fb87357c8959e4

Item digest: d3fcc5644825a903d365c5356b4e51c6754683966d400872169b733c2b7ed313

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

Authored support steps: 2. This is not measured graph distance or model difficulty.