Linear Algebra
Exercise LA-011
nl bridge from inspected source. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- prescribed columns are orthonormal
- the conjecture drops the strict inequality and allows prescribed-count = dimension
- real matrices
- determinant +1 means rotation (SO(N)), -1 means reflection
Question
The special-orthogonal completion result guarantees that prescribed orthonormal columns can be extended to a determinant-+1 orthogonal matrix WHENEVER the number of prescribed columns is strictly less than the ambient dimension. A student conjectures the strict inequality is just a technical convenience and that the result still holds when the prescribed columns already fill all the positions (number of prescribed columns equal to the ambient dimension). Give an explicit counterexample disproving the student's conjecture, and identify exactly which step of the strictly-fewer-columns argument has no analogue in the fully-prescribed case.
Hint: mathematical route
The r < N hypothesis in exists_specialOrthogonal_completion is necessary: a fully-prescribed det=-1 orthonormal frame (e.g. diag(1,-1)) has no determinant-+1 completion, since no unused column remains for the sign-flip repair.
- A fully-prescribed orthonormal frame of determinant -1 exists in dimension 2.
- With all columns prescribed the completion is unique and keeps determinant -1, so no SO completion exists.
- The failing step is the sign-flip repair, which requires an unused column guaranteed only by prescribed-count < dimension.
Reference solution
Work in dimension N = 2 with r = 2 prescribed columns, i.e. all columns prescribed. Let the two prescribed orthonormal columns be (1, 0) and (0, -1), placed at positions 1 and 2. They are orthonormal: each has unit length and they are orthogonal, so the matrix V = [[1,0],[0,-1]] satisfies V-transpose V = identity. The only orthogonal matrix whose columns at positions 1 and 2 are exactly these vectors is V itself, because every column is already dictated by the prescription; there is no free column to choose. But det(V) = (1)(-1) - 0 = -1, so V is a reflection, not a rotation, and it is the unique completion. Therefore no determinant-+1 orthogonal matrix has these prescribed columns, disproving the conjecture: the result genuinely fails when the prescribed columns fill all positions. The step with no analogue is the orientation-repair step. In the strictly-fewer-columns argument one selects an UNUSED column position and flips its sign to turn a determinant-(-1) completion into a determinant-(+1) one while leaving all prescribed columns untouched. When every position is prescribed there is no unused column to absorb the sign flip; any sign change or rotation would have to alter a prescribed column, which is forbidden. So the existence of a spare column, guaranteed only by the strict inequality (number of prescribed columns < ambient dimension), is exactly the ingredient that disappears, and with it the determinant-+1 guarantee.
Assessment rubric
- Gives an explicit fully-prescribed orthonormal frame with determinant -1 (e.g. columns (1,0),(0,-1) in dimension 2). (1 weight)
- Argues the completion is forced to be V itself with determinant -1, so no determinant-+1 completion exists. (1 weight)
- Identifies the missing step as the sign-flip orientation repair, which needs an unused column available only when prescribed-count < dimension. (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 exists_specialOrthogonal_completion (lines 107-121) with its strict hypothesis hr : r < N, exists_specialOrthogonal_completion_of_unused (lines 83-104), signFlip_det (lines 74-75)
Source SHA-256:2a38bfa0dda457b563f5178e20dc2ccbb1281ff7d5f7357e4096a3c29fa2bb5d· MIT (repository LICENSE)
Contract: 539674a15b8183e733496b1988822f1e92cd98944e0030f97b601a67854a17ed
Item digest: 71e5ff52e00d5ec5c88b81ae1265a8094d961c43c77f466c3fb32c8b23f7196f
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.