Stored Cost Refinement
Exercise LA-206
nl bridge from inspected source. Explicit question version 2 with distinct contract-change review; the predecessor question is not equivalent current gold. Core, family and split are retained. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- Wide shape m at most n; stored matrices are nested vectors
- Each materialization reads two stored words per output entry plus the surcharge
- Sequential stage costs add per counter; bounds are exact-real, not finite-bit
- Original derivation from inspected local source; no fresh Lean verification
This question explicitly revises its historical contract. A Lean companion must bind the current contract hash, not the predecessor hash. This is one reserved core, not two exercises.
Question
Let A be a stored real m-by-n matrix, with m at most n. Its wide thin-LQ routine transposes A, runs the full stored rectangular compiler on the transpose, extracts R as an m-by-m matrix from the residual, and extracts Q as an m-by-n matrix from the accumulated transform. Costs are vectors of nonnegative integer operation counters. Write C(X) for the actual counter vector of the rectangular compiler on stored input X, and P(N,M) for its declared polynomial upper budget, so C(X) is at most P(N,M) componentwise for every N-by-M X. For an N-by-M materialization whose entries each read one row and one entry, the exact counter vector is E(N,M)=2*N*M*tick(read)+(N*M+N)*(2*tick(read)+2*tick(write)). Here tick(op) is one unit in counter op and zero in the others. Let At be the actual stored transpose produced by the first stage.
Assess the assertion that the actual wide cost always equals E(n,m)+P(n,m)+E(m,m)+E(m,n). Give a concrete counterexample if it is false; the emit counter at m=n=1 is a useful discriminator. Then derive the exact additive identity in terms of C(At), and prove the resulting componentwise upper bound. Finally show that the R and Q returned by this same routine satisfy A=R*Q and Q*Q-transpose=I_m, including rank-deficient inputs and empty dimensions. Distinguish this wide routine from the all-shape dispatcher and keep operation counts separate from finite-bit runtime.
Hint: mathematical route
A wide thin-LQ run has an exact sum of actual stage costs, but only an upper bound after the compiler cost is replaced by its polynomial budget; its deterministic factors satisfy the exact same-run LQ identities.
- The one-by-one emit trace refutes exact equality with upper budgets; the three materialization costs are exact at their output dimensions.
- The exact stage sum uses the actual compiler cost on the actual stored transpose; replacing only that term by its universal budget yields the componentwise wide bound.
- The same run's factors satisfy A=R*Q and Q*Q-transpose=I_m by recovery, prefix restriction and orthogonality, without a rank or nonempty-dimension assumption.
Reference solution
The asserted equality with the polynomial budget is false. At m=n=1, take the stored zero matrix. The sole compiler column has no row below its pivot, so its column sweep emits no elimination record. Identity materialization and replay of the empty log emit nothing, as do the transpose and the two extractions. The actual wide emit counter is therefore zero. But P(1,1).emit=1 and all three E terms have emit counter zero. Thus the proposed budget equality would say 0=1. This witness concerns the actual fixed compiler, not a lower bound for optimal elimination.
Sequential Run.bind adds the costs of the actual executed stages. The transpose has exact cost E(n,m), and the extractions have exact costs E(m,m) and E(m,n), independent of their input values. Consequently cost(wide(A))=E(n,m)+C(At)+E(m,m)+E(m,n). The compiler's universal componentwise bound applies to this actual At, yielding cost(wide(A)) <= E(n,m)+P(n,m)+E(m,m)+E(m,n). Replacing the single actual compiler cost by an upper bound gives an inequality, not another exact identity. Materialization charges still apply to empty rows: E(N,0) includes the row surcharge. An empty compiler log still pays its end-marker read. None of these charges is an emit.
For correctness, let B be the residual and T the orthogonal transform returned by the compilation of At. Their denotations satisfy B=T*A-transpose, T-transpose*B=A-transpose and T-transpose*T=I_n. Transposing the recovery equation gives A=B-transpose*T. The residual satisfies B(k,i)=0 whenever i<k. Since every i is below m, all terms with k at least m vanish in each entry of B-transpose*T. Restricting that finite sum to the first m indices gives R(i,k)=B(k,i), Q(k,j)=T(k,j) and A=R*Q, exactly the two stored extractions. Because T is square and orthogonal, T*T-transpose=I_n as well; restricting its row indices to the first m rows gives Q*Q-transpose=I_m. No full-row-rank assumption was used: these are the deterministic stored factors even for zero or repeated rows. For m=0 the sums and I_m are empty, so the same statements hold; when n=0 the wide premise forces m=0. The library's wide_R/wide_Q and constructive wide_factorization/wide_orthogonal refinements establish precisely this same-run identity.
The all-shape compile dispatcher additionally charges one dimension comparison. That charge is not part of wide(A). These are counts in the extended exact-real stored-word model, including materialization and log operations, not finite-precision runtime, numerical stability or a gate-optimality theorem. This answer is a source-grounded mathematical reconstruction, not an admitted native Lean view or a new kernel certificate for all of the prose.
Assessment rubric
- Refutes literal equality with upper budgets using the actual one-by-one emit trace (zero actual versus polynomial budget one), and gives the exact four-stage additive identity with C(At), not P, in the compiler slot. (1 weight)
- Substitutes the universal compiler inequality to obtain the componentwise wide bound with correct dimensions. Distinguishes exact materialization charges, empty-row/end-marker costs, dispatcher comparison and non-finite-bit scope. (1 weight)
- Derives same-run A=R*Q from transpose recovery and zero-below-diagonal prefix restriction, and Q*Q-transpose=I_m from the rows of the orthogonal transform. Handles rank-deficient and empty cases without adding hypotheses. (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/StoredThinLQ.lean
extractionBudget40-41; transpose_cost43-46; wide74-80; wide_correct94-98; wideBudget100-102; wide_cost_le104-109
Source SHA-256:ed08ef278a93268f7d9620cb2ddafc2e3468fcc4f2543923251a3ce4e057177a· MIT (repository LICENSE)
Contract: 71cdeee685c80bfaba5f6895b54c3e5fc3324c65eaeb05e57f48a1e1f05eace1
Item digest: 231e45a37b252d45aad91303bf97480068815b58052c8fbd0bbdaf6322d3a62b
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.
Question revision lineage
{ "question_version": 2, "predecessor_key": "qcb-core-la-206", "predecessor_item_digest": "570ef6e2369350a88e413eebd4a96a3608685517dc5e1d1f6b7a08e741cd77ba", "predecessor_contract_hash": "b35892d85ffaca3d7e12c9966621cc1109c0d747aca52bdd96a54e846fdf89f1", "current_contract_hash": "71cdeee685c80bfaba5f6895b54c3e5fc3324c65eaeb05e57f48a1e1f05eace1", "changed_contract_fields": [ "question" ], "repair_record": "shared/repairs/la-206-cost-contract-successor.json", "repair_record_digest": "36db0e160d48b66509b15c1657d14312495b9be11d08eb942af40f5971e7314e", "review_record": "reports/textbook-v1/repairs/la-206-cost-contract-successor-review.json", "review_digest": "5a2056b8e9acf0f08d4f19ec9b7a3c7cedf96b8154114f3173a4560688f4a908", "equivalence_to_predecessor_claimed": false, "additional_core_count": 0 }