Matrix Constructions
Exercise LA-105
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 with B^T B = I
- The named column is supported only on its diagonal row
- Pivots produced by elimination equal a nonnegative pair length
- Original derivation from inspected local source; no fresh Lean verification
Question
Let B have orthonormal columns (B^T B = I) and suppose one column c of B is supported only on its diagonal row, i.e. every entry of column c off that row is zero. Prove that the diagonal entry B[c,c] squares to 1. If in addition the sweep guarantees that this pivot is nonnegative, prove that it equals exactly +1.
Hint: mathematical route
An orthonormal matrix with a column supported only on its diagonal has that pivot squaring to 1; a nonnegative-pivot guarantee pins it to exactly +1.
- Write the diagonal Gram entry as the sum of squared column entries.
- Collapse the sum to the single diagonal term via the support hypothesis.
- Deduce the pivot squares to 1 from orthonormality.
- Combine the square-one condition with the nonnegativity bound to force +1.
Reference solution
The (c,c) entry of B^T B is the inner product of column c with itself, which equals the sum over all rows of B[row,c]^2. By the support hypothesis only the diagonal row survives, so this sum collapses to B[c,c]^2. Orthonormality gives the (c,c) entry of B^T B equal to 1, hence B[c,c]^2 = 1. A real number whose square is 1 is +1 or -1; combined with the sweep guarantee 0 <= B[c,c], the only possibility is +1. The nonnegativity itself comes from the elimination placing the pivot equal to a pair length sqrt(x^2+y^2) >= 0, propagated through the recursion. This settles the pivot sign without any normalization or square-root reciprocal, purely from orthonormality and a sign bound.
Assessment rubric
- Collapse the diagonal Gram entry to a single squared term using support (1 weight)
- Conclude the square equals 1 from orthonormality (1 weight)
- Use the nonnegative-pivot guarantee to pin the value to +1 (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
columnSweep_pivot_nonneg422-439; orthogonal_supported_column_sq441-455; columnSweep_prefix_succ457-483
Source SHA-256:a43c3b4f543738cb317be01fa664fd466bfa28e21c33d10c7a90e74037a58d9c· MIT (repository LICENSE)
Contract: b97d0674b26cda0e00dc6ce39f9f1d40ef7d46dd9fc9f6157a04ef6dc98019bb
Item digest: 059fbedeca9a54a2029f3769ccac4ed3d567bda7d0899acd6cb3cc9cc3fb0c2d
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 4. This is not measured graph distance or model difficulty.