Linear Algebra
Exercise LA-009
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
- V-transpose * V = I_r (orthonormal columns)
- the placement e is an injection from r labels into N positions
- part (b) additionally assumes r < N
- real matrices and the standard inner product on R^N
- orthonormal family is linearly independent; dimension bounds independent families
Question
Let V be a real N-by-r matrix whose columns are orthonormal, expressed by the identity V-transpose times V equals the r-by-r identity. (a) Prove the dimensional obstruction r <= N. (b) Suppose further that the strict inequality r < N holds and that the r columns are placed at r distinct positions among the N available column positions via an injective assignment from the r column-labels into the N positions. Prove that this assignment cannot be surjective, i.e. at least one of the N positions receives no prescribed column. Make the counting argument explicit and explain how these two facts together guarantee a spare position exists exactly when r < N.
Hint: mathematical route
Orthonormal columns (V-transpose V = I_r) force r <= N by independence; and when r < N an injective placement e : Fin r -> Fin N is non-surjective by card_le_of_surjective, leaving a spare position.
- V-transpose V = I makes the columns an orthonormal, hence linearly independent, family.
- A linearly independent family in R^N has at most N members, so r <= N.
- If the injection e were surjective then N <= r, contradicting r < N, so some position is unused.
Reference solution
(a) The identity V-transpose times V = identity says that for every pair of column labels the inner product of the corresponding columns is 1 when the labels agree and 0 when they differ; that is, the r columns form an orthonormal family in R^N. An orthonormal family is linearly independent: if a linear combination of the columns were zero, taking the inner product with each column in turn (using orthonormality) forces every coefficient to be zero. A linearly independent family in an N-dimensional vector space has at most N members, because its size cannot exceed the dimension. Hence r, the number of columns, satisfies r <= N. This is the isometry dimensional obstruction: an inner-product-preserving (isometric) linear map from R^r into R^N can exist only when r <= N. (b) The placement is an injective function e from the r column-labels into the N positions. Suppose, for contradiction, that e were also surjective. A surjection from a finite set of size r onto a finite set of size N forces the size of the target to be at most the size of the source, i.e. N <= r (a surjection cannot increase cardinality). But we assumed r < N, i.e. N > r, contradicting N <= r. Therefore e is not surjective: there exists at least one position in the N positions that is not in the image of e, i.e. an unused position receiving no prescribed column. Together: part (a) shows orthonormal columns can only exist when r <= N, and part (b) shows that in the strict regime r < N the injective placement always leaves a spare position. When instead r = N, the injection is a bijection and no spare position exists, which is precisely the boundary that distinguishes the two regimes.
Assessment rubric
- Translates V-transpose V = I into orthonormality and derives linear independence of the columns. (1 weight)
- Concludes r <= N because a linearly independent family has size at most the dimension (isometry obstruction). (1 weight)
- Gives the counting contradiction: a surjection Fin r -> Fin N would force N <= r, contradicting r < N, so e is non-surjective. (1 weight)
- Concludes a spare/unused position exists exactly in the strict regime r < N (and not when r = N). (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 declaration exists_specialOrthogonal_completion (lines 107-121), whose body derives non-surjectivity of e from r < N via a finite-cardinality (card_le_of_surjective) contradiction; orthonormality from V-transpose*V = 1 is set up in exists_orthogonal_completion (lines 20-59)
Source SHA-256:2a38bfa0dda457b563f5178e20dc2ccbb1281ff7d5f7357e4096a3c29fa2bb5d· MIT (repository LICENSE)
Contract: 70f6fc38a3ef7adf46d888970c917a21c7ca952710fa868a9045e5072e0bc9bf
Item digest: b31607a7ea2a259a413bb5b7c11780ee9b302542f801bc1ce38ca72cfc3e1311
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.