Stored Cost Refinement
Exercise LA-209
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
- Every bond along the chain is at most D; input cores are stored tables
- Eight independent primitive counters plus a fixed six-word node record
- The recursive environment is read, not recomputed; counts are exact-real, not finite-bit
- Original derivation from inspected local source; no fresh Lean verification
Question
A stored tensor-train norm is computed by streaming local Gram environments from right to left. At the empty tail the environment is a materialized identity of bond size r. At a non-empty node carrying a core of left bond l and right bond m, the recursively computed right environment E (an m-by-m stored matrix) is updated: for each of the two physical bits the core slice is contracted with E (a first materialized pass) and the result is contracted with the transposed slice (a second materialized pass), and the two per-bit matrices are added; a fixed six-word node record is charged. Each per-node update therefore costs on the order of l*m*m + l*l*m matrix-contraction work plus additive and materialization terms. Assume every bond along a length-n chain is at most D. Prove by induction on the chain that the total summed cost of the Gram computation is bounded by n*(24*D-cubed + 25*D-squared + 20*D + 6) + 5*D-squared + 4*D + 6.
Hint: mathematical route
By chain induction, prove the stored Gram-environment computation costs at most n*(24*D-cubed+25*D-squared+20*D+6)+5*D-squared+4*D+6, with the cubic term from the per-node contractions.
- The empty-tail identity environment plus its node record is bounded by 5*D-squared+4*D+6.
- One node update is bounded by 24*D-cubed+25*D-squared+20*D with the cubic term from the two contractions.
- Induction over the chain accumulates the per-node coefficient n times.
Reference solution
Induct on the chain. Base case (empty tail): the environment is the materialized identity of bond r at most D, whose summed cost is 5*r-squared + 4*r at most 5*D-squared + 4*D, plus the fixed node record 6; this matches the n=0 instance of the bound. Inductive step at a node with left bond l, right bond m and tail chain C: the recursive Gram of C is bounded by the induction hypothesis (its bonds are at most D). The one-node update contracts the stored core against the already-stored environment E for both bits and adds the results; bounding l and m by D, the update's summed cost 12*l*m*m + 12*l*l*m + 8*l*m + 17*l*l + 20*l is at most 24*D-cubed + 25*D-squared + 20*D, and the node record adds 6, so one node contributes at most 24*D-cubed + 25*D-squared + 20*D + 6. Adding this to the inductive bound for the tail increments the n-coefficient by one, giving (n+1)*(24*D-cubed + 25*D-squared + 20*D + 6) + 5*D-squared + 4*D + 6. The cubic-in-D term comes from the two matrix contractions, each costing on the order of a bond cubed when all three dimensions reach D. These are exact-real word-operation counts including every materialization pass, not finite-bit or whole-machine runtimes; the two uses of E are stored reads of the same cached environment, not a recomputation.
Assessment rubric
- Base case bounds the identity environment plus node record by 5*D-squared+4*D+6 (1 weight)
- Bound one update by 24*D-cubed+25*D-squared+20*D using l,m at most D, attributing the cubic term to the contractions (1 weight)
- Complete the induction to the per-node coefficient and note exact-real counting with a cached environment (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/StoredTensorTrainNorm.lean
update80-86; gram103-108; update_total_cost_le234-242; gram_total_cost_le256-284
Source SHA-256:60fa71fc821f7598f5df739b231f5b25cf1927824d2b028ef723f9ee04074011· MIT (repository LICENSE)
Contract: b071581d64c0f7cb6fcc68cea7880d35c840361e2a11e51728274fbce2b0cc64
Item digest: 6e688a66b2ad5ce4760787a4e1ca2cbadba1fb9f536048ff3512ea316b3b0157
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.