Documentation

GQ2.Roe.DevissageInduction

The dévissage induction on the r_R spine: prop_5_15_R from the simple case #

Mechanical R-spine clone of GQ2/DevissageInduction.lean (campaign decision, docs/orchestration/roe-r20-recon.md). prop_5_15_of_simple_R: if IsSelfDual_R t B holds for every simple finite elementary-2 C-module B, then it holds for every finite elementary-2 C-module A. Strong induction on Nat.card A; the induction step forwards hw : t.WildRelR to lemma_5_11_R along 0 → W → A → A ⧸ W → 0, and the subsingleton (zero-module) base case is R25's trivialSelfDual_R (GQ2/Roe/TrivialSelfDual.lean) — exactly as the Γ_A capstone uses trivialSelfDual. Proof ported verbatim.

The self-duality predicate IsSelfDual_R and the base case trivialSelfDual_R are R25's (GQ2/Roe/TrivialSelfDual.lean), reused here per the campaign convention (recon §1.5); the reusable induction infrastructure stableSubAction/stableQuotAction/two_torsion_sub/ two_torsion_quot/card_lt_of_ne_top/card_quot_lt_of_ne_bot (all (A)-generic, word-free) is reused from GQ2.DevissageInduction, never cloned.

source
theorem GQ2.FoxH.prop_5_15_of_simple_R {C : Type u_1} [Group C] [Finite C] (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (hgen : t.Generates) (hsimp : ∀ (B : Type u) [inst : AddCommGroup B] [inst_1 : DistribMulAction C B] [inst_2 : Finite B], (∀ (b : B), b + b = 0) → IsSimpleModTwo C B → IsSelfDual_R t B) {A : Type u} [AddCommGroup A] [DistribMulAction C A] [Finite A] (hA₂ : ∀ (a : A), a + a = 0) :
IsSelfDual_R t A

Prop 5.15, dévissage half (the Prop. 5.15 proof), on the r_R spine: IsSelfDual_R for all finite elementary-2 C-modules, parameterized over the simple case (hsimp). R-spine clone of prop_5_15_of_simple; proof ported verbatim. The induction step is lemma_5_11_R along 0 → W → A → A ⧸ W → 0 for a C-stable W ∉ {⊥, ⊤}; the subsingleton base is R25's trivialSelfDual_R.

Paper-tag ledger (Roe note paper/roe-presentation-verification.tex; hand-maintained) #