Linear Algebra
Exercise LA-006
local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- an orthogonal completion with the prescribed columns exists
- r < N so at least one column is unused
- real matrices
- SO(N) = orthogonal matrices of determinant +1
- sign flip is a diagonal matrix with a single -1 entry
Question
Suppose r orthonormal real columns are placed at r distinct positions among the N columns of an orthogonal matrix, and suppose r < N so at least one column position is left free. The naive completion to an orthogonal matrix may land in the reflection family (determinant -1) rather than the rotation family (determinant +1). Prove that one can always repair the orientation so the final matrix has determinant exactly +1 while leaving every one of the r prescribed columns completely unchanged. Explain why the strict inequality r < N is exactly what makes the repair possible, and why the repair cannot in general be done when r = N.
Hint: mathematical route
When r < N, prescribed orthonormal columns extend to a determinant-+1 orthogonal matrix by a single sign flip on an unused column, preserving all prescribed columns.
- Orthogonality forces the determinant to be +1 or -1.
- r < N guarantees an unused column position to host the sign flip.
- The single-column sign flip is orthogonal with determinant -1.
- Right-multiplying by the sign flip corrects the determinant to +1 while preserving every prescribed column.
Reference solution
Start from any orthogonal completion U whose prescribed columns are the given vectors. Because U is orthogonal, U-transpose U = I forces det(U)^2 = 1, so det(U) is either +1 or -1. If it is already +1 there is nothing to do. If it is -1, we fix it with a single-column sign flip at an unused position. Since r < N, the r prescribed positions do not exhaust the N columns, so there is at least one position, call it 'unused', that carries no prescribed column. Let S be the diagonal matrix that is the identity except for a -1 in the unused position. S is orthogonal (it is diagonal with entries +/-1, so S-transpose S = I) and det(S) = -1. Replace U by U*S. Then (U S)-transpose (U S) = S-transpose (U-transpose U) S = S-transpose S = I, so U*S is still orthogonal; and det(U S) = det(U) det(S) = (-1)(-1) = +1, so it is now a rotation. Crucially, right-multiplying by this diagonal S only rescales the single unused column by -1 and leaves every other column, in particular all r prescribed columns, exactly as it was. Hence the prescribed data is preserved and the orientation is corrected. The strict inequality r < N is essential because the repair needs a column that is NOT prescribed to absorb the sign flip; if r = N every column is prescribed, flipping any of them would change the required data, and indeed a fully prescribed orthonormal frame with determinant -1 simply cannot be reoriented to +1 without altering a prescribed column, so no determinant-+1 completion that fixes all N columns exists.
Assessment rubric
- Derives det(U) in {+1,-1} from orthogonality (det squared = 1). (1 weight)
- Uses r < N to secure an unused column position and builds the diagonal sign-flip S there. (1 weight)
- Shows U*S stays orthogonal and has determinant +1 (product of determinants). (1 weight)
- Shows right-multiplication by S changes only the unused column, preserving all prescribed columns, and explains the r = N obstruction. (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/RealIsometryCompletion.lean
complete declarations signFlip (lines 62-63), signFlip_orthogonal (lines 65-72), signFlip_det (lines 74-75), mul_signFlip_preserves (lines 77-79), exists_specialOrthogonal_completion_of_unused (lines 83-104), exists_specialOrthogonal_completion (lines 107-121)
Source SHA-256:2a38bfa0dda457b563f5178e20dc2ccbb1281ff7d5f7357e4096a3c29fa2bb5d· MIT (repository LICENSE)
Contract: 4017b4202cfed5756a3a1b8b0fe5fc1a28e958dce97985795b65f6cd7f9d7ca8
Item digest: 4eae07a7fa7dc01f54e03e5d15700d11bec10c23f9368e6d01b5f44fc0d675f6
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 4. This is not measured graph distance or model difficulty.