def Formalization.GeometricAlgebra.SubspaceRadical {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (W : Submodule k V) : Submodule k V

The radical of a subspace W for the bilinear form B: the part of W that is orthogonal to all of W.

theorem Formalization.GeometricAlgebra.exists_complement_within {k : Type u_1} [Field k] [Invertible 2] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (p q : Submodule k V) (h : p ≤ q) : ∃ r ≤ q, Disjoint p r ∧ p ⊔ r = q

Given a chain p ≤ q of subspaces in a finite-dimensional space, there exists a complementary subspace r ≤ q to p within q.

theorem Formalization.GeometricAlgebra.restrict_complement_of_radical_nondegenerate {k : Type u_1} [Field k] [Invertible 2] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (B : LinearMap.BilinForm k V) (hBr : B.IsRefl) (W W₁ : Submodule k V) (hW₁_le : W₁ ≤ W) (hDisj : Disjoint (W ⊓ B.orthogonal W) W₁) (hSup : W ⊓ B.orthogonal W ⊔ W₁ = W) : (B.restrict W₁).Nondegenerate

If W₁ is a complement to the radical W ⊓ Wᗮ inside W, then the restriction of B to W₁ is nondegenerate.

def Formalization.GeometricAlgebra.IsHyperbolicPair {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (x y : V) : Prop

A hyperbolic pair for B consists of two isotropic vectors x, y with B x y = 1.

theorem Formalization.GeometricAlgebra.exists_eval_one {k : Type u_1} [Field k] [Invertible 2] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (B : LinearMap.BilinForm k V) (hBnd : B.Nondegenerate) (x : V) (hx_ne : x ≠ 0) : ∃ (z : V), (B x) z = 1

For a nondegenerate bilinear form B, every nonzero vector x has some z with B x z = 1.

theorem Formalization.GeometricAlgebra.isotropic_adjustment {k : Type u_1} [Field k] [Invertible 2] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (B : LinearMap.BilinForm k V) (hBs : B.IsSymm) (x z : V) (hx_iso : (B x) x = 0) (hxz : (B x) z = 1) : IsHyperbolicPair B x (z - (⅟2 * (B z) z) • x)

Adjust a vector z with B x z = 1 to obtain a hyperbolic pair partner for the isotropic x (subtract off the right multiple of x to make z isotropic).

theorem Formalization.GeometricAlgebra.hyperbolic_pair_from_radical_with_tail_orth {k : Type u_1} [Field k] [Invertible 2] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (B : LinearMap.BilinForm k V) (hB : B.Nondegenerate) (hBs : B.IsSymm) (W W₁ : Submodule k V) (hW₁_le : W₁ ≤ W) (_hSup : SubspaceRadical B W ⊔ W₁ = W) (hW₁_nd : (B.restrict W₁).Nondegenerate) {n : ℕ} (bW₀ : Module.Basis (Fin (n + 1)) k ↥(SubspaceRadical B W)) : ∃ y₀ ∈ B.orthogonal W₁, IsHyperbolicPair B (↑(bW₀ 0)) y₀ ∧ ∀ (j : Fin n), (B ↑(bW₀ j.succ)) y₀ = 0

Given a vector x₀ in the radical of W together with a basis-tail condition, produce a hyperbolic partner y₀ to x₀ orthogonal to the tail of the basis.

theorem Formalization.GeometricAlgebra.radical_shrinks_after_hyperbolic_extension {k : Type u_1} [Field k] [Invertible 2] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (B : LinearMap.BilinForm k V) (hBs : B.IsSymm) (W : Submodule k V) {n : ℕ} (bW₀ : Module.Basis (Fin (n + 1)) k ↥(SubspaceRadical B W)) (y₀ : V) (hBy₀ : (B ↑(bW₀ 0)) y₀ = 1) (hBy₀_tail : ∀ (j : Fin n), (B ↑(bW₀ j.succ)) y₀ = 0) : ∃ (bW₀' : Module.Basis (Fin n) k ↥(SubspaceRadical B (W ⊔ k ∙ y₀))), ∀ (j : Fin n), ↑(bW₀' j) = ↑(bW₀ j.succ)

Adjoining a hyperbolic partner y₀ (for the first basis vector of the radical of W) to W reduces the dimension of the radical by one.

theorem Formalization.GeometricAlgebra.nondegen_complement_extension_with_W₁ {k : Type u_1} [Field k] [Invertible 2] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (B : LinearMap.BilinForm k V) (hB : B.Nondegenerate) (hBs : B.IsSymm) (W W₁ : Submodule k V) (hW₁_le : W₁ ≤ W) (hDisj : Disjoint (SubspaceRadical B W) W₁) (hSup : SubspaceRadical B W ⊔ W₁ = W) (hW₁_nd : (B.restrict W₁).Nondegenerate) (x₀ y₀ : V) (hx₀ : x₀ ∈ SubspaceRadical B W) (hy₀_orth : y₀ ∈ B.orthogonal W₁) (hhp : IsHyperbolicPair B x₀ y₀) : have W' := W ⊔ k ∙ y₀; ∃ (W₁' : Submodule k V), W₁ ≤ W₁' ∧ Submodule.span k {x₀, y₀} ≤ W₁' ∧ W₁' ≤ W' ∧ Disjoint (SubspaceRadical B W') W₁' ∧ SubspaceRadical B W' ⊔ W₁' = W' ∧ (B.restrict W₁').Nondegenerate

Extend a nondegenerate complement W₁ of the radical of W to a nondegenerate complement of the radical of W' = W ⊔ ⟨y₀⟩ by adjoining the hyperbolic pair {x₀, y₀}.

def Formalization.GeometricAlgebra.IsHyperbolicSpace {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (S : Submodule k V) : Prop

A subspace S is a hyperbolic space for B if it is spanned by a finite collection of mutually orthogonal hyperbolic pairs {x_i, y_i}.

theorem Formalization.GeometricAlgebra.kernel_decomposition_hyperbolic_planes_full {k : Type u_3} [Field k] [Invertible 2] {V : Type u_4} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (B : LinearMap.BilinForm k V) (hB : B.Nondegenerate) (hBs : B.IsSymm) (W W₁ : Submodule k V) (hW₁_le : W₁ ≤ W) (hDisj : Disjoint (SubspaceRadical B W) W₁) (hSup : SubspaceRadical B W ⊔ W₁ = W) (hW₁_nd : (B.restrict W₁).Nondegenerate) (n : ℕ) (bW₀ : Module.Basis (Fin n) k ↥(SubspaceRadical B W)) : ∃ (y : Fin n → V), (∀ (i : Fin n), y i ∈ B.orthogonal W₁) ∧ (∀ (i : Fin n), IsHyperbolicPair B (↑(bW₀ i)) (y i)) ∧ (∀ (i j : Fin n), i ≠ j → (B ↑(bW₀ i)) (y j) = 0 ∧ (B (y i)) (y j) = 0) ∧ (B.restrict (W ⊔ Submodule.span k (Set.range y))).Nondegenerate ∧ IsHyperbolicSpace B (SubspaceRadical B W ⊔ Submodule.span k (Set.range y)) ∧ Disjoint W (Submodule.span k (Set.range y))

Full kernel decomposition: given a basis bW₀ for the radical of W and a nondegenerate complement W₁, produce hyperbolic partners y_i that extend W to a subspace whose radical-complement is fully nondegenerate and contains an explicit hyperbolic-plane decomposition.