Stored Cost Refinement
Exercise LA-201
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
- Finite-dimensional real matrices stored as nested vectors; all scalars are exact reals
- Eight independent primitive counters; each primitive call costs one unit of its own counter
- Proof checking, counter bookkeeping and loop-index arithmetic are free; a materialized pass of length M charges two reads and two writes per index
- Original derivation from inspected local source; no fresh Lean verification
Question
Work in an exact-real word-operation model that keeps eight separate running counters: field operations, square roots, inverse-cosine calls, other trigonometric calls, exact comparisons, stored-word reads, stored-word writes, and emitted records. Each primitive call adds one unit to its own counter; proof checking, counter bookkeeping and loop-index arithmetic are free, and stored data are nested vectors. A plane rotation acts on two stored length-M real rows u and v with coefficients c and s, returning rows whose j-th entries are c*u_j - s*v_j and s*u_j + c*v_j. The implementation first materializes a stored vector of M computed entry-pairs, then materializes the first output row and the second output row as two further stored passes. Every materialized pass over M indices additionally charges two reads and two writes per index to write each intermediate value and read it back for projection, and each single entry-pair is computed with exactly the six field operations c*u_j, s*v_j, s*u_j, c*v_j, their difference, and their sum. Prove that rotating the two rows costs exactly 6*M field operations, 10*M reads and 6*M writes, and account for the origin of every read and write.
Hint: mathematical route
In an eight-counter exact-real operation model, prove a stored two-row plane rotation on length-M rows costs exactly 6*M field, 10*M read and 6*M write operations, accounting for each from the three materialized passes.
- A single entry-pair costs six field operations plus two input reads.
- Each materialized pass of length M adds two reads and two writes per index on top of its entry work.
- Summing the three passes yields exactly 6*M field, 10*M read and 6*M write.
Reference solution
Count the three materialized passes separately. Pass 1 computes the entry-pairs: for each index j it reads u_j and v_j (2 reads) and performs the six field operations, so its own work is 6 field + 2 reads per index; the materialization surcharge adds 2 reads + 2 writes per index, giving 6*M field + 4*M reads + 2*M writes. Pass 2 materializes the first output row by reading the stored pair at each index (1 read) and projecting its first component (free), with surcharge 2 reads + 2 writes, giving 3*M reads + 2*M writes. Pass 3 does the same for the second component, another 3*M reads + 2*M writes. Summing: field = 6*M; reads = 4*M + 3*M + 3*M = 10*M; writes = 2*M + 2*M + 2*M = 6*M. The field count is purely the arithmetic of the rotation; the reads split into 2*M genuine input reads, 2*M pair reads for the two projections, and 6*M materialization read-backs; the writes are the three stored passes at 2*M each. This is an exact operation count in the extended exact-real model, not a finite-bit running-time bound, and it does not assert that any of these operations is physically free.
Assessment rubric
- Each entry-pair uses exactly six field operations and two input reads (1 weight)
- Correctly charge the two-read/two-write materialization surcharge on all three passes (1 weight)
- Derive the exact totals 6*M field, 10*M read, 6*M write with per-pass accounting (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/StoredGivens.lean
entryPair123-130; entryPair_cost135-138; collect60-64; collect_cost83-85; rowPair141-153; rowPair_cost272-277
Source SHA-256:87a1f69d5b138f23c96a6f77a438aa81edef27427cb2581c4defe019079d2ee4· MIT (repository LICENSE)
Contract: d7b3dec5159690491a18cfeb97141c85667401a599b0e6ef1b11c68ca6886ca8
Item digest: 4b2411a0ba33a8286691461446ef4686f5dd20ab90d92061bc04fe1fbd74eb65
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.