Lean checks the proposition indexed as “exists orthogonal completion”; the hypotheses and conclusion in the code panel fix its exact scope. An arbitrary injection specifies the physical positions of the active columns, so no assumption that they form a prefix is needed.
theorem exists_orthogonal_completion {N r : ℕ}
(V : _root_.Matrix (Fin N) (Fin r) ℝ) (e : Fin r ↪ Fin N)
(hV : V.transpose * V = 1) :
∃ U : _root_.Matrix (Fin N) (Fin N) ℝ,
U.transpose * U = 1 ∧ ∀ i a, U i (e a) = V i a := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “sign flip”. Change the sign of one chosen column; every other column is unchanged.
def signFlip {N : ℕ} (j : Fin N) : _root_.Matrix (Fin N) (Fin N) ℝ :=
_root_.Matrix.diagonal (fun i => if i = j then -1 else 1)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “sign flip orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem signFlip_orthogonal {N : ℕ} (j : Fin N) :
(signFlip j).transpose * signFlip j = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “sign flip det”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem signFlip_det {N : ℕ} (j : Fin N) : (signFlip j).det = -1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “mul sign flip preserves”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem mul_signFlip_preserves {N : ℕ} (U : _root_.Matrix (Fin N) (Fin N) ℝ)
(j i a : Fin N) (ha : a ≠ j) : (U * signFlip j) i a = U i a := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “exists special orthogonal completion of unused”; the hypotheses and conclusion in the code panel fix its exact scope. Correct a negative determinant using a known unused column.
theorem exists_specialOrthogonal_completion_of_unused {N r : ℕ}
(V : _root_.Matrix (Fin N) (Fin r) ℝ) (e : Fin r ↪ Fin N)
(hV : V.transpose * V = 1) (unused : Fin N) (hu : ∀ a, e a ≠ unused) :
∃ U : _root_.Matrix (Fin N) (Fin N) ℝ,
U.transpose * U = 1 ∧ U.det = 1 ∧ ∀ i a, U i (e a) = V i a := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “exists special orthogonal completion”; the hypotheses and conclusion in the code panel fix its exact scope. A strict active-dimension bound guarantees a spare orientation column.
theorem exists_specialOrthogonal_completion {N r : ℕ} (hr : r < N)
(V : _root_.Matrix (Fin N) (Fin r) ℝ) (e : Fin r ↪ Fin N)
(hV : V.transpose * V = 1) :
∃ U : _root_.Matrix (Fin N) (Fin N) ℝ,
U.transpose * U = 1 ∧ U.det = 1 ∧ ∀ i a, U i (e a) = V i a := by
commit-pinned source · Verso Blueprint panel