Block Encoding
Exercise BE-002
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
- Unitary circuit on S tensor W tensor D
- A clean workspace promise concerns all input data vectors on the signal-success subspace
- auxiliaryQubits = signalQubits + pureAncillas
- Clean block uses the all-zero auxiliary bra and ket simultaneously
Question
A circuit acts on a signal register S, a workspace W and a data register D, starting S,W at zero. The signal value0 is called success. Explain the additional mathematical promise needed to call W clean on every successful branch. Does knowing only the smaller submatrix obtained by projecting BOTH S and W to zero imply that promise? Give a two-dimensional workspace counterexample, and explain which auxiliary qubits still occupy physical space.
Hint: mathematical route
Success-sector workspace cleanup is an independent promise, not implied by the doubly projected block; a one-qubit rotation supplies a concrete counterexample.
- The smaller clean submatrix constrains only the all-zero workspace component, not other successful workspace values.
- A workspace rotation has nonzero excited output while its all-zero subblock remains exactly cos t.
- Therefore a clean-workspace success promise is additional to subblock equality.
Reference solution
Workspace cleanliness on signal success means that for every data input v, projecting the final state onto S=0 leaves a vector of the form |0>_S|0>_W tensor T v, with no component at S=0,W nonzero. This is an extra restriction on success-sector amplitudes. The doubly projected submatrix alone fixes only the W=0 component and does not constrain W nonzero. Counterexample: take signal and data one-dimensional and let W be a qubit with unitary R=[[cos t,-sin t],[sin t,cos t]],0<t<pi/2. Its doubly projected block is the scalar cos t, an exact legitimate block for that scalar target. Yet R|0>=cos t|0>+sin t|1>, so workspace is not clean even though signal success is certain. Both signal and workspace qubits enlarge the physical unitary, regardless of whether a resource ledger counts them in different roles. Projection is not itself uncomputation; a separately proved clean-workspace promise cannot be inferred just from the scalar clean submatrix.
Assessment rubric
- State success-sector workspace cleanup for every data input (1 weight)
- Valid rotation has correct projected block but dirty success sector (1 weight)
- Separate projection, cleanup, and allocated physical auxiliary space (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/BlockEncoding.lean
structure RegisterLayout {systemQubits, signalQubits, pureAncillas}; def auxiliaryQubits 'combines the signal qubits selecting the block with pure ancillas that must be returned to a clean state' (lines 14-30); structure BlockEncodingCost (lines 50-55)
Source SHA-256:fe06f75a29822e28ccdbfedfb0b0e87f90872620fae7aed359085fad8fae64b4· MIT (repository LICENSE)
Contract: b396769e0e1faf7adab0231ba5978a667474658f4b8b4777d6c6331a828627d5
Item digest: 0225404a2bcf4af0f22e5bf5145a57227181783389be19800bce939c379853e1
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.