Coprime-action stability and the terminal Schur–Zassenhaus splitting (Stage H residual)

This file discharges the standard finite-group-theory axiom Q2Presentation.Induction.terminalSplit_of_scalarTerminal of Induction/ScalarTerminal.lean, proving its exact statement as the theorem terminalSplit_of_scalarTerminal_proven, sorry-free and with axiom closure {propext, Classical.choice, Quot.sound} only.

The one piece missing from mathlib v4.28.0 is coprime-action stability: a finite group A of order coprime to a 2-group L, acting on L trivially on every chief factor, centralises L. mathlib has only the cyclic-Sylow version (ZGroup.commutator_eq_bot_or_commutator_eq_self). We prove the general statement we need by the standard route:

• commutator_eq_bot_of_subfactor_centralizes — the elementary kicker: if A centralises M ◁ L and L/M (i.e. ⁅L,A⁆ ≤ M and ⁅M,A⁆ = ⊥), with L a 2-group and |A| odd, then A centralises L. Proof: for l ∈ L, a ∈ A, the element d = ⁅a,l⁆ ∈ M is a-central, so aᵏ l a⁻ᵏ = dᵏ l; at k = |A| (odd) this gives dᵏ = 1, and d has 2-power order in the 2-group L, forcing d = 1.
• commutator_subgroup_eq_bot_of_scalarTerminal — the quotient induction: strong induction on Nat.card L down a Y-chief series; at each step pick a maximal proper Y-normal subgroup M, apply the scalar-terminal hypothesis and the kicker.

These two are pure, general finite group theory (any G). The terminal splitting then follows from: the tame relation makes H = Y/L_Y 2-nilpotent (Burnside transfer on its cyclic Sylow 2-subgroup), Schur–Zassenhaus on the odd part, coprime stability for centralising, and the characteristic Hall 2'-subgroup giving normality in Y.

Part 1 — coprime-action stability (general finite group theory)

theorem Q2Presentation.Induction.commutator_eq_bot_of_subfactor_centralizes {G : Type u_1} [Group G] [Finite G] {A L M : Subgroup G} (hML : M ≤ L) (hLA : ⁅L, A⁆ ≤ M) (hMA : ⁅M, A⁆ = ⊥) (hL2 : IsPGroup 2 ↥L) (hAodd : Odd (Nat.card ↥A)) : ⁅L, A⁆ = ⊥

The elementary coprime kicker. Let A, L, M be subgroups of a finite group G with M ≤ L. If A centralises the quotient L/M (⁅L,A⁆ ≤ M) and centralises M (⁅M,A⁆ = ⊥), L is a 2-group and |A| is odd, then A centralises L (⁅L,A⁆ = ⊥).

This is the standard "odd automorphism trivial on a 2-group 2-step factor is trivial" fact (Isaacs FGT 3.x / Gorenstein): for l ∈ L, a ∈ A, set d = ⁅a,l⁆ = a l a⁻¹ l⁻¹ ∈ ⁅L,A⁆ ≤ M. Since A centralises M, a commutes with d, so by induction aᵏ l a⁻ᵏ = dᵏ l. At k = Nat.card A (aᵏ = 1) this yields dᵏ = 1; but d lies in the 2-group L, so orderOf d is a power of 2 dividing the odd k, forcing d = 1, i.e. ⁅l,a⁆ = 1.

Part 2 — the quotient induction down a chief series

theorem Q2Presentation.Induction.commutator_subgroup_eq_bot_of_scalarTerminal (Yt : BoundaryFramedTarget) (A : Subgroup Yt.Y) (hAodd : Odd (Nat.card ↥A)) (hST : ScalarTerminalTarget Yt) (L : Subgroup Yt.Y) : L.Normal → L ≤ Yt.LY → ⁅L, A⁆ = ⊥

Coprime stability via scalar-terminality. If A ≤ Y has odd order and Yt is scalar-terminal (every Y-chief factor inside L_Y is Y-trivial), then A centralises every Y-normal subgroup of L_Y. Strong induction on Nat.card L: pick a maximal proper Y-normal M < L, which is a chief factor, so scalar-terminality gives ⁅L,A⁆ ≤ M; induction gives ⁅M,A⁆ = ⊥; the kicker finishes.

Part 3 — the tame quotient H has a normal 2-complement

theorem Q2Presentation.Induction.tame_exists_odd_normal_pow2_index {H : Type u_1} [Group H] [Finite H] (s t : H) (hgen : Subgroup.closure {s, t} = ⊤) (htame : rconj t s = t ^ 2) : ∃ (N : Subgroup H), N.Normal ∧ Odd (Nat.card ↥N) ∧ ∃ (k : ℕ), N.index = 2 ^ k

The tame relation makes H 2-nilpotent. If H = ⟨s, t⟩ with s⁻¹ t s = t² (tame), then ⟨t⟩ is a normal subgroup of odd order with cyclic quotient H/⟨t⟩, so the Sylow 2-subgroup of H is cyclic, and Burnside transfer (IsCyclic.isComplement') produces a normal 2'-complement N ◁ H: odd order, with 2-power index.

Part 4 — the terminal Schur–Zassenhaus splitting (the deliverable)

theorem Q2Presentation.Induction.terminalSplit_of_scalarTerminal_proven (Yt : BoundaryFramedTarget) (s t : Yt.H) (hgen : Subgroup.closure {s, t} = ⊤) (htame : rconj t s = t ^ 2) (h : ScalarTerminalTarget Yt) : ∃ (Ñ : Subgroup Yt.Y), Ñ.Normal ∧ Odd (Nat.card ↥Ñ) ∧ (∃ (k : ℕ), Ñ.index = 2 ^ k) ∧ ∀ l ∈ Yt.LY, ∀ n ∈ Ñ, l * n = n * l

THE DELIVERABLE — terminalSplit_of_scalarTerminal proved as a theorem. The exact statement of Q2Presentation.Induction.terminalSplit_of_scalarTerminal, here a theorem whose closure is {propext, Classical.choice, Quot.sound} only. (Conclusion written as the definitional unfolding of TerminalReduction Yt, so it is defeq to that predicate and can be spliced directly into ScalarTerminal.lean in place of the axiom.)

The argument: the tame quotient H = Y/L_Y has a normal 2-complement N (tame_exists_odd_normal_pow2_index); its preimage P = π_Y⁻¹(N) contains L_Y with odd, coprime index [P : L_Y] = |N|, so Schur–Zassenhaus splits off a complement Ñ; coprime stability (commutator_subgroup_eq_bot_of_scalarTerminal) makes Ñ centralise L_Y, exhibiting P = L_Y × Ñ with Ñ the odd Hall factor — characterised as the odd-order elements of P, hence normal in Y — of odd order and 2-power index.

Acceptance checks

terminalSplit_of_scalarTerminal_proven has the exact statement of the axiom Q2Presentation.Induction.terminalSplit_of_scalarTerminal of Induction/ScalarTerminal.lean: same binders (Yt) (s t) (hgen) (htame) (h), and conclusion the definitional unfolding of TerminalReduction Yt. This file deliberately does not import ScalarTerminal.lean (so that ScalarTerminal.lean may import this file when the axiom is swapped, with no import cycle); the conclusion is therefore written as the ∃ Ñ, … body of TerminalReduction, which is definitionally equal to TerminalReduction Yt. Hence in ScalarTerminal.lean the axiom can be replaced by

theorem terminalSplit_of_scalarTerminal (Yt) (s t) (hgen) (htame) (h) : TerminalReduction Yt := Q2Presentation.Induction.terminalSplit_of_scalarTerminal_proven Yt s t hgen htame h

which type-checks by that defeq.