Block Encoding
Exercise BE-010
nl bridge from inspected source. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- U,V unitary with unit normalization for simplicity
- Each clean block uses its own auxiliary bra/ket0; column-vector chronological order
- Product applies right factor first (B), then left (A), to the system
- Clean branch requires all-zero ancilla before each factor
Question
Suppose unitaries U and V have clean blocks A and B on the same data space. Explain why applying V then U with DISJOINT auxiliary registers initialized at zero yields clean block AB. Show concretely why simply reusing a single auxiliary register can fail. Is resetting that register or applying its inverse automatically a free coherent repair?
Hint: mathematical route
Disjoint clean auxiliary registers compose blocks by matrix multiplication; X/X refutes naive same-register reuse, and neither reset nor inverse is a free coherent repair.
- Independent clean auxiliary indices leave a data-index product sum AB.
- The X/X same-register witness creates a garbage-return path missed by AB.
- Reset/inverse is not an automatically valid coherent product repair.
Reference solution
With independent auxiliary indices, the final all-zero projection fixes each register only at its own factor; summing over the common data index gives sum_k A(i,k)B(k,j), hence AB. Reusing one register instead introduces paths that leave its zero sector under V and return under U. A minimal example has one-dimensional data and a qubit auxiliary, U=V=X. Each individual clean block is <0|X|0>=0, so AB=0, but <0|X X|0>=1. Resetting an entangled auxiliary is not unitary and may erase coherence; it does not turn the same-register product into the coherent operator AB for free. Applying V inverse cancels V on the entire state and can also erase the desired action, not merely its garbage. A different coherent cleanup construction must be proved under its own promises and charged; disjoint fresh registers give the straightforward product construction. The matrix product of already-extracted blocks alone is not a proof of a particular same-register circuit.
Assessment rubric
- Correct independent-auxiliary finite sum gives AB (1 weight)
- U=V=X zero individual blocks but composite clean block1 (1 weight)
- Reset nonunitary and inverse can erase desired action; no free cleanup claim (1 weight)
Graph-grounded prerequisites
These are support/source anchors, not an automatically extracted theorem-dependency proof.
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.
Sources and provenance
- QuantumBlockEncoding/BlockEncodingClassics.lean
theorem matrix_mul_congr_pointwise (lines 792-797); def productCleanBlockCertificate 'cleanBlock := Matrix.mul left.cleanBlock right.cleanBlock' (lines 800-808); def productResourceCost adding auxiliaryQubits and gateCount, depth adds (lines 831-839)
Source SHA-256:94ac6632924df0a49b1ebd99bb5d9ed69b2ea463ec527033f38bd73deeb1346a· MIT (repository LICENSE) - QuantumBlockEncoding/ConcreteSemantics.lean
comment that any normalized orthogonal failure branch is additional unitarity evidence (lines 271-294)
Source SHA-256:454c0c5e215ca197c5883bedf74882f392d259c7afeadc63912230437698ebe5· MIT (repository LICENSE)
Contract: 0bdf1a4bf69df64ebe571fe8d04861d975e5b3cb3f22255aa53993b54edb49bb
Item digest: ee013faa49782085ff133a942fb0e639d3357fa9a4eed212f42f0bb7096d2323
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.