Matrix Constructions
Exercise LA-111
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; every bond dimension is at most D
- Stored-scalar count sums 2*l*m over all cores
- Stored scalars count physically laid-out entries, not arithmetic operations
- Original derivation from inspected local source; no fresh Lean verification
Question
A matrix-product chain stores dense local cores; the number of stored scalars sums 2*l*m across cores, where l and m are the left and right bond dimensions of each core. Given that every bond of the chain is at most D and the chain has n cores, prove the stored-scalar count is at most 2*n*D^2. Then explain why this counts stored addresses only, and does not by itself bound arithmetic runtime.
Hint: mathematical route
A matrix-product chain of n cores with bonds at most D stores at most 2*n*D^2 scalars; this is a stored-address count and not a bound on contraction arithmetic.
- Bound a single core's stored entries by 2*D^2 using both bond bounds.
- Extract the tail's leading bond to justify m <= D at each step.
- Sum over cores by induction to reach 2*n*D^2.
- Distinguish stored addresses from contraction arithmetic cost.
Reference solution
Induct on the chain. The empty chain stores 0 scalars, which is at most 2*0*D^2. For a chain whose first core has bonds l (left) and m (right) followed by a tail, the stored count is 2*l*m + stored(tail). The bond bound gives l <= D and m <= D, so 2*l*m <= 2*D*D = 2*D^2. By the induction hypothesis stored(tail) <= 2*(n-1)*D^2. Adding, the total is at most 2*D^2 + 2*(n-1)*D^2 = 2*n*D^2. The required m <= D for the first core is read from the bound on the tail's leading left bond (or directly for a terminal core), so the inequality closes at every step. This counts the number of real entries physically laid out in the cores: it is a storage/address measure. It says nothing about the number of multiplications or additions used to contract the chain, nor about numerical precision; those are separate quantities. A per-bit-string amplitude still requires its own contraction work, which this bound does not estimate.
Assessment rubric
- Per-core bound 2*l*m <= 2*D^2 from both bond bounds (1 weight)
- Induction summing to 2*n*D^2 with correct bond extraction (1 weight)
- Explain this is a stored-address count, not a runtime bound (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
storedScalars75-77; storedScalars_le79-93; ofKernel_storedScalars95-98
Source SHA-256:d916236ffc04fb1d09c9737d77ad83c965ea12716d1f22d6e7c0ec7b1a34e974· MIT (repository LICENSE)
Contract: b8ef8ca34c83a343fe46910f0623319f7e960289542a7ef1fc1cec0cbf6bf6fe
Item digest: 913e7d71276fa5074d8dde978f1e7bb69b6655f8aaa0087808b89035aad8a38e
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 4. This is not measured graph distance or model difficulty.