Matrix Constructions
Exercise LA-104
local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- Finite-dimensional real matrix; the swept window stays within the row range
- Each elimination touches only one adjacent ordered row pair
- Bottom-up sweep: lower rows are folded into the next higher row
- RY half-angle convention; a zero pair produces an identity step
- Original derivation from inspected local source; no fresh Lean verification
Question
A column is cleared by a bottom-up sweep: starting from a low index, adjacent rows are rotated upward one pair at a time so that each lower entry is folded into the one above it. Prove that after sweeping the window of rows from lo to lo+count, every entry of that column strictly below the top row lo is zero, while any row lying outside the window (above lo or below lo+count) is left exactly as it was.
Hint: mathematical route
A bottom-up adjacent sweep zeros a column strictly below its top window row while leaving rows outside the window untouched, by a zeroing induction protected by outside-invariance.
- Show one adjacent elimination fixes every row other than the touched pair.
- Propagate this to full outside-invariance of the sweep by induction.
- Zero the current swept entry using the exact pair-elimination identity.
- Use outside-invariance on the smaller window to protect the created zero.
Reference solution
Argue by induction on the number of adjacent eliminations. The outside-invariance is proved first: a single adjacent elimination on the pair (r,r+1) changes only rows r and r+1, so any row whose index is below lo or above lo+count is never one of these pairs across the whole sweep, and its value is unchanged; this is a direct per-step bookkeeping over the recursion. For the zeroing claim, consider a row index v with lo < v <= lo+count. In the inductive step the sweep performs the elimination that folds row v into v-1 (clearing the entry at v) and then recurses on the remaining upper eliminations, which only touch rows at or above v-1 and hence, by outside-invariance for the smaller window, do not disturb the freshly created zero at v. The base pivot pair uses the exact elimination identity, which places 0 in the lower slot. Thus every strictly-below entry ends at 0 while the frame outside the window is untouched. This describes exact-real elimination semantics, not an iteration-count cost.
Assessment rubric
- Prove rows outside the window are unchanged by every step (1 weight)
- Use the pair elimination to zero the swept entry, by induction over the window (1 weight)
- Argue later eliminations do not disturb an already-created zero (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/AdjacentGivens.lean
eliminateEntry_pivot145-149; eliminateEntry_unchanged151-154; columnSweep_outside265-281; columnSweep_zeroed283-303
Source SHA-256:a43c3b4f543738cb317be01fa664fd466bfa28e21c33d10c7a90e74037a58d9c· MIT (repository LICENSE)
Contract: 7ff433908b502627c6e8ebbd3a28a77ecaeca050598226f6927c0e55d7034761
Item digest: d116f4f01eb9ee69ff710e3d88155094fba848cfbe1475bc166d29434e5c98ea
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 4. This is not measured graph distance or model difficulty.