Stored Cost Refinement
Exercise LA-204
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
- Recorded steps carry an exact angle and a pair of adjacent rows
- Eight independent primitive counters in the exact-real model
- The accumulated transform is replayed, never formed as a dense matrix product; costs are not finite-bit runtimes
- Original derivation from inspected local source; no fresh Lean verification
Question
A rectangular elimination records a chronological list of two-row rotation steps. Rather than forming the accumulated orthogonal transform by multiplying out dense plane-rotation matrices, a stored replay starts from a materialized identity and re-applies each recorded two-row rotation to the stored matrix in order; the empty list charges one read of the end marker, and each recorded step charges one read of the record, one field operation for halving its angle, two trigonometric calls for the pair of coefficients, and one stored two-row rotation. On a k-by-N working matrix a single such rotation costs the fixed amount described earlier (field, read and write terms linear in N and in the matrix dimension). Prove two things about replaying a list of L steps: first, that the result denotes exactly the product of the recorded plane rotations applied to the starting matrix, and second, that the total cost is L times a fixed per-step budget plus one extra read, with the extra read coming from the empty-list base case.
Hint: mathematical route
By list induction, prove a stored replay of L recorded rotations denotes the product of plane rotations (not formed densely) and costs L times a per-step budget plus one trailing read.
- The empty list returns the start matrix and the cons case rotates once then recurses.
- List induction shows the replay denotes the composed product of recorded plane rotations.
- Each step charges one field, two trig, a rotation and three reads, giving total L*budget + one trailing read.
Reference solution
Both claims go by induction on the step list. Correctness: for the empty list, replay returns the starting matrix, which equals the empty product applied to it. For a cons step followed by the rest, replay rotates the current matrix by the step's recorded angle and recurses; by the induction hypothesis the recursion denotes the remaining product, and one rotation realizes exactly the plane-rotation matrix of this step, so composing gives the full product applied to the start. This shows the stored replay refines the dense matrix-product specification without ever evaluating that product. Cost: for the empty list the only charge is the single end-marker read, matching 0*budget + one read. For a cons step, the step charges one read of the record, one field halving, two trigonometric calls and one two-row rotation; summing with the inductive cost L_tail*budget + one read gives (L_tail+1)*budget + one read, where the per-step budget collects exactly the field, two trig, rotation field/read/write and the three reads (two from the rotation, one from the record). Hence an L-step replay costs L*budget + one read, and the two reads inside the rotation plus the record read explain the three-read-per-step term, while the single trailing read is the base case.
Assessment rubric
- Prove by list induction that replay denotes the product of recorded rotations without forming the dense product (1 weight)
- Identify the per-step budget: one field, two trig, one rotation, and three reads (1 weight)
- Derive total cost L*budget + one read with the trailing read from the empty-list base case (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/StoredRectangularGivens.lean
replay110-118; replay_value120-128; replayStepBudget130-133; replay_cost135-143
Source SHA-256:f8638a6d287b3b984fa530b13eeb18e3992904543236bd0756eda41fa6490d98· MIT (repository LICENSE)
Contract: b247362adcb73658b60ff9b1a5815502f5f76ac26c79a6f59804d78da526f442
Item digest: 705a52ec7b52b60d5ea01c2f2bf97d622094dcf936d909b80d18cfd481591425
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.