This definition gives the library's named construction or computation for “rotate rows”.
noncomputable def rotateRows {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ)
(i j : Fin N) (theta : ℝ) : _root_.Matrix (Fin N) (Fin M) ℝ :=
fun row col =>
if row = i then Real.cos (theta / 2) * A i col - Real.sin (theta / 2) * A j col
else if row = j then Real.sin (theta / 2) * A i col + Real.cos (theta / 2) * A j col
else A row col
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “plane matrix”.
noncomputable def planeMatrix {N : ℕ} (i j : Fin N) (theta : ℝ) :
_root_.Matrix (Fin N) (Fin N) ℝ := rotateRows 1 i j theta
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “plane matrix mul”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem planeMatrix_mul {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ)
(i j : Fin N) (theta : ℝ) : planeMatrix i j theta * A = rotateRows A i j theta := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “rotate rows inverse”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem rotateRows_inverse {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ)
(i j : Fin N) (distinct : i ≠ j) (theta : ℝ) :
rotateRows (rotateRows A i j theta) i j (-theta) = A := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “plane matrix inverse”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem planeMatrix_inverse {N : ℕ} (i j : Fin N) (distinct : i ≠ j) (theta : ℝ) :
planeMatrix i j (-theta) * planeMatrix i j theta = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “plane matrix transpose”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem planeMatrix_transpose {N : ℕ} (i j : Fin N) (distinct : i ≠ j) (theta : ℝ) :
(planeMatrix i j theta).transpose = planeMatrix i j (-theta) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “plane matrix orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem planeMatrix_orthogonal {N : ℕ} (i j : Fin N) (distinct : i ≠ j) (theta : ℝ) :
(planeMatrix i j theta).transpose * planeMatrix i j theta = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “rotate rows preserves orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem rotateRows_preserves_orthogonal {N : ℕ} (A : _root_.Matrix (Fin N) (Fin N) ℝ)
(orthogonal : A.transpose * A = 1) (i j : Fin N) (distinct : i ≠ j) (theta : ℝ) :
(rotateRows A i j theta).transpose * rotateRows A i j theta = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “split angle real first column”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem splitAngle_real_firstColumn (x y : ℝ) :
Real.cos ((splitAngle x y).eval / 2) * pairNorm x y = x ∧
Real.sin ((splitAngle x y).eval / 2) * pairNorm x y = y := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “elimination angle”.
noncomputable def eliminationAngle (x y : ℝ) : ℝ := -(splitAngle x y).eval
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “elimination angle zero”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem eliminationAngle_zero : eliminationAngle 0 0 = 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eliminate pair”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem eliminate_pair (x y : ℝ) :
Real.cos (eliminationAngle x y / 2) * x -
Real.sin (eliminationAngle x y / 2) * y = pairNorm x y ∧
Real.sin (eliminationAngle x y / 2) * x +
Real.cos (eliminationAngle x y / 2) * y = 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “pair norm eq zero iff”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem pairNorm_eq_zero_iff (x y : ℝ) : pairNorm x y = 0 ↔ x = 0 ∧ y = 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “pair norm pos of nonzero”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem pairNorm_pos_of_nonzero (x y : ℝ) (nonzero : x ≠ 0 ∨ y ≠ 0) :
0 < pairNorm x y := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “eliminate entry”.
noncomputable def eliminateEntry {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ)
(i j : Fin N) (col : Fin M) : _root_.Matrix (Fin N) (Fin M) ℝ :=
rotateRows A i j (eliminationAngle (A i col) (A j col))
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eliminate entry pivot”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem eliminateEntry_pivot {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ)
(i j : Fin N) (distinct : i ≠ j) (col : Fin M) :
eliminateEntry A i j col i col = pairNorm (A i col) (A j col) ∧
eliminateEntry A i j col j col = 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eliminate entry unchanged”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem eliminateEntry_unchanged {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ)
(i j row : Fin N) (col otherCol : Fin M) (hi : row ≠ i) (hj : row ≠ j) :
eliminateEntry A i j col row otherCol = A row otherCol := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eliminate entry preserves zero column”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem eliminateEntry_preserves_zero_column {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ)
(i j : Fin N) (col oldCol : Fin M) (hi : A i oldCol = 0) (hj : A j oldCol = 0)
(row : Fin N) : eliminateEntry A i j col row oldCol = A row oldCol := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eliminate entry preserves orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem eliminateEntry_preserves_orthogonal {N : ℕ} (A : _root_.Matrix (Fin N) (Fin N) ℝ)
(orthogonal : A.transpose * A = 1) (i j : Fin N) (distinct : i ≠ j) (col : Fin N) :
(eliminateEntry A i j col).transpose * eliminateEntry A i j col = 1 :=
rotateRows_preserves_orthogonal A orthogonal i j distinct _
/-- A zero pair produces an actual identity step, without division by zero. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eliminate entry zero pair”; the hypotheses and conclusion in the code panel fix its exact scope. A zero pair produces an actual identity step, without division by zero.
theorem eliminateEntry_zero_pair {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ)
(i j : Fin N) (col : Fin M) (firstZero : A i col = 0) (secondZero : A j col = 0) :
eliminateEntry A i j col = A := by
commit-pinned source · Verso Blueprint panel
This record groups the data and proof fields needed for “step”. A proposition-valued field is a requirement until a constructor supplies it. An actual adjacent-row rotation, carrying the precise ordered support.
structure Step (N : ℕ) where
first : Fin N
second : Fin N
adjacent : first.val + 1 = second.val
angle : ℝ
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “distinct”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem Step.distinct {N : ℕ} (step : Step N) : step.first ≠ step.second := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “matrix”.
noncomputable def Step.matrix {N : ℕ} (step : Step N) :
_root_.Matrix (Fin N) (Fin N) ℝ := planeMatrix step.first step.second step.angle
/-- Chronological action: the first listed matrix acts first. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “apply steps”. Chronological action: the first listed matrix acts first.
noncomputable def applySteps {N M : ℕ} : List (Step N) →
_root_.Matrix (Fin N) (Fin M) ℝ → _root_.Matrix (Fin N) (Fin M) ℝ
| [], A => A
| step :: rest, A => applySteps rest (step.matrix * A)
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “inverse”.
noncomputable def Step.inverse {N : ℕ} (step : Step N) : Step N :=
{ step with angle := -step.angle }
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “apply steps append”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem applySteps_append {N M : ℕ} (left right : List (Step N))
(A : _root_.Matrix (Fin N) (Fin M) ℝ) :
applySteps (left ++ right) A = applySteps right (applySteps left A) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “apply steps reverse inverse”; the hypotheses and conclusion in the code panel fix its exact scope. Reversing the chronological list and negating every angle exactly undoes it.
theorem applySteps_reverse_inverse {N M : ℕ} (steps : List (Step N))
(A : _root_.Matrix (Fin N) (Fin M) ℝ) :
applySteps (steps.reverse.map Step.inverse) (applySteps steps A) = A := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “column sweep”.
noncomputable def columnSweep {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ)
(col : Fin M) (lo : ℕ) : (count : ℕ) → lo + count < N →
_root_.Matrix (Fin N) (Fin M) ℝ
| 0, _ => A
| count + 1, bound =>
columnSweep (eliminateEntry A ⟨lo + count, by omega⟩
⟨lo + count + 1, by omega⟩ col) col lo count (by omega)
/-- The list is computed from the changing matrix, not supplied as a certificate. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “column sweep steps”. The list is computed from the changing matrix, not supplied as a certificate.
noncomputable def columnSweepSteps {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ)
(col : Fin M) (lo : ℕ) : (count : ℕ) → lo + count < N → List (Step N)
| 0, _ => []
| count + 1, bound =>
let first : Fin N := ⟨lo + count, by omega⟩
let second : Fin N := ⟨lo + count + 1, by omega⟩
{ first := first, second := second, adjacent := rfl,
angle := eliminationAngle (A first col) (A second col) } ::
columnSweepSteps (eliminateEntry A first second col) col lo count (by omega)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “column sweep steps length”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem columnSweepSteps_length {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ)
(col : Fin M) (lo count : ℕ) (bound : lo + count < N) :
(columnSweepSteps A col lo count bound).length = count := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “column sweep steps action”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem columnSweepSteps_action {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ)
(col : Fin M) (lo count : ℕ) (bound : lo + count < N) :
applySteps (columnSweepSteps A col lo count bound) A = columnSweep A col lo count bound := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “column sweep exact recovery”; the hypotheses and conclusion in the code panel fix its exact scope. The original matrix is recovered from the computed residual.
theorem columnSweep_exact_recovery {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ)
(col : Fin M) (lo count : ℕ) (bound : lo + count < N) :
applySteps ((columnSweepSteps A col lo count bound).reverse.map Step.inverse)
(columnSweep A col lo count bound) = A := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “column sweep outside”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem columnSweep_outside {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ)
(col : Fin M) (lo count : ℕ) (bound : lo + count < N)
(row : Fin N) (otherCol : Fin M) (outside : row.val < lo ∨ lo + count < row.val) :
columnSweep A col lo count bound row otherCol = A row otherCol := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “column sweep zeroed”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem columnSweep_zeroed {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ)
(col : Fin M) (lo count : ℕ) (bound : lo + count < N)
(row : Fin N) (lower : lo < row.val) (upper : row.val ≤ lo + count) :
columnSweep A col lo count bound row col = 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “column sweep preserves zero column”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem columnSweep_preserves_zero_column {N M : ℕ}
(A : _root_.Matrix (Fin N) (Fin M) ℝ) (col oldCol : Fin M)
(lo count : ℕ) (bound : lo + count < N)
(zeros : ∀ row : Fin N, lo ≤ row.val → row.val ≤ lo + count → A row oldCol = 0)
(row : Fin N) : columnSweep A col lo count bound row oldCol = A row oldCol := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “column sweep preserves orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem columnSweep_preserves_orthogonal {N : ℕ}
(A : _root_.Matrix (Fin N) (Fin N) ℝ) (orthogonal : A.transpose * A = 1)
(col : Fin N) (lo count : ℕ) (bound : lo + count < N) :
(columnSweep A col lo count bound).transpose * columnSweep A col lo count bound = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “det two row mix”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem det_two_row_mix {N : ℕ} (A : _root_.Matrix (Fin N) (Fin N) ℝ)
(i j : Fin N) (distinct : i ≠ j) (a b c d : ℝ) :
(((A.updateRow i (a • A i + b • A j)).updateRow j (c • A i + d • A j))).det =
(a * d - b * c) * A.det := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “rotate rows det”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem rotateRows_det {N : ℕ} (A : _root_.Matrix (Fin N) (Fin N) ℝ)
(i j : Fin N) (distinct : i ≠ j) (theta : ℝ) :
(rotateRows A i j theta).det = A.det := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “plane matrix det”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem planeMatrix_det {N : ℕ} (i j : Fin N) (distinct : i ≠ j) (theta : ℝ) :
(planeMatrix i j theta).det = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “column sweep preserves det”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem columnSweep_preserves_det {N : ℕ}
(A : _root_.Matrix (Fin N) (Fin N) ℝ) (col : Fin N)
(lo count : ℕ) (bound : lo + count < N) :
(columnSweep A col lo count bound).det = A.det := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “prefix identity”.
def PrefixIdentity {N : ℕ} (A : _root_.Matrix (Fin N) (Fin N) ℝ) (k : ℕ) : Prop :=
∀ col : Fin N, col.val < k → ∀ row : Fin N, A row col = if row = col then 1 else 0
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “orthogonal zero of fixed column”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem orthogonal_zero_of_fixed_column {N : ℕ} (A : _root_.Matrix (Fin N) (Fin N) ℝ)
(orthogonal : A.transpose * A = 1) (old col : Fin N) (distinct : old ≠ col)
(fixed : ∀ row : Fin N, A row old = if row = old then 1 else 0) : A old col = 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “column sweep prefix”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem columnSweep_prefix {N : ℕ} (A : _root_.Matrix (Fin N) (Fin N) ℝ)
(col : Fin N) (count : ℕ) (bound : col.val + count < N)
(fixedPrefix : PrefixIdentity A col.val) : PrefixIdentity (columnSweep A col col.val count bound) col.val := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “column sweep pivot nonneg”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem columnSweep_pivot_nonneg {N M : ℕ} (A : _root_.Matrix (Fin N) (Fin M) ℝ)
(col : Fin M) (lo count : ℕ) (bound : lo + count < N) (positive : 0 < count) :
0 ≤ columnSweep A col lo count bound ⟨lo, by omega⟩ col := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “orthogonal supported column sq”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem orthogonal_supported_column_sq {N : ℕ} (A : _root_.Matrix (Fin N) (Fin N) ℝ)
(orthogonal : A.transpose * A = 1) (col : Fin N)
(support : ∀ row : Fin N, row ≠ col → A row col = 0) : A col col ^ 2 = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “column sweep prefix succ”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem columnSweep_prefix_succ {N : ℕ} (A : _root_.Matrix (Fin N) (Fin N) ℝ)
(orthogonal : A.transpose * A = 1) (col : Fin N) (count : ℕ)
(dimension : col.val + count + 1 = N) (positive : 0 < count)
(fixedPrefix : PrefixIdentity A col.val) :
PrefixIdentity (columnSweep A col col.val count (by omega)) (col.val + 1) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “matrix eq one of full prefix”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem matrix_eq_one_of_full_prefix {N : ℕ} (A : _root_.Matrix (Fin N) (Fin N) ℝ)
(fixedPrefix : PrefixIdentity A N) : A = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “matrix eq one of last prefix”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem matrix_eq_one_of_last_prefix {N : ℕ} (A : _root_.Matrix (Fin N) (Fin N) ℝ)
(orthogonal : A.transpose * A = 1) (determinant : A.det = 1)
(k : ℕ) (dimension : k + 1 = N) (fixedPrefix : PrefixIdentity A k) : A = 1 := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “full sweep”.
noncomputable def fullSweep {N : ℕ} (A : _root_.Matrix (Fin N) (Fin N) ℝ)
(k : ℕ) : (remaining : ℕ) → k + remaining = N → _root_.Matrix (Fin N) (Fin N) ℝ
| 0, _ => A
| 1, _ => A
| remaining + 2, dimension =>
fullSweep (columnSweep A ⟨k, by omega⟩ k (remaining + 1) (by omega))
(k + 1) (remaining + 1) (by omega)
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “full sweep steps”.
noncomputable def fullSweepSteps {N : ℕ} (A : _root_.Matrix (Fin N) (Fin N) ℝ)
(k : ℕ) : (remaining : ℕ) → k + remaining = N → List (Step N)
| 0, _ => []
| 1, _ => []
| remaining + 2, dimension =>
columnSweepSteps A ⟨k, by omega⟩ k (remaining + 1) (by omega) ++
fullSweepSteps (columnSweep A ⟨k, by omega⟩ k (remaining + 1) (by omega))
(k + 1) (remaining + 1) (by omega)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “full sweep steps action”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem fullSweepSteps_action {N : ℕ} (A : _root_.Matrix (Fin N) (Fin N) ℝ)
(k remaining : ℕ) (dimension : k + remaining = N) :
applySteps (fullSweepSteps A k remaining dimension) A = fullSweep A k remaining dimension := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “full sweep steps length twice”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem fullSweepSteps_length_twice {N : ℕ} (A : _root_.Matrix (Fin N) (Fin N) ℝ)
(k remaining : ℕ) (dimension : k + remaining = N) :
(fullSweepSteps A k remaining dimension).length * 2 = remaining * (remaining - 1) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “full sweep steps length”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem fullSweepSteps_length {N : ℕ} (A : _root_.Matrix (Fin N) (Fin N) ℝ)
(k remaining : ℕ) (dimension : k + remaining = N) :
(fullSweepSteps A k remaining dimension).length = remaining * (remaining - 1) / 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “full sweep eq one”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem fullSweep_eq_one {N : ℕ} (A : _root_.Matrix (Fin N) (Fin N) ℝ)
(orthogonal : A.transpose * A = 1) (determinant : A.det = 1)
(k remaining : ℕ) (dimension : k + remaining = N) (fixedPrefix : PrefixIdentity A k) :
fullSweep A k remaining dimension = 1 := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “decompose so”. A computed finite list of adjacent RY planes in chronological circuit order.
noncomputable def decomposeSO {N : ℕ} (A : _root_.Matrix (Fin N) (Fin N) ℝ) : List (Step N) :=
(fullSweepSteps A 0 N (by omega)).reverse.map Step.inverse
/-- Every real determinant-one orthogonal matrix is exactly the action of the
constructed adjacent-plane list. The final identity is proved, not supplied. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “decompose so action”; the hypotheses and conclusion in the code panel fix its exact scope. Every real determinant-one orthogonal matrix is exactly the action of the constructed adjacent-plane list.
theorem decomposeSO_action {N : ℕ} (A : _root_.Matrix (Fin N) (Fin N) ℝ)
(orthogonal : A.transpose * A = 1) (determinant : A.det = 1) :
applySteps (decomposeSO A) 1 = A := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “decompose so length”; the hypotheses and conclusion in the code panel fix its exact scope. Including harmless identity rotations at zero pivots gives an exact count.
theorem decomposeSO_length {N : ℕ} (A : _root_.Matrix (Fin N) (Fin N) ℝ) :
(decomposeSO A).length = N * (N - 1) / 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “plane matrix selected entry”; the hypotheses and conclusion in the code panel fix its exact scope. The ordered two-dimensional block uses exactly the selected-RY convention.
theorem planeMatrix_selected_entry {N : ℕ} (i j : Fin N) (distinct : i ≠ j)
(theta : ℝ) (rowBit colBit : Fin 2) :
planeMatrix i j theta (if rowBit = 0 then i else j) (if colBit = 0 then i else j) =
realRyPlaneBlock theta rowBit colBit := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “plane matrix fixed column”; the hypotheses and conclusion in the code panel fix its exact scope. Every basis vector outside the selected pair is fixed, including its sign.
theorem planeMatrix_fixed_column {N : ℕ} (i j col : Fin N) (theta : ℝ)
(outsideFirst : col ≠ i) (outsideSecond : col ≠ j) (row : Fin N) :
planeMatrix i j theta row col = (1 : _root_.Matrix (Fin N) (Fin N) ℝ) row col := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “steps matrix”. Chronological matrix product, matching the circuit list convention.
noncomputable def stepsMatrix {N : ℕ} : List (Step N) → _root_.Matrix (Fin N) (Fin N) ℝ
| [] => 1
| step :: rest => stepsMatrix rest * step.matrix
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “apply steps eq matrix mul”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem applySteps_eq_matrix_mul {N M : ℕ} (steps : List (Step N))
(A : _root_.Matrix (Fin N) (Fin M) ℝ) : applySteps steps A = stepsMatrix steps * A := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “decompose so matrix”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem decomposeSO_matrix {N : ℕ} (A : _root_.Matrix (Fin N) (Fin N) ℝ)
(orthogonal : A.transpose * A = 1) (determinant : A.det = 1) :
stepsMatrix (decomposeSO A) = A := by
commit-pinned source · Verso Blueprint panel