Matrix Constructions
Exercise LA-120
local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- Finite real matrices; each list entry is a plane rotation with its own matrix
- Chronological convention: the first listed rotation acts first
- The accumulated matrix multiplies the list in reverse order (last entry left-most)
- Original derivation from inspected local source; no fresh Lean verification
Question
A list of plane rotations can be applied to a matrix in two ways. The step-by-step action takes the list and the matrix and applies the first listed rotation to the matrix, then the next to the result, and so on. Alternatively one forms a single accumulated matrix from the list (built so that the last listed rotation multiplies on the left-most, i.e. the product is taken in reverse-list order) and multiplies it once against the matrix. Prove that these two procedures agree for every list and every matrix, and explain why the accumulated product must be taken in reverse list order.
Hint: mathematical route
Iterated step-by-step application of a plane-rotation list equals one multiplication by the accumulated matrix taken in reverse list order; the reverse order is forced by first-listed-acts-first.
- Base case: empty list gives the matrix, matching identity accumulation.
- Expand the step-by-step action of a cons list as leading step then rest.
- Apply the induction hypothesis and reassociate to isolate the full accumulated matrix.
- Explain the reverse product order is the unique convention matching first-listed-acts-first.
Reference solution
Induct on the list. For the empty list, the step-by-step action returns the matrix unchanged and the accumulated matrix is the identity, so both give the matrix. For a list (step :: rest) applied to M, the step-by-step action first forms step.matrix * M (applying step) and then applies rest to that, so by the induction hypothesis it equals accMatrix(rest) * (step.matrix * M). Associativity of matrix multiplication rewrites this as (accMatrix(rest) * step.matrix) * M. The accumulated matrix of the whole list is defined as accMatrix(rest) * step.matrix precisely so that the leading step sits on the right of the product; hence (accumulated matrix of the full list) * M, matching the claim. The reverse-list product order is forced by the chronological convention: the first listed rotation acts first on M, so it must be the right-most factor (closest to M), which means later list entries accumulate to its left. Taking the product in forward order would apply the rotations in the wrong temporal sequence and break the agreement. Therefore the two procedures coincide exactly for all lists, with the reverse order being the unique convention consistent with first-listed-acts-first. This is an exact identity about two equal formulations, not a claim about multiplication cost.
Assessment rubric
- Base case: empty list gives the matrix via identity accumulation (1 weight)
- Inductive step uses associativity to peel the leading step onto the right (1 weight)
- Explain reverse product order is forced by first-listed-acts-first (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
Step.matrix188-189; applySteps192-195; stepsMatrix633-635; applySteps_eq_matrix_mul637-642
Source SHA-256:a43c3b4f543738cb317be01fa664fd466bfa28e21c33d10c7a90e74037a58d9c· MIT (repository LICENSE)
Contract: 7dc440d1fe1add6272ca442c9e2287d3f6bb7231c65feca8f1bf5640ef96ab0c
Item digest: 378ddb50eda58d0fe217c02313ba7c13f7550d190ac84862faa25f8e3a1cb315
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 4. This is not measured graph distance or model difficulty.