Stored Cost Refinement
Exercise LA-202
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 of N rows
- Replacing a stored row is charged as a full persistent copy of N reads and N writes
- No in-place-update or copy-on-write optimization is assumed; the bound is an exact-real operation count, not a finite-bit runtime
- Original derivation from inspected local source; no fresh Lean verification
Question
Continue in the eight-counter exact-real operation model where stored matrices are vectors of N stored rows and replacing one stored row is charged as a full persistent copy costing N reads and N writes, never an in-place update. A rotation step on an N-by-M stored matrix reads the two rows i and j to be combined, computes the two rotated rows (whose production costs 6*M field, 10*M read and 6*M write), and then stores the two new rows with two separate persistent row-replacements. Prove that one such rotation step costs 6*M field operations, 10*M + 2*N + 2 reads, and 6*M + 2*N writes, and explain why the step cannot be made cheaper by assuming in-place row updates.
Hint: mathematical route
Prove one stored rotation step costs 6*M field, 10*M+2*N+2 read and 6*M+2*N write operations, where the 2*N spine-copy term is a stipulated charge of the cost contract.
- Reading the two combined rows and producing the rotated rows contributes 2 reads plus 6*M field, 10*M read, 6*M write.
- Each persistent row-replacement copies the N-row spine for N reads and N writes.
- Summation gives 6*M field, 10*M+2*N+2 read, 6*M+2*N write, and the 2*N term is the contract's stipulated spine-copy charge.
Reference solution
Add the charged subparts. Reading rows i and j from the stored matrix contributes 2 reads. Producing the two rotated rows contributes 6*M field, 10*M reads and 6*M writes. Each persistent row-replacement copies the whole length-N spine of rows, charging N reads and N writes; two replacements add 2*N reads and 2*N writes. Totals: field = 6*M; reads = 10*M + 2 + 2*N; writes = 6*M + 2*N. The 2*N read/write term is a deliberate feature of the cost contract: the model charges a full persistent row-replacement as N reads and N writes of the row-index spine. This is a stipulated charge, not a theorem that no sharing is possible; a functional persistent vector may in fact share the unaffected rows, but the model declines to credit any such copy-on-write or structural-sharing optimization and bills the full spine copy regardless. Charging it this way makes the bound robust: it holds for any implementation of row replacement without relying on aliasing analysis, and it is an exact-real word-operation count rather than a finite-bit machine running time. The 2*N term would only vanish under a model that explicitly credits in-place or shared updates, which this cost contract does not.
Assessment rubric
- Account the two input row reads and the row-production cost (1 weight)
- Charge each persistent replacement as a full N-read, N-write spine copy (1 weight)
- Explain the 2*N term is a stipulated spine-copy charge in the cost contract, not a proof that sharing is impossible (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
replace67-68; rotate161-167; rowPair_cost272-277; rotate_cost279-285
Source SHA-256:87a1f69d5b138f23c96a6f77a438aa81edef27427cb2581c4defe019079d2ee4· MIT (repository LICENSE)
Contract: 110acf94b75690eb0a06def756120100d44658b9107accf8fbd0d63d1616d9a6
Item digest: cffaec368aa74c7a29a98568529ed0821b8c45328ba670593e9b00c3d43c19f3
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.