Matrix Constructions
Exercise LA-110
local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- Fixed-width real cores; right boundary vector of length D
- Readout is the chronological matrix-vector product from the right boundary
- Absorbing the right boundary makes the terminal bond 1
- Original derivation from inspected local source; no fresh Lean verification
Question
In a matrix-product chain with width-D cores and a fixed right boundary vector of length D, define the readout of a bit string as the chronological matrix-vector product that starts from the right boundary and applies each core's selected matrix in turn. Prove that building the chain by absorbing the right boundary into the last core (so the terminal bond is 1) reproduces exactly this readout at every incoming bond.
Hint: mathematical route
Absorbing the right boundary vector into the last core of a matrix-product chain (terminal bond 1) reproduces the chronological matrix-vector readout at every incoming bond, by induction.
- Set up induction on the number of cores left of the last.
- Base case: the single absorbed core equals the length-one readout.
- Inductive step: expand the contraction as a sum over the next bond.
- Match the readout recursion by the induction hypothesis.
Reference solution
Induct on the number of cores beyond the last. The base case is a single core: absorbing the right vector makes the last core's entry at incoming bond a equal to sum over out-dependent action of (selected matrix times right)[a], which is by definition the readout of a length-one word at bond a; the terminal bond-1 contraction is just this scalar. For the inductive step with one more core on the left, the contraction of the built chain at bond a is sum over b of (selected matrix of the new core)[a,b] times the contraction of the shorter built chain at bond b. By the induction hypothesis the shorter contraction equals the readout starting one step later, so the whole expression is sum over b of M[a,b] * readout(rest)[b], which is exactly the matrix-vector product defining readout at the current step. Hence the built chain contracts to the readout for every word and every incoming bond. This identifies two definitions of the same amplitude; it makes no contraction-cost assertion and the terminal rank is one by construction.
Assessment rubric
- Base case: single absorbed core equals the length-one readout (1 weight)
- Inductive step expands the contraction as a matrix-vector product over the next bond (1 weight)
- Apply the induction hypothesis to match the readout recursion (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/MatrixProductChain.lean
readout14-17; tailChain20-24; tailChain_contract26-35
Source SHA-256:d916236ffc04fb1d09c9737d77ad83c965ea12716d1f22d6e7c0ec7b1a34e974· MIT (repository LICENSE)
Contract: d297079a01a83660ae8d70ff066f48ec012c846fe6043d1cbe110f1d6640c172
Item digest: fad513662c7653c200c59df3ebf0190dd261233cbc497793dff6c0821c892001
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 4. This is not measured graph distance or model difficulty.