F-H1 — tower-head simplicity (lem:simplehead part 2, tower)

def Q2Presentation.Induction.towerModuleSubgroup {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (U : Submodule (ZMod 2) (towerM K)) : Subgroup p.fst.Y

The Y-subgroup underlying an invariant submodule of the TOWER module M = K/Φ(K): the preimage in K of the subgroup of K/Φ(K) underlying U — the mstage moduleSubgroup (HeadSimple.lean:64) with the extra Frattini-quotient comap layer.

Equations

• One or more equations did not get rendered due to their size.

theorem Q2Presentation.Induction.mem_towerModuleSubgroup {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (U : Submodule (ZMod 2) (towerM K)) (y : p.fst.Y) : y ∈ towerModuleSubgroup chief K U ↔ ∃ (hy : y ∈ K.Ksub), Additive.ofMul ((QuotientGroup.mk' (frattini ↥K.Ksub)) ⟨y, hy⟩) ∈ U

theorem Q2Presentation.Induction.towerHead_submodule_dichotomy {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (V' : Submodule (ZMod 2) (towerM K ⧸ towerT K)) (hact : ∀ (c : towerC K), ∀ v ∈ V', (headActE chief K c) v ∈ V') : V' = ⊥ ∨ V' = ⊤

F-H1 (tower-head simplicity): a towerC-invariant submodule of the head V = towerM K ⧸ towerT K is ⊥ or ⊤ — lem:simplehead part 2 at the tower carrier (design §4.1 F-H1; the mstage original, head_submodule_dichotomy at HeadSimple.lean:82, is unmodified). Pull V' back to U ≤ towerM K (which contains towerT), then to the Y-normal subgroup D = towerModuleSubgroup U with lower ⊓ K ≤ D ≤ K; the chief clause traps D ⊔ lower between lower and upper, and K.minimal_inside closes the top case.

F-H2 — a normal 2-subgroup of the acting group acts trivially

theorem Q2Presentation.Induction.exists_ne_zero_fixed_of_two_subgroup {G : Type} [Group G] {W : Type} [AddCommGroup W] [Module (ZMod 2) W] [Finite W] [Nontrivial W] (ρ : G →* W ≃ₗ[ZMod 2] W) (P : Subgroup G) (hP2 : IsPGroup 2 ↥P) : ∃ (w : W), w ≠ 0 ∧ ∀ g ∈ P, (ρ g) w = w

Fixed-point existence: a 2-subgroup acting 𝔽₂-linearly on a finite NONTRIVIAL module fixes a NONZERO vector — |W^P| ≡ |W| ≡ 0 (mod 2) (IsPGroup.card_modEq_card_fixedPoints, |W| = 2^d with d ≥ 1) and 0 ∈ W^P, so |W^P| ≥ 2.

theorem Q2Presentation.Induction.two_subgroup_acts_trivially_of_dichotomy {G : Type} [Group G] {W : Type} [AddCommGroup W] [Module (ZMod 2) W] [Finite W] [Nontrivial W] (ρ : G →* W ≃ₗ[ZMod 2] W) (hdich : ∀ (U : Submodule (ZMod 2) W), (∀ (g : G), ∀ w ∈ U, (ρ g) w ∈ U) → U = ⊥ ∨ U = ⊤) (P : Subgroup G) (hPn : P.Normal) (hP2 : IsPGroup 2 ↥P) (g : G) : g ∈ P → ∀ (w : W), (ρ g) w = w

F-H2: a NORMAL 2-subgroup acting 𝔽₂-linearly on a finite nontrivial module with the invariant-submodule dichotomy acts trivially — the fixed space is a nonzero invariant submodule (nonzero by the mod-2 fixed-point count, invariant by normality), hence ⊤ (design §4.1 F-H2; manuscript l.2717–2719's argument shape).

F-H3 — the wild kill and the tame factorization

def Q2Presentation.Induction.towerWildImage {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Subgroup (towerC K)

The image of the marked wild 2-subgroup L_Y in towerC K = Y/K.

Equations

• Q2Presentation.Induction.towerWildImage chief K = Subgroup.map (QuotientGroup.mk' K.Ksub) p.fst.LY

theorem Q2Presentation.Induction.towerWildImage_normal {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : (towerWildImage chief K).Normal

theorem Q2Presentation.Induction.towerWildImage_isTwoGroup {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : IsPGroup 2 ↥(towerWildImage chief K)

theorem Q2Presentation.Induction.towerWildImage_le_headActHom_ker {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : towerWildImage chief K ≤ (headActHom chief K).ker

F-H3 (the wild kill): the wild image is a normal 2-subgroup of towerC K, so by F-H1's dichotomy and F-H2 it acts trivially on the head — L_Y/K ≤ ker headActHom (design §4.1 F-H3).

def Q2Presentation.Induction.headOfY {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : p.fst.Y →* HeadIm chief K

The composite Y → towerC K → HeadIm (both canonical quotients).

Equations

• Q2Presentation.Induction.headOfY chief K = (QuotientGroup.mk' (Q2Presentation.Induction.headActHom chief K).ker).comp (QuotientGroup.mk' K.Ksub)

theorem Q2Presentation.Induction.headOfY_surjective {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Function.Surjective ⇑(headOfY chief K)

theorem Q2Presentation.Induction.piY_ker_le_headOfY_ker {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : p.fst.piY.ker ≤ (headOfY chief K).ker

ker π_Y = L_Y dies in the faithful head image (the wild kill, composed through both quotients).

noncomputable def Q2Presentation.Induction.headOfH {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : p.fst.H →* HeadIm chief K

The tame factorization of the head (F-H3): the faithful head image is a quotient of the finite tame target p.1.H = Y/L_Y — the hom descended along π_Y (piY_surj, ker_piY), with headOfH ∘ π_Y = headOfY (headOfH_piY).

Equations

• Q2Presentation.Induction.headOfH chief K = (p.fst.piY.liftOfSurjective ⋯) ⟨Q2Presentation.Induction.headOfY chief K, ⋯⟩

theorem Q2Presentation.Induction.headOfH_piY {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (y : p.fst.Y) : (headOfH chief K) (p.fst.piY y) = (headOfY chief K) y

theorem Q2Presentation.Induction.headOfH_surjective {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Function.Surjective ⇑(headOfH chief K)

F-H4 — the metacyclic H_V shape of the faithful image

noncomputable def Q2Presentation.Induction.headOfTame {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : ↑Ttame.toProfinite.toTop →* HeadIm chief K

The tame boundary composite Ttame →* HeadIm through the frame p.2 (design §4.1 F-H4: frame ONLY, no Marking/hlift binders).

Equations

• Q2Presentation.Induction.headOfTame chief K = (Q2Presentation.Induction.headOfH chief K).comp (ProfiniteGrp.Hom.hom p.snd.alpha).toMonoidHom

noncomputable def Q2Presentation.Induction.headSigma {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : HeadIm chief K

σ̃ — the unramified generator's image in the faithful head image.

Equations

• Q2Presentation.Induction.headSigma chief K = (Q2Presentation.Induction.headOfTame chief K) Q2Presentation.tameSigma

noncomputable def Q2Presentation.Induction.headTau {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : HeadIm chief K

τ̃ — THE canonical ramification operator of the block (design §4.2/§4.5: headTau = 1 exactly captures the unramified discharge below; when P8-S2a lands, blockTameRamFlag is to be DEFINED as the Bool-spelling of headTau ≠ 1, so the F-ram gate and the sign-lane flag are the same object).

Equations

• Q2Presentation.Induction.headTau chief K = (Q2Presentation.Induction.headOfTame chief K) Q2Presentation.tameTau

theorem Q2Presentation.Induction.head_tame_rel {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : rconj (headTau chief K) (headSigma chief K) = headTau chief K ^ 2

The tame relation τ̃^σ̃ = τ̃² holds in the head image (Ttame_tame_rel pushed through headOfTame; manuscript convention rconj x g = g⁻¹xg).

theorem Q2Presentation.Induction.headTau_orderOf_odd {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Odd (orderOf (headTau chief K))

τ̃ has ODD order — finite_tame_tau_odd (Lemma 3.1's oddness part) at the finite head image.

theorem Q2Presentation.Induction.headIm_generated {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Subgroup.closure {headSigma chief K, headTau chief K} = ⊤

The faithful image is generated by σ̃, τ̃ (tame_target_generated at the frame, pushed through the surjective headOfH).

theorem Q2Presentation.Induction.headTau_zpowers_normal {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : (Subgroup.zpowers (headTau chief K)).Normal

⟨τ̃⟩ ⊴ HeadIm — normal inertia (design §4.1 F-H4), via the banked GREEN generic OddSplitting.tame_zpowers_normal (Lifting/OddSplitting.lean:214 — generation + tame relation + odd order; the mechanism of manuscript Lemma 3.1).

theorem Q2Presentation.Induction.headIm_mod_headTau_cyclic {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (x : HeadIm chief K ⧸ Subgroup.zpowers (headTau chief K)) : x ∈ Subgroup.zpowers ((QuotientGroup.mk' (Subgroup.zpowers (headTau chief K))) (headSigma chief K))

The quotient by the inertia is cyclic, generated by σ̃ — H_V-shape part 2, stated in the honest generator-membership form (design §4.1 F-H4: odd normal I = ⟨τ̃⟩, cyclic H/I).

F-H5 — the unramified discharge: headTau = 1 ⟹ hodd ⟹ model

theorem Q2Presentation.Induction.headIm_eq_zpowers_of_headTau_eq_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (h1 : headTau chief K = 1) : Subgroup.zpowers (headSigma chief K) = ⊤

Unramified ⟹ the faithful image is cyclic: ⟨σ̃⟩ = ⊤.

theorem Q2Presentation.Induction.headIm_odd_of_unramified {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (h1 : headTau chief K = 1) : Odd (Nat.card (HeadIm chief K))

F-H5 — the unramified clause is a THEOREM (lem:basedetclass l.2342–2345): at headTau = 1 the faithful image is cyclic; by Cauchy an even order would give an element t of order 2, whose (normal, since the group is cyclic) ⟨t⟩ acts trivially by F-H2 over F-H1's dichotomy — contradicting faithfulness of actQ (QuotientGroup.kerLift_injective). So |HeadIm| is odd. IMPLICATION ONLY — the converse is FALSE (odd ramified blocks exist, design §4.3): never state this as an iff.

theorem Q2Presentation.Induction.headTau_ne_one_of_not_odd {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hodd : ¬Odd (Nat.card (HeadIm chief K))) : headTau chief K ≠ 1

Contrapositive certification (design §4.2): an EVEN faithful image forces genuine ramification — the F-G3 residual's ¬Odd |HeadIm| gate pins the future keep q2_baseModel_highdim_even to ramified blocks.

theorem Q2Presentation.Induction.baseModelExists_of_unramified {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (h1 : headTau chief K = 1) : BaseModelExists chief K lam hinv hne

The unramified branch of q2_baseModel is a THEOREM (F-H5 exit): headTau = 1 ⟹ Odd |HeadIm| ⟹ BaseModelExists, through the banked baseModelExists_of_oddHeadAction. This makes the manuscript's entire unramified clause of lem:basedetclass (l.2342–2345) in-tree; composed with the F-G3 assembly it certifies the residual keep's content as EXACTLY the ramified 4 < dimV branch.