Matrix Constructions
Exercise LA-106
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 A^T A = I and det A = 1
- First N-1 columns are already the standard identity prefix
- The determinant of a diagonal matrix is the product of its diagonal entries
- Original derivation from inspected local source; no fresh Lean verification
Question
Suppose a real NxN matrix A is orthogonal (A^T A = I), has determinant 1, and its first N-1 columns have already been reduced to the standard identity prefix (column c equals the c-th coordinate vector for every c < N-1 index, where N-1 denotes the last index k with k+1=N). Prove that A must equal the identity matrix. Explain precisely where the determinant hypothesis is used.
Hint: mathematical route
An orthogonal det-1 matrix whose first N-1 columns are the identity prefix must be the identity; the determinant hypothesis pins the final diagonal to +1 rather than a -1 reflection.
- Zero every off-diagonal entry by orthogonality with the fixed coordinate columns.
- Conclude A is diagonal with 1s in the first N-1 positions.
- Compute the determinant as the single remaining diagonal entry.
- Apply det = 1 to force the last diagonal to +1, excluding the -1 reflection.
Reference solution
First show A is diagonal. For any column, if it is one of the fixed early columns it is already a coordinate vector, so its off-diagonal entries vanish. For the single last column, orthogonality against each fixed early column forces its entries in the early rows to be zero: the inner product of the last column with a fixed coordinate column equals that one surviving entry, which must be 0. The remaining possible nonzero off-diagonal entries lie in the last column at the last row region, but the symmetric orthogonality argument eliminates those too, leaving A diagonal. On the diagonal, every early entry is 1 by the prefix hypothesis, so A = diag(1,...,1,A[last,last]). Taking determinants of a diagonal matrix gives the product of diagonal entries, which here is exactly A[last,last]. The determinant hypothesis det A = 1 therefore forces A[last,last] = 1. Without det = 1 the last diagonal could be -1 (a reflection), which is still orthogonal with an identity prefix but is not the identity; the determinant is precisely what selects the +1 orientation. Hence A = I.
Assessment rubric
- Use orthogonality with fixed coordinate columns to force off-diagonal zeros (1 weight)
- Reduce A to a diagonal with 1s except possibly the last entry (1 weight)
- Use det = 1 to pin the last diagonal to +1 and note -1 is the alternative (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
orthogonal_zero_of_fixed_column403-408; matrix_eq_one_of_full_prefix485-488; matrix_eq_one_of_last_prefix490-525
Source SHA-256:a43c3b4f543738cb317be01fa664fd466bfa28e21c33d10c7a90e74037a58d9c· MIT (repository LICENSE)
Contract: baa6f1660a7ee18b2fced7806f2d00f27c529d47aa0e9fd5da16a9ab0cedccec
Item digest: 2e7a6b4d161e7e91748a4d476a0fc00e1f24695c727136037c0478ed59488ad3
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 4. This is not measured graph distance or model difficulty.