Stored Cost Refinement
Exercise LA-203
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 stored matrices; eight independent primitive counters
- The per-step budget is independent of the angle-computation branch
- A zero-angle rotation still emits one record; the budget is an upper bound on arithmetic counters only
- Original derivation from inspected local source; no fresh Lean verification
Question
In the eight-counter exact-real model, a column sweep eliminates entries below a pivot by performing a chronological chain of elimination steps. Each step first computes an elimination angle and the two rotation coefficients (bounded by a fixed per-step budget B that is independent of which branch of the angle computation is taken), applies a rotation to the stored matrix, and then emits exactly one rotation record (one unit on the emitted-record counter). A sweep performing k steps is defined by recursion: zero steps emit nothing and do no work; a sweep of k+1 steps performs one elimination step and then recurses on the resulting matrix, emitting one record for the step. Prove by induction on k that (a) the total cost of a k-step sweep is at most k*(B + one emit) on every counter, and (b) the emitted-record counter equals exactly k, even though some steps may rotate by a harmless zero angle.
Hint: mathematical route
By induction on step count, prove a k-step column sweep is bounded by k*(step budget + emit) on every counter and emits exactly k records including zero-angle steps.
- The recursion splits a (k+1)-step sweep into one step, the k-step tail, and one emission.
- The branch-independent step budget bounds each step, giving the k*(B+emit) upper bound by induction.
- Each step emits exactly one record, so the emit counter equals k exactly, even for zero-angle steps.
Reference solution
Argue by induction on the number of steps k. Base case k=0: the sweep returns the input unchanged with zero cost on every counter, so both the bound 0*(B+emit) and the exact emit count 0 hold. Inductive step k+1: by the recursive definition the sweep cost equals the cost of one elimination step, plus the cost of the k-step sweep on the updated matrix, plus one emitted record. For (a), the single step is bounded by B on every counter (the per-step budget already absorbs the branch-independent angle budget, both rotation coefficients, the rotation, and the stored reads), the recursive part is bounded by k*(B+emit) by the induction hypothesis, and the emit contributes one unit; adding gives at most (k+1)*(B+emit) on every counter. For (b), the single step emits exactly one record and the recursive sweep emits exactly k by hypothesis, with no other operation touching the emit counter, so the total is exactly k+1. The exact emit equality holds regardless of the actual angles because a zero-angle rotation still produces and emits its record; the step budget B is only an upper bound on the arithmetic counters, so the two claims are of different strengths: an exact count for emissions and an inequality for the rest.
Assessment rubric
- Set up induction on step count with correct base and recursive decomposition (1 weight)
- Prove the k*(B+emit) upper bound using the branch-independent step budget (1 weight)
- Prove the emit counter equals exactly k including zero-angle steps, distinguishing exact count from upper bound (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
columnSweep219-229; stepBudget300; columnSweep_cost_le313-326; columnSweep_emit343-353
Source SHA-256:87a1f69d5b138f23c96a6f77a438aa81edef27427cb2581c4defe019079d2ee4· MIT (repository LICENSE)
Contract: 7b445c9300f8c5cdf5e1e627da02a5e2779dce40b8a7f232dcf5bcbd711dc1a7
Item digest: d3c7ffab655e801f0c3275b31d71aff77610f9d16830e0dfc9b47683fbb647f7
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.