Stored Cost Refinement
Exercise LA-218
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 dispatcher charges one comparison and branches on m at most n
- The thin inner dimension is the minimum of m and n
- The tall branch runs no elimination; counts are exact-real, not finite-bit
- Original derivation from inspected local source; no fresh Lean verification
Question
A stored thin-LQ dispatcher takes an m-by-n stored matrix and charges one exact comparison to decide the shape. When m is at most n (the wide case) it transposes, runs the full stored rectangular compilation, and extracts both factors. When m exceeds n (the tall case) it does none of that: it returns the input matrix as the triangular factor together with a materialized identity of size n as the orthonormal factor. Explain what the tall branch returns and why it is correct, and compare the cost of the tall branch against the wide branch. In particular, refute the claim that a thin-LQ factorization always performs a sweep of eliminations.
Hint: mathematical route
Boundary: the tall LQ branch (m>n) runs no sweep, returning the input plus an identity at cost one comparison + 5*n*n+4*n, refuting that thin-LQ always eliminates.
- The tall branch returns the input matrix and a materialized identity, charging only a comparison plus the identity cost.
- It is correct because the thin dimension equals the minimum of m and n, giving a trivial orthonormal factor.
- Only the wide branch performs the compilation, refuting the always-sweep claim.
Reference solution
In the tall branch (m greater than n) the dispatcher performs no elimination sweep at all. It returns the original matrix unchanged in the triangular-factor slot and a freshly materialized n-by-n identity in the orthonormal-factor slot, after paying only the one dimension comparison plus the identity materialization. This is correct for the thin shape because the thin inner dimension is the minimum of m and n, which equals n here; pairing the matrix with the identity trivially reproduces the matrix as a product with an orthonormal (identity) factor of the right size, so the factorization identity and the orthonormality condition both hold by construction. The cost contrast is stark: the wide branch pays the transpose, the cubic-order rectangular compilation and two extractions, whereas the tall branch pays only one comparison plus the identity cost 5*n*n + 4*n, with no field, square-root, inverse-cosine, trigonometric or emit work from any elimination. This refutes the claim that thin-LQ always runs a sweep: on tall inputs the admissible route is the trivial dispatch, and the only elimination-bearing path is the wide branch. The boundary between the branches is the exact comparison m at most n; everything is counted in the exact-real model with no finite-bit runtime claim.
Assessment rubric
- Describe the tall branch returning the input and an identity with only a comparison plus identity cost (1 weight)
- Justify correctness via the thin inner dimension being the minimum of m and n (1 weight)
- Refute 'thin-LQ always sweeps' by contrasting tall (no sweep) and wide (full compilation) costs (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
compileBody111-119; compile122-125; compile_correct162-166; compileBudget174-175; compile_cost_le177-187
Source SHA-256:ed08ef278a93268f7d9620cb2ddafc2e3468fcc4f2543923251a3ce4e057177a· MIT (repository LICENSE)
Contract: 559520fa3b96bc5b02648392e4da0e5bba9e5c3861d62dc370186c36eca77e3b
Item digest: 2b9c9d2449bb0b0da1ab69a254c046c2da52c231a4d71d5ef29f1a828508ee72
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.