Matrix Constructions
Exercise LA-103
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 matrices; each step acts on a distinct ordered row pair
- Chronological application: the first listed rotation acts first
- RY half-angle convention; the inverse rotation negates the angle
- Undo list is the reversed list with every angle negated
- Original derivation from inspected local source; no fresh Lean verification
Question
A sequence of plane rotations is applied to a matrix in chronological order (the first listed rotation acts first). Prove that reversing the list and negating every rotation angle undoes the whole sequence exactly, returning the original matrix.
Hint: mathematical route
Reversing a chronological list of plane rotations and negating every angle exactly inverts the sequence, by a single-step inverse law plus list induction.
- Establish the two-row inverse law plane(-t)*plane(t)=1 via cos^2+sin^2=1.
- Rewrite the reversed-negated undo of (step::rest) as undo-rest then undo-step.
- Apply the induction hypothesis to cancel rest.
- Apply the single-step inverse law to cancel the leading step and recover the matrix.
Reference solution
First, a single plane rotation by angle t followed by the plane rotation on the same ordered pair by -t is the identity: on the chosen two rows the composed linear map has matrix [[cos,-sin],[sin,cos]] times [[cos,sin],[-sin,cos]], which equals the identity because cos^2+sin^2=1 and the cross terms cancel; all other rows are untouched. This gives the single-step inverse law. Now argue by induction on the applied list. For the empty list there is nothing to undo. For a list (step :: rest), applying it means first acting by step then by rest; the proposed undo is (reverse rest ++ [step^{-1}]) with every angle negated, i.e. first undo rest then undo step. By the induction hypothesis undoing rest returns the matrix to the state right after step, and then the single-step inverse law removes step, recovering the original matrix. Because each step is distinct on an adjacent ordered pair, the inverse law applies at every stage. The result is an exact recovery statement, not an assertion about numerical conditioning.
Assessment rubric
- Prove the single-step inverse law plane(t) then plane(-t) is identity (1 weight)
- Set up induction on the list with correct reversed/negated undo order (1 weight)
- Combine induction hypothesis and single-step law to recover the matrix (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/AdjacentGivens.lean
planeMatrix_inverse57-60; Step.inverse197-198; applySteps_append200-205; applySteps_reverse_inverse207-220
Source SHA-256:a43c3b4f543738cb317be01fa664fd466bfa28e21c33d10c7a90e74037a58d9c· MIT (repository LICENSE)
Contract: c0db7e415e110fec88211f2fa4e978ca8df963e9be0e3083d8406bb57540744e
Item digest: 169363b29832bc0b484a2c0a455b9b07a8fce233631ec20ffbd7868be52abb66
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 4. This is not measured graph distance or model difficulty.