State Preparation
Exercise SP-012
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
- ranks change inside a fixed padded register, with an explicit active-label predicate per stage
- stages agree with the tensor cores only on active input columns; inactive completions are arbitrary
- active a means the predicate holds for bond label a at that stage; inactive labels are the complement
- transfer is the chronological contraction of the cores
Question
In the sequential bond construction with rank changes inside a fixed padded register, a reader claims: 'If the completion columns of the stages (the inputs for inactive, zero-padded bond labels) are chosen differently, the emitted state could change, so the construction is ambiguous.' Refute this using the support-propagation argument, and state precisely the minimal hypotheses under which the emitted state is uniquely the tensor contraction regardless of the inactive completion.
Hint: mathematical route
Inactive zero-padded completion columns are gauge freedom: support propagation forces the emitted state to equal the tensor contraction regardless of those columns, refuting an ambiguity claim.
- Under initial support, core support, and active-only clean columns, the run has no leakage: inactive-label amplitudes are zero at every stage.
- The step sum splits into active terms (fixed by clean columns) and inactive terms (killed by the zero prior amplitude), so inactive stage columns never contribute.
- Hence run equals the tensor contraction applied to the boundary with no inactive-column constraint, so differing completions give the identical emitted state.
Reference solution
The claim is false. The emitted state depends only on amplitudes carried on ACTIVE bond labels, and inactive labels provably carry zero amplitude throughout the run, so columns acting on inactive inputs multiply zero and never contribute. Concretely, assume: (initial support) the boundary vanishes on inactive labels at stage 0; (core support) each tensor core is zero outside the next active label set; and (clean columns) each stage equals the tensor core only on active input columns. Then one proves, by induction, that the run has no leakage: at any intermediate stage the amplitude on an inactive label is zero. The induction splits the step sum over bond labels a into active and inactive: on active a the clean-column hypothesis supplies the correct core entry, while on inactive a the inductive support invariant makes the prior amplitude zero, killing the term regardless of what the stage's inactive column contains. This yields the rank-changing identity run = (transfer K n x) applied to boundary with no constraint on inactive completion columns. Because the right-hand side involves only the cores K and the boundary, two stage families that agree on active columns but differ arbitrarily on inactive completion columns produce the SAME emitted state. Minimal hypotheses: initial support, core support, and active-only clean-column equality. Under these, the emitted state is uniquely the tensor contraction, so the inactive completions are genuine gauge freedom, not a source of ambiguity. (The completions still matter for full unitarity of each stage, but not for the emitted amplitudes.)
Assessment rubric
- States that only active-label amplitudes drive the emitted state and that inactive labels carry zero amplitude throughout. (1 weight)
- Gives the three hypotheses (initial support, core support, active-only clean columns) and the no-leakage induction splitting the step sum into active/inactive. (1 weight)
- Shows inactive terms vanish because prior amplitude is zero there, independent of the stage's inactive column entries. (1 weight)
- Concludes run = transfer applied to boundary with no inactive-column constraint, so differing completions give the same state (gauge freedom), refuting the ambiguity 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/SequentialBondPreparation.lean
lines 125-174: theorem transfer_boundary_supported (initialSupport, coreSupport) (inactive : not active n b) : (transfer K n x).mulVec boundary b = 0; theorem run_eq_transfer_of_supported (initialSupport, coreSupport, cleanColumns : for all t bit b a, active t a -> U t (bit,b) (0,a) = K t (bit,b) a) : run U boundary n (x,b) = (transfer K n x).mulVec boundary b; theorem run_supported : run U boundary n (x,b) = 0 when inactive
Source SHA-256:ad4542b108d44f196f2a02f78e59b58f43d45b1e890709cf4c22e1222805d5c5· MIT (repository LICENSE)
Contract: 9b4945b6459a978af30e43cf0f57928a6a704439a1f8a079b9bd4af523571658
Item digest: 071ab0623ad314e9dec69f07d951817d7eba436b0cdbfe21a38c52f4ec7b8e30
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.