Stored Cost Refinement
Exercise LA-207
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
- Reading a stored core entry is a row read followed by an entry read (two reads)
- Eight independent primitive counters; pure zero carries no charge
- The accumulation addition is one field operation per summand; counts are exact-real, not finite-bit
- Original derivation from inspected local source; no fresh Lean verification
Question
In the eight-counter exact-real model, a bounded sum over an index set of size k is evaluated by a monadic fold: starting from the pure value zero (no charge), each of the k summands is produced and then added to the running accumulator with one field addition. Suppose every summand has the same per-counter cost B. Prove that the whole sum costs exactly k*(B + one field operation). Then specialize to a single contraction entry over a bond of size D, where each summand reads one entry of a stored core (two reads) and one entry of a stored vector (one read) and multiplies them (one field), so B is three reads plus one field, and conclude that the entry costs exactly D*(three reads + two field operations).
Hint: mathematical route
Prove a size-k monadic sum of equal-cost summands costs k*(B+one field), and specialize to a bond-D contraction entry costing D*(three reads + two field).
- An empty bounded sum has zero cost and a (k+1)-sum charges B plus one accumulation field over the k-tail.
- Induction yields the exact sum cost k*(B+field).
- With B = three reads + one field per summand, the contraction entry costs D*(three reads + two field).
Reference solution
Induct on k. Base case k=0: the empty sum is the pure zero with no charge, matching 0*(B+field). Inductive step: a sum over k+1 indices produces the first summand (cost B), binds an addition of it to the recursively evaluated tail (that addition is one field operation), and the tail is a sum over k indices. By the induction hypothesis the tail costs k*(B+field); adding the first summand's B and the one field for its combination gives B + field + k*(B+field) = (k+1)*(B+field). So the sum costs exactly k*(B+field) on every counter. For the contraction entry: each summand reads a stored core entry, which is a row read followed by an entry read (two reads), reads one stored vector entry (one read), and multiplies the two values (one field), so B = three reads + one field. Substituting into the law gives D*((three reads + one field) + one field) = D*(three reads + two field operations). The second field per index is exactly the accumulation addition, which is why the entry has two field operations per bond index rather than one. This is an exact count in the extended exact-real model, not a finite-bit cost.
Assessment rubric
- Prove the sum cost law k*(B+field) by induction with correct base and accumulation step (1 weight)
- Identify the summand cost B as three reads plus one field for a contraction entry (1 weight)
- Conclude D*(three reads + two field), attributing the extra field to accumulation (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
terminalEntry11-16; sumEntries_cost_eq125-133; terminalEntry_cost135-143
Source SHA-256:7a697d064a5fddd909bba048d6adc36cb645421bd565e2357588fef1ff0449f2· MIT (repository LICENSE)
Contract: 9b66821c7859076e9dd7de46a0f481c2eec7a0d6f88ad71b87ede1922079897a
Item digest: 172127f1825454b15f930b84064179096752d4fe8288d27eba49940a6a8d600e
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.