State Preparation
Exercise SP-007
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
- the only hypothesis is clean-column equality of each stage with the corresponding tensor core; no global state action is assumed
- the boundary is an explicit bond vector supplied to the run
- the last emitted core multiplies on the left (same order as circuit evaluation)
- transfer at length 0 is the identity matrix
Question
In the sequential bond construction, a complete state after n emitted bits is produced by applying stage matrices in order, starting from an explicit bond boundary vector. Assume for each stage index t and each clean input column (fresh bit input = 0, bond input a) the stage entry equals the corresponding tensor core entry K t. Prove by induction on n that the full run amplitude at bit word x and final bond label b equals the matrix-vector product of the chronological transfer contraction of the cores with the boundary, (transfer K n x) applied to the boundary, read at b. State precisely which columns of the stages are therefore irrelevant.
Hint: mathematical route
The sequential run amplitude equals the chronological transfer contraction of the cores applied to the boundary, provable by induction using only clean-column equality.
- Base case: run at length 0 equals the boundary, and transfer at length 0 is the identity, so both sides agree.
- The length-(n+1) run is one step on the length-n run; the clean-column collapse writes its amplitude as a sum over the bond label of clean-column entries times prior amplitudes.
- Clean-column equality plus the inductive hypothesis identify the sum with coreSlice(K n)(x(last)) times the length-n transfer applied to the boundary.
- The recursive definition of transfer folds this into transfer K (n+1) x applied to the boundary, and fresh-bit-input-1 columns never enter, so completions there are irrelevant.
Reference solution
Induct on n. Base n = 0: run at length 0 is just the boundary read at the bond label, and transfer K 0 x is the identity matrix, so (transfer K 0 x) applied to boundary at b equals boundary b; both sides agree. Inductive step from n to n+1: by definition the length-(n+1) run is one step applied to the length-n run. Expanding the step via the clean-column collapse (only fresh-bit-input-0 columns act), the amplitude at (x, b) is sum over a of (stage entry at output bit x(last), bond b, clean column a) times (length-n run at (init x, a)). The clean-column hypothesis rewrites each stage entry to K n (x(last), b) a, i.e. the (b,a) entry of the emitted-bit slice coreSlice (K n) (x(last)). The inductive hypothesis rewrites the length-n run at (init x, a) to (transfer K n (init x)) applied to boundary at a. So the amplitude becomes sum over a of coreSlice(K n)(x(last)) at (b,a) times [(transfer K n (init x)) applied to boundary] at a, which is exactly the matrix-vector product coreSlice(K n)(x(last)) times (transfer K n (init x) applied to boundary), read at b. By the recursive definition of transfer, coreSlice(K n)(x(last)) * transfer K n (init x) = transfer K (n+1) x, and composing a matrix with a matrix-vector product equals the product matrix applied to the vector. Hence the amplitude equals (transfer K (n+1) x) applied to boundary at b, closing the induction. The irrelevant columns are exactly the fresh-bit-input-1 columns of every stage: they never appear in the collapsed sum, so arbitrary unitary completions on those columns leave the emitted state unchanged.
Assessment rubric
- Handles the base case using transfer at length 0 = identity and run at length 0 = boundary. (1 weight)
- Expands the inductive step via the clean-column collapse of one step into a sum over the bond label a. (1 weight)
- Applies the clean-column hypothesis and the inductive hypothesis, then recognizes the sum as coreSlice(K n)(x(last)) times the length-n transfer-applied-to-boundary, i.e. transfer K (n+1) x applied to boundary. (1 weight)
- States that only clean (fresh-bit-input-0) columns matter, so arbitrary completions on fresh-bit-input-1 columns are irrelevant. (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 86-110: noncomputable def transfer K | 0,_ => 1 | n+1,x => coreSlice (K n) (x (Fin.last n)) * transfer K n (Fin.init x); theorem run_eq_transfer (U K) (cleanColumns : for all t bit b a, U t (bit,b) (0,a) = K t (bit,b) a) (boundary) (n x b) : run U boundary n (x,b) = (transfer K n x).mulVec boundary b, proved by induction with step_apply, cleanColumns, ih, mulVec_mulVec
Source SHA-256:ad4542b108d44f196f2a02f78e59b58f43d45b1e890709cf4c22e1222805d5c5· MIT (repository LICENSE)
Contract: 22dfe5a670aeba9bec8bea6209789cb26784265fb68d49a47177c3a3c741f7f4
Item digest: f47a739f7ea08d5acd553764322f8c24c2c6b1e7c40abe98923f3bceb2f8963a
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 4. This is not measured graph distance or model difficulty.