Stored Cost Refinement
Exercise LA-205
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
- The eight per-counter polynomial budgets are as stated
- Totalling means summing the eight counters
- Exact-real word-RAM operation model with no bit-level charge; not a finite-bit runtime
- Original derivation from inspected local source; no fresh Lean verification
Question
A full stored rectangular compilation of an N-by-M matrix produces a reduced residual, a chronological list of rotation steps, and a fully accumulated N-by-N transform. In the eight-counter exact-real model its per-counter cost has been bounded by an explicit polynomial budget whose values on the eight counters are: field = N*M*(6*M+6*N+9); square root = N*M; inverse-cosine = N*M; other trigonometric = 4*N*M; comparison = 2*N*M + M + N*N; read = N*M*(10*M+14*N+10) + 2*N*N + 2*N + 1; write = N*M*(6*M+10*N+1) + 2*N*N + 2*N; emitted records = N*M. Prove that the sum of all eight counters is bounded by N*M*(22*M+30*N+29) + 5*N*N + 4*N + M + 1, and explain why this single scalar is an operation count in an extended exact-real model and not a finite-bit running time.
Hint: mathematical route
Prove the eight per-counter polynomial budgets of a stored rectangular compilation sum to N*M*(22*M+30*N+29)+5*N*N+4*N+M+1 and read it as an exact-real, not finite-bit, count. The write budget includes the required +2*N spine term.
- The N*M-scaled parts of all eight counters collect to 22*M+30*N+29.
- The remaining quadratic, linear and constant terms sum to 5*N*N+4*N+M+1.
- The scalar total is an exact-real operation count, not finite-bit complexity.
Reference solution
Add the eight per-counter polynomials. Group the N*M*(...) coefficients: from field 6*M+6*N+9, from read 10*M+14*N+10, from write 6*M+10*N+1, giving 22*M+30*N+20 inside the N*M factor; the square-root, inverse-cosine, emitted and part of the comparison counters each contribute an extra N*M (that is 1+1+1 from sqrt/angle/emit, 4 from the other trig, and 2 from the comparison), adding 9 more inside the same N*M factor and yielding N*M*(22*M+30*N+29). The remaining non-N*M terms are: comparison M + N*N, read 2*N*N + 2*N + 1, write 2*N*N + 2*N; summing the N*N terms gives 5*N*N, the linear-in-N terms give 4*N, the M term stays M, and the constants give 1. Hence the grand total is N*M*(22*M+30*N+29) + 5*N*N + 4*N + M + 1. The quantity counts exact-real primitive operations (field arithmetic, exact square roots and trigonometric evaluations, exact comparisons) and stored-word traffic in a word-RAM style model; it charges no bit-level cost for representing or rounding reals, so it is explicitly not a finite-bit running-time bound.
Assessment rubric
- Correctly collect the N*M coefficient to 22*M+30*N+29 across all eight counters (1 weight)
- Sum the lower-order terms to 5*N*N + 4*N + M + 1 (1 weight)
- Explain the exact-real word-model reading and that it is not finite-bit complexity (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
polynomialBudget213-221; total236-238; compile_total_cost_le240-253
Source SHA-256:f8638a6d287b3b984fa530b13eeb18e3992904543236bd0756eda41fa6490d98· MIT (repository LICENSE)
Contract: dfd4c9600efe5d894a40f124912fba467b0c48a8926b9c9c15bf772aa8035008
Item digest: 3e52d9ef18efc62d9cff3b7087e30bb8b30494040dba6f8b2292182c2274badc
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.