Matrix Constructions
Exercise LA-102
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 square matrix; two distinct selected rows
- Determinant is multilinear and alternating in rows
- RY half-angle convention for the rotation coefficients
- A single row transposition contributes sign -1
- Original derivation from inspected local source; no fresh Lean verification
Question
Replacing two distinct rows i and j of a square matrix by the linear mixtures (a*row_i + b*row_j) and (c*row_i + d*row_j) multiplies the determinant by (a*d - b*c). Use this to prove that a plane rotation acting on rows i and j by the half-angle convention leaves the determinant unchanged.
Hint: mathematical route
Mixing two rows by (a,b),(c,d) scales the determinant by a*d-b*c; for a plane rotation this factor is cos^2+sin^2=1, so the determinant is preserved.
- Expand the determinant multilinearly in both replaced rows into four terms.
- Discard the two equal-row terms as zero determinants.
- Evaluate the swap term with sign -1 and collect the factor a*d - b*c.
- Substitute the rotation coefficients to obtain the factor cos^2+sin^2=1.
Reference solution
Expanding the determinant linearly in the two updated rows produces four terms. The two terms that reuse the same original row twice (coefficients a*c on row_i in both slots, and b*d on row_j in both slots) are determinants with two equal rows, hence 0. The surviving cross terms are a*d times the original determinant and b*c times the determinant with rows i and j swapped; the swap introduces one transposition, so its sign is -1 and that determinant equals -det. Collecting gives (a*d)*det + (b*c)*(-det) = (a*d - b*c)*det. For a plane rotation the mixing coefficients are a=cos(t/2), b=-sin(t/2), c=sin(t/2), d=cos(t/2), so a*d - b*c = cos^2(t/2) + sin^2(t/2) = 1. Therefore the rotation preserves the determinant exactly. This is an exact algebraic identity about the determinant, not an arithmetic evaluation cost.
Assessment rubric
- Kill the repeated-row terms via equal-row determinant 0 (1 weight)
- Identify the swap term sign as -1 and assemble a*d - b*c (1 weight)
- Specialize rotation coefficients to get factor cos^2+sin^2=1 (1 weight)
Graph-grounded prerequisites
These are support/source anchors, not an automatically extracted theorem-dependency proof.
Lean view and evidence boundary
Exact formal conclusion: independently decoded and compared with this question, then checked with the fixed reference in Lean. This is a library-lemma application, not a deep proof-search result. The kernel does not certify every sentence of the natural-language explanation.
{
"imports": [
"QuantumBlockEncoding.AdjacentGivens"
],
"target": "∀ {N : ℕ} (A : _root_.Matrix (Fin N) (Fin N) ℝ) (i j : Fin N), i ≠ j → ∀ theta : ℝ, (QuantumBlockEncoding.AdjacentGivens.rotateRows A i j theta).det = A.det"
}Fixed reference proof
by exact QuantumBlockEncoding.AdjacentGivens.rotateRows_detArbitrary real square input matrix and distinct rows; no adjacency, orthogonality or determinant-one input assumption. Half-angle convention is preserved.
Execution class: trusted local reference; not isolated model-output evaluation. The same core, family and split apply to both views.
Source-blind reconstruction, distinct comparison and actual reference receipts: inspect the evidence records.
Sources and provenance
- QuantumBlockEncoding/AdjacentGivens.lean
det_two_row_mix341-365; rotateRows_det367-378; planeMatrix_det381-383
Source SHA-256:a43c3b4f543738cb317be01fa664fd466bfa28e21c33d10c7a90e74037a58d9c· MIT (repository LICENSE)
Contract: 4be120801daf6e4de98794d14d4c0db5f93bcb6924b3c6aae20252167d662f93
Item digest: 470ce4707a5d7cebab5a056b624cf70eb6448b2fdee43c594b57cf19d273943f
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 4. This is not measured graph distance or model difficulty.