Block Encoding
Exercise BE-011
local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- Normalizer N (normalizerA) is a complex scalar; the counterexample needs N != 0
- B is Hermitian (as in the PDE theorem) for the corrected block to equal S1
- Each term scaled by 1/2; filler is N*e^{i*phi} on the lower-right diagonal
- S1 is the Hermitian part of [[A,B],[0,0]] with lower-right block 0
Question
In an LCU-style assembly of a Hermitian piece, each selected term contributes a scaled controlled-phase source whose upper block carries the intended operator and whose lower-right filler block is normalizer times a phase e^{i*phi}. A source writes both filler phases as e^{i*pi} = -1 and claims the two filler blocks cancel so the clean block equals the intended Hermitian piece S1. Show by direct computation of the lower-right clean entry that the printed all-(-1)-phase choice does NOT cancel, give the exact value of that entry, prove the clean block therefore differs from S1 when the normalizer is nonzero, and exhibit the corrected phase assignment that does make the fillers cancel while preserving the intended operator blocks.
Hint: mathematical route
Shows the all-(-1) LCU filler phases give lower-right clean entry -N and so cannot equal S1 (whose lower-right block is 0) for nonzero normalizer, and gives the phase-balanced correction that recovers S1.
- The all-(-1) filler phases give lower-right clean entry (1/2)N(-1)+(1/2)N(-1) = -N.
- S1 has lower-right block 0, so for N!=0 the printed clean block is not S1.
- Replacing one filler phase by its opposite (0 vs -1) cancels the lower-right fillers and preserves the upper blocks, giving S1 under Hermitian B.
Reference solution
The assembly adds three scaled sources (each scaled by 1/2): a controlled-phase source for A with filler phase, one for A-dagger with filler phase, and a Pauli-X-tensor-B term that has zero lower-right block. The lower-right filler of a scaled controlled-phase source with normalizer N and phase e^{i*phi} is (1/2)*N*e^{i*phi} on the diagonal. With BOTH A and A-dagger terms using phase e^{i*pi} = -1, the lower-right diagonal clean entry is (1/2)*N*(-1) + (1/2)*N*(-1) + 0 = -N. So the printed clean lower-right block equals -N (the identity-filler blocks ADD rather than cancel). But the intended Hermitian piece S1 has lower-right block equal to 0 (S1 is the Hermitian part of the homogenized matrix [[A,B],[0,0]], whose lower-right block is 0). Therefore, if N != 0, the printed clean block has lower-right entry -N != 0 = S1's lower-right entry, so the printed-phase clean block is NOT equal to S1 - a genuine counterexample to the all-(-1) cancellation claim. Corrected assignment: give the two filler phases OPPOSITE signs, e.g. keep the A-dagger term at phase -1 but set the A term's filler phase to 0 (i.e. e^{i*0}=+1) while leaving its upper operator block intact. Then the lower-right clean entry becomes (1/2)*N*(+1) + (1/2)*N*(-1) + 0 = 0, matching S1's zero lower-right block, and the upper A, A-dagger and off-diagonal B blocks are unchanged, so the phase-balanced clean block equals S1 exactly (under the paper's Hermitian B). The lesson: filler phases are a real proof obligation - identical phases add, opposite phases cancel; only a phase-balanced choice recovers the intended block.
Assessment rubric
- Compute the printed all-(-1)-phase lower-right clean entry as -N (fillers add, not cancel) (1 weight)
- Show S1's lower-right block is 0, hence for N!=0 the printed clean block differs from S1 (genuine counterexample) (1 weight)
- Give the corrected opposite/phase-balanced assignment making the lower-right entry 0 while preserving upper operator blocks, so the clean block equals S1 (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/GHLHamiltonian.lean
def scaledControlledPhaseSource lower-right filler 'if i=j then normalizer*phase' (lines 191-198); def eq29PrintedClean (lines 221-229); theorem eq29PrintedClean_lowerRight = -normalizerA (lines 247-251); theorem eq29PrintedClean_ne_S1 (lines 254-262); theorem eq29PhaseBalancedClean_eq_S1 (lines 268-296)
Source SHA-256:2e453b72433b4031e29ba73e9e22c3be0f63e4640781b9c81219fdf908ee80c7· MIT (repository LICENSE)
Contract: 9e9bccaae57c46fe1fff05df06e0c0071e3529ef445ddaa4594a06051afbdbfe
Item digest: b64c8446192d113eddb6f829ef3cce766d74ac79527a75bec2bebc8674cce7fd
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.