structure GeometricAlgebra.SwapCompositionInvariant {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F F'₁ F'₂ : Flag k V) (h₁ : F.isOppositeFlag F'₁) (h₂ : F.isOppositeFlag F'₂) (e : V ≃ₗ[k] V) (levels_done : ℕ) : Prop

Inductive invariant for the composition of swap automorphisms used to conjugate one opposite flag to another. After levels_done swap steps, the automorphism e is required to stabilize every level of the fixed flag F and to have already mapped the top levels_done levels of F'₁ onto the corresponding levels of F'₂.

• preserves_F (i : Fin F.len) : Submodule.map (↑e) (F.spaces i) = F.spaces i
• maps_F'_done (j : Fin F'₁.len) : let j₂ := ⟨↑j, ⋯⟩; ↑j ≥ F'₁.len - levels_done → Submodule.map (↑e) (F'₁.spaces j) = F'₂.spaces j₂

theorem GeometricAlgebra.swap_composition_base {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F F'₁ F'₂ : Flag k V) (h₁ : F.isOppositeFlag F'₁) (h₂ : F.isOppositeFlag F'₂) : SwapCompositionInvariant F F'₁ F'₂ h₁ h₂ (LinearEquiv.refl k V) 0

Base case of the swap-composition induction: the identity automorphism trivially satisfies the invariant after 0 levels have been handled.

structure GeometricAlgebra.SwapCompositionStepHyp (k : Type u_3) [Field k] (V : Type u_4) [AddCommGroup V] [Module k V] : Prop

Inductive-step hypothesis packaging the existence of a swap that advances the SwapCompositionInvariant from levels_done to levels_done + 1, for every choice of flags and prior approximation e_prev. This is the key local construction supplied by stepHyp_proof.

• step (F F'₁ F'₂ : Flag k V) (h₁ : F.isOppositeFlag F'₁) (h₂ : F.isOppositeFlag F'₂) (levels_done : ℕ) (h_lt : levels_done < F'₁.len) (e_prev : V ≃ₗ[k] V) (inv : SwapCompositionInvariant F F'₁ F'₂ h₁ h₂ e_prev levels_done) : ∃ (e_next : V ≃ₗ[k] V), SwapCompositionInvariant F F'₁ F'₂ h₁ h₂ e_next (levels_done + 1)

theorem GeometricAlgebra.invariant_at_level {k : Type u_3} [Field k] {V : Type u_4} [AddCommGroup V] [Module k V] (step_hyp : SwapCompositionStepHyp k V) (F F'₁ F'₂ : Flag k V) (h₁ : F.isOppositeFlag F'₁) (h₂ : F.isOppositeFlag F'₂) (m : ℕ) (hm : m ≤ F'₁.len) : ∃ (e : V ≃ₗ[k] V), SwapCompositionInvariant F F'₁ F'₂ h₁ h₂ e m

Iterating the step hypothesis: for every m ≤ F'₁.len there exists an automorphism satisfying the SwapCompositionInvariant at level m. Proof is by induction on m.

theorem GeometricAlgebra.opposite_conjugacy_of_step {k : Type u_3} [Field k] {V : Type u_4} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (step_hyp : SwapCompositionStepHyp k V) : OppositeConjugacyCompositionHyp k V

Running the swap-composition induction up to F'₁.len produces an automorphism that fixes F and sends F'₁ to F'₂, yielding the OppositeConjugacyCompositionHyp.

theorem GeometricAlgebra.complIsomOfIsCompl_coe_eq {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (W C₁ C₂ : Submodule k V) (hc₁ : IsCompl W C₁) (hc₂ : IsCompl W C₂) (c : ↥C₁) : ↑((complIsomOfIsCompl W C₁ C₂ hc₁ hc₂) c) = ↑((C₂.linearProjOfIsCompl W ⋯) ↑c)

The underlying vector of complIsomOfIsCompl W C₁ C₂ hc₁ hc₂ c is obtained from c by linear projection onto C₂ along W (via the symmetric complement).

theorem GeometricAlgebra.swapComplement_sub_mem_W {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (W C₁ C₂ : Submodule k V) (hc₁ : IsCompl W C₁) (hc₂ : IsCompl W C₂) (v : V) : (swapComplement W C₁ C₂ hc₁ hc₂) v - v ∈ W

The swap-complement automorphism agrees with the identity modulo W: for every v ∈ V, the difference swapComplement W C₁ C₂ hc₁ hc₂ v - v lies in W.

theorem GeometricAlgebra.swapComplement_preserves_of_both_le {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (W C₁ C₂ S : Submodule k V) (hc₁ : IsCompl W C₁) (hc₂ : IsCompl W C₂) (hC₁_le : C₁ ≤ S) (hC₂_le : C₂ ≤ S) : Submodule.map (↑(swapComplement W C₁ C₂ hc₁ hc₂)) S = S

A subspace S that contains both complements C₁ and C₂ is stabilized by the swap-complement automorphism swapComplement W C₁ C₂ hc₁ hc₂.

theorem GeometricAlgebra.swapComplement_preserves_sup {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (W C₁ C₂ S : Submodule k V) (hc₁ : IsCompl W C₁) (hc₂ : IsCompl W C₂) (hle : W ≤ S) : Submodule.map (↑(swapComplement W C₁ C₂ hc₁ hc₂)) S = S

A subspace S that contains W is stabilized by the swap-complement automorphism swapComplement W C₁ C₂ hc₁ hc₂, because the swap moves vectors only by elements of W.

theorem GeometricAlgebra.stepHyp_proof {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] : SwapCompositionStepHyp k V

Concrete construction of the step hypothesis SwapCompositionStepHyp: given an automorphism e_prev realizing the invariant at level levels_done, post-compose with the appropriate swap-complement automorphism (along F.spaces i_F) to obtain e_next realizing the invariant at level levels_done + 1. The swap moves the transported complement C₁_trans onto F'₂.spaces target₂ while stabilizing every level of F and every higher level of F'₁ already aligned with F'₂.