Stored Cost Refinement
Exercise LA-208
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
- All cores stored and bond-bounded by D; reference copying is charged per remaining core
- Eight independent primitive counters; input cores already materialized
- No kernel callback is evaluated in production; counts are exact-real, not finite-bit
- Original derivation from inspected local source; no fresh Lean verification
Question
A stored matrix-product chain over n+1 cores, each of bond size D, is closed into a scalar-boundary chain in two conceptual halves. First the tail is processed recursively: at the last position the terminal core is contracted against a right boundary vector, and at every earlier position the current core is kept while the remaining table is copied by reference and the tail is recursed; a fixed small per-node record is charged at each position. Second the leftmost core is contracted against a left boundary vector. The returned chain exactly refines the kernel chain contracted against the two boundary vectors. Prove that the summed cost of the whole closure is bounded by a polynomial that is quadratic in the chain length n and cubic-free but quadratic in the bond D, and explain why the tail recursion contributes an n-squared term while the single left closure contributes only a bond-dependent term with no dependence on n.
Hint: mathematical route
Prove the stored chain closure costs 20*D-squared+30*D+5*n-squared+7*n+constant, explaining the n-squared term as a reference-copy series and the n-independent left closure.
- The tail recursion over n+1 positions copies references whose per-position cost grows with the index.
- The accumulated reference-copy series is quadratic in n, giving the 5*n-squared+7*n term.
- The single left closure is bond-dependent only, so the total is 20*D-squared+30*D+5*n-squared+7*n+constant.
Reference solution
Split the accounting as the construction does. The tail recursion visits n+1 positions. The terminal contraction at the last position contracts a D-by-D core against a length-D vector, costing on the order of D-squared field and read work plus boundary materialization, a fixed function of D. Each earlier position copies the remaining table of references (cost linear in the number of remaining cores, i.e. linear in the position index) and charges a fixed node record; summing the reference-copy cost over the n earlier positions gives an arithmetic series that is quadratic in n, which is the source of the n-squared term, while the fixed node records contribute a term linear in n. Hence the tail total is bounded by a constant times D-squared plus a constant plus terms 5*n-squared + 7*n + constant. The left closure performs exactly one initial contraction of a D-by-D core against a length-D left vector plus one node record; this is a single bond-dependent cost with no sum over positions, hence no n dependence. Adding the two halves gives the closure bound 20*D-squared + 30*D + 5*n-squared + 7*n + constant. The decoupling is structural: the tail walks the whole chain so its copying accumulates with length, whereas the left boundary touches only the one leftmost core. All of this is counted in the extended exact-real word model, not as finite-bit running time, and the referenced cores are already materialized so no kernel callback is evaluated.
Assessment rubric
- Separate the n+1-position tail recursion from the single left closure (1 weight)
- Explain the n-squared term as the arithmetic series of reference-copy costs over positions (1 weight)
- Explain why the left closure is bond-dependent only, with no n dependence, and note exact-real counting (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/StoredMatrixProductChain.lean
ofTable55-59; tailChain_total_cost_le202-214; closeLeft_tail_total_cost_le216-226; ofTable_total_cost_le230-237
Source SHA-256:7a697d064a5fddd909bba048d6adc36cb645421bd565e2357588fef1ff0449f2· MIT (repository LICENSE)
Contract: d3e686b4fc622d99fc1e9bbfea90d5c6b8072d7cb6a8c49a241aa61ef2a137ad
Item digest: 2af4654334ec83645d32e3ac7541aa9ca67e8c78afa43aa5ed50f9d40b1ea312
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.