QuantumComputinglib learn · inspect · formalize
Checked on this commit 4,524 public declarations commit 4e2c5b2c0be5 Build record

Shared mathematical foundations / Linear Algebra

Linear Algebra

Exercise LA-005

intermediate · proof · train

local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.

Assumptions and conventions

  • V has orthonormal columns, i.e. V-transpose * V = I_r
  • the placement of columns is an injection into the N positions
  • real matrices
  • orthogonal matrix means U-transpose * U = I
  • inner-product space R^N has dimension N

Question

You are given r real column vectors in R^N that are orthonormal (each has unit length and distinct ones are orthogonal), presented as the columns of an N-by-r matrix V satisfying V-transpose times V equals the r-by-r identity. You are also given an arbitrary assignment that places these r columns into r distinct column positions among the N columns of a target N-by-N matrix (the positions need not be the first r columns, and need not be contiguous). Prove that there exists an N-by-N real orthogonal matrix U (U-transpose times U equals the N-by-N identity) whose columns at exactly those r prescribed positions are the given vectors. Make explicit each ingredient your argument relies on.

Hint: mathematical route

Prescribed orthonormal columns placed at arbitrary distinct positions via an injection extend to an orthogonal matrix agreeing on those positions.

  1. The identity equation is equivalent to the r columns being an orthonormal family of size r <= N.
  2. An injective placement into distinct positions preserves the orthonormality of the family.
  3. The family extends to an orthonormal basis of R^N because the space dimension equals the number of positions.
  4. The basis assembled as columns gives an orthogonal U agreeing on all prescribed positions.
Reference solution

First, the hypothesis V-transpose times V = identity says exactly that the r columns of V form an orthonormal family of vectors in R^N; in particular the family has r elements and since an orthonormal family is linearly independent, r <= N. Second, the prescribed placement is an injection from the r column-labels into the N positions, so it merely relabels the same r orthonormal vectors at distinct physical positions without changing their inner products; the placed family is therefore still orthonormal. Third, in the N-dimensional inner-product space R^N, any orthonormal family can be extended to an orthonormal basis of the whole space (basis-extension / Gram-Schmidt completion); this produces N - r additional unit vectors orthogonal to each other and to the prescribed ones, filling the N - r unused positions. Fourth, assemble U by taking as its columns these N orthonormal vectors, with the prescribed vectors sitting at their assigned positions and the completion vectors at the remaining positions. Because all N columns are orthonormal, U-transpose times U is the identity, i.e. U is orthogonal, and by construction its columns at the prescribed positions are exactly the given vectors. Hence such a U exists. The essential ingredients are: (i) the equivalence between the identity equation and column-orthonormality, (ii) invariance of orthonormality under an injective relabeling of positions, and (iii) the orthonormal-basis extension theorem in a finite-dimensional inner-product space whose dimension equals the number of positions.

Assessment rubric
  1. Translates V-transpose V = I into orthonormality of the r columns and notes r <= N. (1 weight)
  2. Argues the injective placement preserves orthonormality (relabeling distinct positions keeps inner products). (1 weight)
  3. Invokes orthonormal-basis extension to fill the remaining N - r positions in R^N. (1 weight)
  4. Assembles U, concludes orthogonality from all-columns-orthonormal and that prescribed columns match. (1 weight)

Graph-grounded prerequisites

These are support/source anchors, not an automatically extracted theorem-dependency proof.

Download the shared core registry

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.

Read the Lean track and existing diagnostic warmups

Sources and provenance

Contract: 1e92086e6a6002919a18af74383a4757b2f7918a8d5ae6f7fbc073d667dc448f

Item digest: 9de300e5af170f37dfbbb8e216ddc6a74157f274971779218e9477ade22a8db4

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

Authored support steps: 4. This is not measured graph distance or model difficulty.