Matrix Constructions
Exercise LA-108
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 rectangular matrix; the transform is the accumulated rotation product
- Each plane rotation is orthogonal with determinant 1
- Chronological product: the transform left-multiplies the matrix to the residual
- Original derivation from inspected local source; no fresh Lean verification
Question
A rectangular NxM real matrix A is reduced to an upper-trapezoidal residual by accumulating plane rotations into a single orthogonal transform matrix T, so that T*A equals the residual. Prove that T^T times the residual recovers A exactly, and state why T^T is a valid left inverse of T here.
Hint: mathematical route
The accumulated rotation transform is orthogonal with determinant 1, so its transpose times the upper-trapezoidal residual recovers the original rectangular matrix exactly.
- Show the accumulated transform is orthogonal (T^T T = I).
- Record the reduction identity T*A = residual.
- Left-multiply by T^T and collapse T^T T to the identity.
- Note determinant 1 confirms a genuine rotation and exact transpose inverse.
Reference solution
The accumulated transform T is a product of plane rotations, each of which is orthogonal; a product of orthogonal matrices is orthogonal, so T^T T = I. The construction guarantees T*A = residual by chaining the per-step actions (each plane rotation left-multiplies the current matrix, matching the chronological product). Multiplying this identity on the left by T^T gives T^T*(T*A) = T^T*residual. The left side regroups by associativity as (T^T T)*A = I*A = A, using orthogonality. Hence T^T*residual = A, an exact reconstruction. T^T is the valid left inverse precisely because T is orthogonal: no numerical pseudo-inverse or least-squares step is involved; the inverse is the transpose by the orthogonality identity. Furthermore T has determinant 1 since each plane rotation has determinant 1, so T is a genuine rotation, not merely an orthogonal reflection. These are exact matrix identities, not an evaluation-cost claim.
Assessment rubric
- Establish T^T T = I from a product of orthogonal plane rotations (1 weight)
- Left-multiply T*A = residual by T^T and regroup via orthogonality (1 weight)
- Note T has determinant 1 so the transpose is the exact inverse (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/RectangularGivens.lean
transform_mul130-133; transform_orthogonal144-145; transform_det147-148; exact_recovery150-153
Source SHA-256:8066d811985b60d5f30eeb6cef50c516a00d9f8b95182a2d541c7c9eb35fa133· MIT (repository LICENSE)
Contract: 9266d4f17c32ea01631fb147c91067ce8d10902ab5cfe8546b9ba98c021f9c68
Item digest: b49acfec30465319f4637b8b0bc8fb1655146b68a99b8b9d6688fff48ec32fa7
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 4. This is not measured graph distance or model difficulty.