Matrix Constructions
Exercise LA-112
local source supported. Additive answer successor with distinct content-bound review; historical rejected answer retained only for audit. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- Finite real NxM matrix; columns processed in order with a bottom-up adjacent sweep
- A pivot row exists only when the column index is below the row count
- Upper-prefix at index k: each processed column c<k is zero strictly below row c
- Original derivation from inspected local source; no fresh Lean verification
Question
A rectangular NxM real matrix is reduced column by column: at column k, if a pivot row exists, a bottom-up adjacent sweep clears that column below the diagonal. Say a matrix has the upper-prefix property at index k when, for every already-processed column c < k, every entry strictly below row c in column c is zero. Prove that processing one more column advances this staircase property from index k to k+1, and hence that after processing all M columns the residual is upper-trapezoidal (entry at row r, column c is zero whenever c < r).
Hint: mathematical route
The strict upper-prefix invariant survives because the next sweep touches rows r>=k, all strictly below every earlier column c<k. No old diagonal entry is assumed zero; skipped pivots and empty dimensions are vacuous.
- For an existing pivot k<N, the actual bottom-up sweep zeros fresh column k only strictly below its diagonal.
- Earlier c<k has zero entries throughout the later swept window r>=k>c; zero-column preservation and unchanged outside rows retain the old invariant without zeroing A[c,c].
- Fresh zeroing and old-column preservation give UpperPrefix(k+1); when k>=N the fresh clause is vacuous and the skipped sweep also advances it.
- Induction from the vacuous index0 gives UpperPrefix(M), hence all entries with c<r vanish, including empty row/column boundaries.
Reference solution
Assume UpperPrefix(A,k): for every earlier column c<k, A[r,c]=0 whenever c<r. This is a STRICT-below-diagonal condition, not a claim that A[c,c]=0. For exampleI_2 has UpperPrefix at k=1 while A[0,0]=1; a proof demanding that diagonal zero would be false.
For k<M and k<N, the actual sweep acts only on the row window k,...,N-1, bottom-up. Fresh column k is zero at every row r>k after columnSweep_zeroed. For an old column c<k, EVERY row r in the swept window satisfies r>=k>c. Consequently all entries of old column c in that window are zero by the prefix hypothesis. Each two-row rotation combines two zero entries of that old column into two zeros, while rows outside the window are unchanged. Equivalently columnSweep_preserves_zero_column applies with lo=k and count=N-1-k. Thus old entries retain their previous values everywhere and in particular retain their required below-diagonal zeros; the old diagonal row c is outside the swept window and need not be zero. Combining old columns with fresh column k gives UpperPrefix at k+1.
If k>=N, no pivot row exists and the actual procedure skips the sweep. Every old c<k remains covered. The only newly included column c=k has no row r>k in Fin N, so its required clause is vacuous. Hence the same one-index advance holds without a hidden k<N assumption on all processed columns.
Now induct on the number of remaining columns, starting with the vacuous UpperPrefix(A,0). Each processed or skipped column advances the index by one. After M columns UpperPrefix(reduced(A),M) holds. For any actual column c in Fin M, c<M; if c<r, the invariant gives reduced(A)[r,c]=0. This is the claimed upper-trapezoidal residual. N=0 or M=0 is harmless: there are no rows/columns witnessing a forbidden entry and the empty/skipping recursions preserve the vacuous invariant. No nonzero pivot, full rank, diagonal normalization, cost or numerical stability premise was needed.
Assessment rubric
- Show the freshly swept column is zero below its diagonal (1 weight)
- Show earlier columns' below-diagonal zeros are preserved by the new sweep (1 weight)
- Induct from the vacuous index 0 to full upper-trapezoidal residual at index M (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/RectangularGivens.lean
UpperPrefix49-50; columnSweep_upperPrefix52-65; sweep_upperPrefix67-83; reduced_zero_below135-139
Source SHA-256:8066d811985b60d5f30eeb6cef50c516a00d9f8b95182a2d541c7c9eb35fa133· MIT (repository LICENSE) - QuantumBlockEncoding/AdjacentGivens.lean
columnSweep_preserves_zero_column305-323
Source SHA-256:a43c3b4f543738cb317be01fa664fd466bfa28e21c33d10c7a90e74037a58d9c· MIT (repository LICENSE)
Contract: 77c102094d16f2fe997c42dfd3e75fcf661263f56d7065fd074fbd91556f1014
Item digest: 8fe4711d0fe3aae0b3f3039da4682956ee94ca6aac9b5ef4def2245b91cd7dfd
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 4. This is not measured graph distance or model difficulty.
Answer revision lineage
{ "predecessor_item_digest": "5a3312d25c43d37773774a1db3e7a6d4ef238bc017da1b184a887dc2db33e54e", "predecessor_key": "qcb-core-la-112", "repair_record": "shared/repairs/la-112-strict-prefix-window-repair.json", "repair_record_digest": "fc6f47406babdf7ca0cf529d9cca366ccdef61d3ea18e9dbfabbdd02d6b346ad", "review_record": "reports/textbook-v1/repairs/la-112-strict-prefix-window-repair-review.json", "review_digest": "6eebebd7b967596ef21cef4100d1ae4abcfac61ff0c0bd1af337d8e01b367dba" }