§6 pushout construction, step 1 (checkpoint-F9 slice 1)

The transgression maps of prop:simpleheaddet on the literal §7 tower: sec7SqAux (k ↦ k²) and sec7CommAux ((k,k') ↦ [k,k']) land in the ambient Frattini copy R = Φ(K) and descend along Φ(K) (centrality + exponent two), so they define maps on M = K/Φ(K) — the concrete carriers for the packet fields of minimalBlock_preheadActualCentralExtensionPushoutDataOfRawTower. Quadratic law, equivariance, annihilation/radical: next slices (scripts_fable/DESIGN_F9_pushout_construction.md).

Ambient group-identity lemmas (coercion-free)

The transgression carriers

def Q2Presentation.Induction.sec7SqAux {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (k : ↥K.Ksub) : towerR chief K

The square of a kernel element, in the ambient Frattini copy.

Equations

• Q2Presentation.Induction.sec7SqAux chief K k = Additive.ofMul ⟨↑k ^ 2, ⋯⟩

def Q2Presentation.Induction.sec7CommAux {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (k k' : ↥K.Ksub) : towerR chief K

The commutator of two kernel elements, in the ambient Frattini copy.

Equations

• Q2Presentation.Induction.sec7CommAux chief K k k' = Additive.ofMul ⟨⁅↑k, ↑k'⁆, ⋯⟩

theorem Q2Presentation.Induction.sec7_frattini_comm {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (z k : ↥K.Ksub) (hz : z ∈ frattini ↥K.Ksub) : ↑z * ↑k = ↑k * ↑z

Ambient centrality of the Frattini layer against K.

theorem Q2Presentation.Induction.sec7_frattini_sq {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (z : ↥K.Ksub) (hz : z ∈ frattini ↥K.Ksub) : ↑z ^ 2 = 1

Ambient exponent two of the Frattini layer.

theorem Q2Presentation.Induction.sec7SqAux_descends {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (k z : ↥K.Ksub) (hz : z ∈ frattini ↥K.Ksub) : sec7SqAux chief K (k * z) = sec7SqAux chief K k

Descent of the squaring transgression along Φ(K).

theorem Q2Presentation.Induction.sec7CommAux_descends_left {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (k k' z : ↥K.Ksub) (hz : z ∈ frattini ↥K.Ksub) : sec7CommAux chief K (k * z) k' = sec7CommAux chief K k k'

Descent of the commutator transgression in the first slot.

theorem Q2Presentation.Induction.sec7CommAux_descends_right {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (k k' z : ↥K.Ksub) (hz : z ∈ frattini ↥K.Ksub) : sec7CommAux chief K k (k' * z) = sec7CommAux chief K k k'

Descent of the commutator transgression in the second slot.

Slice 2: descent to M = K/Φ(K) and the quadratic law

def Q2Presentation.Induction.sec7SqMap {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (m : towerMgrp K) : towerR chief K

The squaring transgression on M = K/Φ(K).

Equations

• Q2Presentation.Induction.sec7SqMap chief K m = Quotient.liftOn' m (Q2Presentation.Induction.sec7SqAux chief K) ⋯

@[simp]

theorem Q2Presentation.Induction.sec7SqMap_mk {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (k : ↥K.Ksub) : sec7SqMap chief K ((QuotientGroup.mk' (frattini ↥K.Ksub)) k) = sec7SqAux chief K k

def Q2Presentation.Induction.sec7CommMap {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (m m' : towerMgrp K) : towerR chief K

The commutator transgression on M = K/Φ(K).

Equations

• Q2Presentation.Induction.sec7CommMap chief K m m' = Quotient.liftOn₂' m m' (Q2Presentation.Induction.sec7CommAux chief K) ⋯

@[simp]

theorem Q2Presentation.Induction.sec7CommMap_mk {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (k k' : ↥K.Ksub) : sec7CommMap chief K ((QuotientGroup.mk' (frattini ↥K.Ksub)) k) ((QuotientGroup.mk' (frattini ↥K.Ksub)) k') = sec7CommAux chief K k k'

theorem Q2Presentation.Induction.sec7SqAux_mul {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (k k' : ↥K.Ksub) : sec7SqAux chief K (k * k') = sec7CommAux chief K k' k + sec7SqAux chief K k + sec7SqAux chief K k'

The quadratic law for the squaring transgression (prop:simpleheaddet mechanism): Sq(kk') = Comm(k',k) + Sq k + Sq k' in the abelian layer R.

Slice 3a: biadditivity and alternation of the commutator transgression

theorem Q2Presentation.Induction.sec7CommAux_mul_left {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (k₁ k₂ k' : ↥K.Ksub) : sec7CommAux chief K (k₁ * k₂) k' = sec7CommAux chief K k₂ k' + sec7CommAux chief K k₁ k'

Left additivity of the commutator transgression in the abelian layer.

theorem Q2Presentation.Induction.sec7CommAux_self {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (k : ↥K.Ksub) : sec7CommAux chief K k k = 0

Alternation of the commutator transgression.

Slice 3b: equivariance of the transgressions under ambient conjugation

theorem Q2Presentation.Induction.sec7SqAux_conj {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (y : p.fst.Y) (k : ↥K.Ksub) : sec7SqAux chief K ((kernelConjAut K y) k) = Additive.ofMul ((kernelFrattiniConjAut chief K y) (Additive.toMul (sec7SqAux chief K k)))

Squaring transgression intertwines ambient conjugation.

theorem Q2Presentation.Induction.sec7CommAux_conj {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (y : p.fst.Y) (k k' : ↥K.Ksub) : sec7CommAux chief K ((kernelConjAut K y) k) ((kernelConjAut K y) k') = Additive.ofMul ((kernelFrattiniConjAut chief K y) (Additive.toMul (sec7CommAux chief K k k')))

Commutator transgression intertwines ambient conjugation.

Slice 4a: the λ-composed quadratic family square λ : QuadF2 M

theorem Q2Presentation.Induction.sec7CommAux_mul_right {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (k k₁ k₂ : ↥K.Ksub) : sec7CommAux chief K k (k₁ * k₂) = sec7CommAux chief K k k₁ + sec7CommAux chief K k k₂

Right additivity of the commutator transgression.

theorem Q2Presentation.Induction.towerR_add_self {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (r : towerR chief K) : r + r = 0

The Frattini layer has exponent two, additive form.

theorem Q2Presentation.Induction.sec7CommAux_swap {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (k k' : ↥K.Ksub) : sec7CommAux chief K k' k = sec7CommAux chief K k k'

Char-2 antisymmetry of the commutator transgression.

Additive-language wrappers on M

def Q2Presentation.Induction.sec7SqAdd {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (m : towerM K) : towerR chief K

The squaring transgression in additive language.

Equations

• Q2Presentation.Induction.sec7SqAdd chief K m = Q2Presentation.Induction.sec7SqMap chief K (Additive.toMul m)

def Q2Presentation.Induction.sec7CommAdd {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (m m' : towerM K) : towerR chief K

The commutator transgression in additive language.

Equations

• Q2Presentation.Induction.sec7CommAdd chief K m m' = Q2Presentation.Induction.sec7CommMap chief K (Additive.toMul m) (Additive.toMul m')

@[simp]

theorem Q2Presentation.Induction.sec7SqAdd_ofMul {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (k : ↥K.Ksub) : sec7SqAdd chief K (Additive.ofMul ((QuotientGroup.mk' (frattini ↥K.Ksub)) k)) = sec7SqAux chief K k

@[simp]

theorem Q2Presentation.Induction.sec7CommAdd_ofMul {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (k k' : ↥K.Ksub) : sec7CommAdd chief K (Additive.ofMul ((QuotientGroup.mk' (frattini ↥K.Ksub)) k)) (Additive.ofMul ((QuotientGroup.mk' (frattini ↥K.Ksub)) k')) = sec7CommAux chief K k k'

theorem Q2Presentation.Induction.sec7CommAdd_add_left {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (m₁ m₂ m' : towerM K) : sec7CommAdd chief K (m₁ + m₂) m' = sec7CommAdd chief K m₁ m' + sec7CommAdd chief K m₂ m'

Additivity of sec7CommAdd in the left slot.

theorem Q2Presentation.Induction.sec7CommAdd_add_right {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (m m₁ m₂ : towerM K) : sec7CommAdd chief K m (m₁ + m₂) = sec7CommAdd chief K m m₁ + sec7CommAdd chief K m m₂

Additivity of sec7CommAdd in the right slot.

theorem Q2Presentation.Induction.sec7CommAdd_zero_left {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (m' : towerM K) : sec7CommAdd chief K 0 m' = 0

Left-zero law for the commutator transgression.

theorem Q2Presentation.Induction.sec7CommAdd_zero_right {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (m : towerM K) : sec7CommAdd chief K m 0 = 0

Right-zero law for the commutator transgression.

def Q2Presentation.Induction.sec7PolarBilin {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (towerR chief K)) : towerM K →ₗ[ZMod 2] towerM K →ₗ[ZMod 2] ZMod 2

The λ-composed bundled bilinear polar form on M.

Equations

• Q2Presentation.Induction.sec7PolarBilin chief K lam = LinearMap.mk₂ (ZMod 2) (fun (m m' : Q2Presentation.Induction.towerM K) => lam (Q2Presentation.Induction.sec7CommAdd chief K m m')) ⋯ ⋯ ⋯ ⋯

def Q2Presentation.Induction.sec7SquareFamily {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (towerR chief K)) : Quadratic.QuadF2 (towerM K)

The λ-composed quadratic form square λ on M (prop:simpleheaddet): form m ↦ λ(Sq m), polar the λ-composed commutator pairing.

Equations

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

Slice 4b-i: S-membership reductions and conditional T-annihilation

The genuinely-§7 content of the annihilation clause is isolated as the explicit hypothesis KillsFrattiniInterS (an invariant character kills the Φ(K) ∩ S layer — manuscript lem:simplehead); everything else is proven group theory.

theorem Q2Presentation.Induction.sec7Sq_mem_lower {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (k : ↥K.Ksub) (hk : ↑k ∈ chief.lower) : ↑(Additive.toMul (sec7SqAux chief K k)) ∈ chief.lower

Squares of K ∩ S-elements land in S (ambient form).

theorem Q2Presentation.Induction.sec7Comm_mem_lower_left {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (k k' : ↥K.Ksub) (hk : ↑k ∈ chief.lower) : ↑(Additive.toMul (sec7CommAux chief K k k')) ∈ chief.lower

Commutators against a K ∩ S-element land in S (normality of S).

def Q2Presentation.Induction.KillsFrattiniInterS {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (towerR chief K)) : Prop

The §7 kill hypothesis (lem:simplehead content, to be supplied by the crux residual): the character kills the ambient Φ(K) ∩ S layer.

Equations

• Q2Presentation.Induction.KillsFrattiniInterS chief K lam = ∀ (r : ↥(Q2Presentation.Induction.kernelFrattini K)), ↑r ∈ chief.lower → lam (Additive.ofMul r) = 0

theorem Q2Presentation.Induction.sec7SquareFamily_annihilates {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (towerR chief K)) (hkill : KillsFrattiniInterS chief K lam) : Annihilates (sec7SquareFamily chief K lam) (towerT K)

Conditional T-annihilation (prop:simpleheaddet annihilation clause): under the kill hypothesis, the λ-composed quadratic family annihilates the radical layer T = (K∩S)/Φ(K).

Slice 5a: the concrete prehead tower, the crux bundle, and packet assembly

def Q2Presentation.Induction.sec7ConcretePreheadTowerData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : MinimalBlockPreheadTowerData p chief.toNonScalarChiefFactor

The concrete prehead tower data of the literal §7 objects.

Equations

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

structure Q2Presentation.Induction.Sec7PushoutCruxData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Type

The F9 crux bundle — exactly the three genuinely-§7 facts of prop:simpleheaddet that remain after the mechanism layer above:

• phi — the equivariant quadratic refinement of the squaring transgression (manuscript l.3730–3770, the self-dual-head polarization);
• kill — invariant characters kill the Φ(K) ∩ S layer (lem:simplehead);
• radical — the polar radical lies in T (head-nondegeneracy, lem:simplehead).

• phi : Module.Dual (ZMod 2) (towerR chief K) → towerM K →ₗ[ZMod 2] Module.Dual (ZMod 2) (towerM K)
• diagonal (lam : Module.Dual (ZMod 2) (towerR chief K)) (m : towerM K) : (sec7SquareFamily chief K lam).form m = ((self.phi lam) m) m
• polar_symm (lam : Module.Dual (ZMod 2) (towerR chief K)) (m m' : towerM K) : ((sec7SquareFamily chief K lam).polar m) m' = ((self.phi lam) m) m' + ((self.phi lam) m') m
• natural (lam : Module.Dual (ZMod 2) (towerR chief K)) : lam ≠ 0 → (∀ (c : towerC K), lam ∘ₗ ↑((towerActR chief K) c) = lam) → ∀ (c : towerC K) (m m' : towerM K), ((self.phi lam) (((towerActM K) c) m)) (((towerActM K) c) m') = ((self.phi lam) m) m'
• kill (lam : Module.Dual (ZMod 2) (towerR chief K)) : lam ≠ 0 → (∀ (c : towerC K), lam ∘ₗ ↑((towerActR chief K) c) = lam) → KillsFrattiniInterS chief K lam
• radical (lam : Module.Dual (ZMod 2) (towerR chief K)) : lam ≠ 0 → (∀ (c : towerC K), lam ∘ₗ ↑((towerActR chief K) c) = lam) → ∀ (m : towerM K), (∀ (m' : towerM K), ((sec7SquareFamily chief K lam).polar m) m' = 0) → m ∈ towerT K

theorem Q2Presentation.Induction.sec7_pushoutPacket_ofCrux {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (crux : Sec7PushoutCruxData chief K) : Nonempty (MinimalBlockPreheadActualCentralExtensionPushoutData (sec7ConcretePreheadTowerData chief K))

Packet assembly: the full prop:simpleheaddet pushout packet over the concrete prehead tower, from the crux bundle plus the compiled mechanism layer.

axiom Q2Presentation.Induction.sec7_pushoutCruxData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Nonempty (Sec7PushoutCruxData chief K)

F9 crux residual (prop:simpleheaddet, l.3730–3770 + lem:simplehead). The three genuinely-§7 facts over the literal tower: the equivariant quadratic refinement φ_λ of the squaring transgression (the self-dual-head polarization), the invariant-character kill of the Φ(K) ∩ S layer, and head-nondegeneracy of the commutator pairing. Everything else in the pushout packet is THEOREM-level (this file): descents, the quadratic law, biadditivity/alternation/antisymmetry, equivariance of the transgressions, sec7SquareFamily, S-membership reductions, and conditional annihilation. Strictly smaller than the checkpoint-F8 residual minimalBlock_preheadActualCentralExtensionPushoutDataOfRawTower, which it replaces on the live route together with sec7_pushoutPacket_ofCrux.

theorem Q2Presentation.Induction.sec7_pushoutPacket {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Nonempty (MinimalBlockPreheadActualCentralExtensionPushoutData (sec7ConcretePreheadTowerData chief K))

The pushout packet over the concrete prehead tower, from the crux residual.

Slice F10-R2: M-level equivariance of the transgressions

theorem Q2Presentation.Induction.sec7SqAdd_equivariant {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (y : p.fst.Y) (m : towerM K) : sec7SqAdd chief K (((towerActM K) ((QuotientGroup.mk' K.Ksub) y)) m) = ((towerActR chief K) ((QuotientGroup.mk' K.Ksub) y)) (sec7SqAdd chief K m)

M-level equivariance of the squaring transgression: Sq(c·m) = actR c (Sq m).

theorem Q2Presentation.Induction.sec7SquareFamily_form_invariant {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (towerR chief K)) (hinv : ∀ (c : towerC K), lam ∘ₗ ↑((towerActR chief K) c) = lam) (c : towerC K) (m : towerM K) : (sec7SquareFamily chief K lam).form (((towerActM K) c) m) = (sec7SquareFamily chief K lam).form m

Invariance of the λ-composed quadratic form for invariant λ: q_λ(c·m) = q_λ(m).

Slice F10-R3: the manuscript-exact crux and the direct extraspecial triple

instance Q2Presentation.Induction.instFiniteZModOfNatNatTowerM {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Module.Finite (ZMod 2) (towerM K)

structure Q2Presentation.Induction.Sec7SimpleHeadCruxData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Prop

The manuscript-exact simple-head crux (prop:simpleheaddet, l.3745–3768): (i) the socle argument b_λ(T,M) = 0; (ii) the shear/H¹-vanishing argument q_λ|_T = 0; (iii) head-nondegeneracy (polar radical ⊆ T). Everything else in the extraspecial determinant interface is THEOREM-level via the polarization construction (Quadratic.polarization) and the compiled transgression layer.

• polar_zero_on_T (lam : Module.Dual (ZMod 2) (towerR chief K)) : lam ≠ 0 → (∀ (c : towerC K), lam ∘ₗ ↑((towerActR chief K) c) = lam) → ∀ t ∈ towerT K, ∀ (m : towerM K), ((sec7SquareFamily chief K lam).polar t) m = 0
• form_zero_on_T (lam : Module.Dual (ZMod 2) (towerR chief K)) : lam ≠ 0 → (∀ (c : towerC K), lam ∘ₗ ↑((towerActR chief K) c) = lam) → ∀ t ∈ towerT K, (sec7SquareFamily chief K lam).form t = 0
• radical_subset_T (lam : Module.Dual (ZMod 2) (towerR chief K)) : lam ≠ 0 → (∀ (c : towerC K), lam ∘ₗ ↑((towerActR chief K) c) = lam) → ∀ (m : towerM K), (∀ (m' : towerM K), ((sec7SquareFamily chief K lam).polar m) m' = 0) → m ∈ towerT K

axiom Q2Presentation.Induction.sec7_simpleHeadCruxData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Nonempty (Sec7SimpleHeadCruxData chief K)

F10 crux residual — exactly the three prop:simpleheaddet facts.

theorem Q2Presentation.Induction.sec7_extraspecialTriple_ofSimpleHeadCrux {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (crux : Sec7SimpleHeadCruxData chief K) : ∃ (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7ConcretePreheadTowerData chief K)), Nonempty (MinimalBlockPreheadExtraspecialAnnihilationData F) ∧ Nonempty (MinimalBlockPreheadExtraspecialRadicalData F)

The extraspecial determinant triple, direct from the manuscript-exact crux (bypassing the pushout-packet interface): the family is the polarization of the λ-composed quadratic forms; diagonal-invariance comes from the compiled transgression equivariance; annihilation and radical re-express through the polarization laws.

Slice F11-R1: commutator equivariance and the Burnside kill

theorem Q2Presentation.Induction.sec7CommAdd_equivariant {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (y : p.fst.Y) (m m' : towerM K) : sec7CommAdd chief K (((towerActM K) ((QuotientGroup.mk' K.Ksub) y)) m) (((towerActM K) ((QuotientGroup.mk' K.Ksub) y)) m') = ((towerActR chief K) ((QuotientGroup.mk' K.Ksub) y)) (sec7CommAdd chief K m m')

M-level equivariance of the commutator transgression.

theorem Q2Presentation.Induction.sec7SquareFamily_polar_invariant {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (towerR chief K)) (hinv : ∀ (c : towerC K), lam ∘ₗ ↑((towerActR chief K) c) = lam) (c : towerC K) (m m' : towerM K) : ((sec7SquareFamily chief K lam).polar (((towerActM K) c) m)) (((towerActM K) c) m') = ((sec7SquareFamily chief K lam).polar m) m'

Invariance of the λ-composed polar form for invariant λ.

theorem Q2Presentation.Induction.sec7_lam_eq_zero_of_kills_sq_comm {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (towerR chief K)) (hsq : ∀ (k : ↥K.Ksub), lam (sec7SqAux chief K k) = 0) (hcm : ∀ (k k' : ↥K.Ksub), lam (sec7CommAux chief K k k') = 0) : lam = 0

The Burnside kill: a character killing all squares and all commutators of K kills all of R = Φ(K).

Slice F11-R2: simplicity of the head (stable-submodule dichotomy)

Mirrors the proven chief-dichotomy skeleton of towerDualInv_zero: a C-stable submodule W with T ≤ W ≤ M has ambient preimage J normal in Y sitting between S and P; chief-ness forces J ⊔ S ∈ {S, P}, giving W = T or W = ⊤. No invariance trick is needed — both cases conclude directly.

def Q2Presentation.Induction.sec7SubmoduleGrp {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (W : Submodule (ZMod 2) (towerM K)) : Subgroup (towerMgrp K)

The multiplicative subgroup of M-classes lying in a submodule W.

Equations

• Q2Presentation.Induction.sec7SubmoduleGrp chief K W = { carrier := {g : Q2Presentation.Induction.towerMgrp K | Additive.ofMul g ∈ W}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem Q2Presentation.Induction.mem_sec7SubmoduleGrp {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {W : Submodule (ZMod 2) (towerM K)} (g : towerMgrp K) : g ∈ sec7SubmoduleGrp chief K W ↔ Additive.ofMul g ∈ W

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

The ambient preimage of a submodule of M inside Y.

Equations

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

theorem Q2Presentation.Induction.sec7SubmoduleAmbient_le {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (W : Submodule (ZMod 2) (towerM K)) : sec7SubmoduleAmbient chief K W ≤ K.Ksub

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

theorem Q2Presentation.Induction.sec7SubmoduleAmbient_normal {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (W : Submodule (ZMod 2) (towerM K)) (hstable : ∀ (c : towerC K), ∀ m ∈ W, ((towerActM K) c) m ∈ W) : (sec7SubmoduleAmbient chief K W).Normal

C-stability makes the ambient preimage normal in Y.

theorem Q2Presentation.Induction.sec7_stable_submodule_dichotomy {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (W : Submodule (ZMod 2) (towerM K)) (hstable : ∀ (c : towerC K), ∀ m ∈ W, ((towerActM K) c) m ∈ W) (hTW : towerT K ≤ W) : W = towerT K ∨ W = ⊤

Head simplicity, upstairs form (lem:simplehead): a C-stable submodule between T and M is T or all of M.

Slice F11-R3: the radical clause from crux-(i) alone

def Q2Presentation.Induction.sec7PolarRadical {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (towerR chief K)) : Submodule (ZMod 2) (towerM K)

The polar radical of the λ-composed form, as a submodule.

Equations

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

theorem Q2Presentation.Induction.sec7_radical_subset_T_of_polarT {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (towerR chief K)) (hlam : lam ≠ 0) (hinv : ∀ (c : towerC K), lam ∘ₗ ↑((towerActR chief K) c) = lam) (hTpolar : ∀ t ∈ towerT K, ∀ (m : towerM K), ((sec7SquareFamily chief K lam).polar t) m = 0) (m : towerM K) (hm : ∀ (m' : towerM K), ((sec7SquareFamily chief K lam).polar m) m' = 0) : m ∈ towerT K

The radical clause of prop:simpleheaddet, PROVEN from clause (i): if the polar form kills T × M, the polar radical lies in T. Head simplicity forces radical ⊔ T ∈ {T, ⊤}; in the ⊤ case the polar form vanishes identically, so q_λ is a C-invariant linear functional, hence 0 (towerDualInv_zero), and the Burnside kill forces λ = 0 — contradiction.

Slice F11-R4: the two-fact crux

structure Q2Presentation.Induction.Sec7SimpleHeadCruxData2 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Prop

The two-fact simple-head crux (prop:simpleheaddet clauses (i)+(ii) only; the radical clause is now THEOREM-level via sec7_radical_subset_T_of_polarT): (i) the socle argument b_λ(T,M) = 0; (ii) the shear/H¹-vanishing q_λ|_T = 0.

• polar_zero_on_T (lam : Module.Dual (ZMod 2) (towerR chief K)) : lam ≠ 0 → (∀ (c : towerC K), lam ∘ₗ ↑((towerActR chief K) c) = lam) → ∀ t ∈ towerT K, ∀ (m : towerM K), ((sec7SquareFamily chief K lam).polar t) m = 0
• form_zero_on_T (lam : Module.Dual (ZMod 2) (towerR chief K)) : lam ≠ 0 → (∀ (c : towerC K), lam ∘ₗ ↑((towerActR chief K) c) = lam) → ∀ t ∈ towerT K, (sec7SquareFamily chief K lam).form t = 0

axiom Q2Presentation.Induction.sec7_simpleHeadCruxData2 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Nonempty (Sec7SimpleHeadCruxData2 chief K)

F11 crux residual — exactly prop:simpleheaddet (i)+(ii).

def Q2Presentation.Induction.sec7SimpleHeadCruxData_of2 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (c2 : Sec7SimpleHeadCruxData2 chief K) : Sec7SimpleHeadCruxData chief K

The three-fact crux, theorem-level from the two-fact crux (the radical clause is supplied by sec7_radical_subset_T_of_polarT).

Equations

• ⋯ = ⋯

Slice F12-a: maps with invariant image into M^∨ vanish

theorem Q2Presentation.Induction.sec7_family_invariant_image_eq_zero {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {W : Type u_1} [AddCommGroup W] [Module (ZMod 2) W] (f : W →ₗ[ZMod 2] Module.Dual (ZMod 2) (towerM K)) (hinvim : ∀ (w : W) (c : towerC K), f w ∘ₗ ↑((towerActM K) c) = f w) : f = 0

A linear family of C-invariant functionals on M is zero (pointwise towerDualInv_zero). This is the engine of the clause-(i) trivial-filtration induction: each trivial layer of T maps into the invariants of M^∨, which vanish.

Slice F12-c: descent along a trivial chain (abstract form)

Given a C-equivariant family f : W →ₗ M^∨ and a finite chain ⊥ = W₀ ≤ W₁ ≤ ⋯ ≤ W_n = ⊤ of C-stable submodules with TRIVIAL layer action (act c w − w ∈ W_i for w ∈ W_{i+1}), the family vanishes: on each layer the image functionals become invariant modulo the inductive hypothesis, and invariant functionals on M are zero (towerDualInv_zero).

theorem Q2Presentation.Induction.sec7_equivariant_family_vanishes_of_trivial_chain {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {W : Type u_1} [AddCommGroup W] [Module (ZMod 2) W] (actW : towerC K →* W ≃ₗ[ZMod 2] W) (f : W →ₗ[ZMod 2] Module.Dual (ZMod 2) (towerM K)) (hequiv : ∀ (c : towerC K) (w : W) (m : towerM K), (f ((actW c) w)) (((towerActM K) c) m) = (f w) m) (n : ℕ) (chain : ℕ → Submodule (ZMod 2) W) (hbot : chain 0 = ⊥) (htop : chain n = ⊤) (htriv : ∀ i < n, ∀ w ∈ chain (i + 1), ∀ (c : towerC K), (actW c) w - w ∈ chain i) : f = 0

Slice F12-d: the adjoint family on T, ready for the chain

def Q2Presentation.Induction.sec7AdjointOnT {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (towerR chief K)) : ↥(towerT K) →ₗ[ZMod 2] Module.Dual (ZMod 2) (towerM K)

The polar adjoint restricted to T, as a linear family into M^∨.

Equations

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

def Q2Presentation.Induction.sec7ActOnT {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (c : towerC K) : ↥(towerT K) ≃ₗ[ZMod 2] ↥(towerT K)

The restricted C-action on T (stability is proven).

Equations

• Q2Presentation.Induction.sec7ActOnT chief K c = ((Q2Presentation.Induction.towerActM K) c).ofSubmodules (Q2Presentation.Induction.towerT K) (Q2Presentation.Induction.towerT K) ⋯

theorem Q2Presentation.Induction.sec7_polar_zero_on_T_of_chain {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (towerR chief K)) (hinv : ∀ (c : towerC K), lam ∘ₗ ↑((towerActR chief K) c) = lam) (actWhom : towerC K →* ↥(towerT K) ≃ₗ[ZMod 2] ↥(towerT K)) (hact : ∀ (c : towerC K) (t : ↥(towerT K)), ↑((actWhom c) t) = ((towerActM K) c) ↑t) (n : ℕ) (chain : ℕ → Submodule (ZMod 2) ↥(towerT K)) (hbot : chain 0 = ⊥) (htop : chain n = ⊤) (htriv : ∀ i < n, ∀ w ∈ chain (i + 1), ∀ (c : towerC K), (actWhom c) w - w ∈ chain i) (t : towerM K) : t ∈ towerT K → ∀ (m : towerM K), ((sec7SquareFamily chief K lam).polar t) m = 0

Clause (i), reduced form: given ANY finite trivial chain on T (the F12-b construction), the polar form kills T × M.

F12-b: construction of the trivial chain on T (below_scalar transport)

theorem Q2Presentation.Induction.sec7ActOnT_coe {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (c : towerC K) (t : ↥(towerT K)) : ↑((sec7ActOnT chief K c) t) = ((towerActM K) c) ↑t

Coe law for the restricted action.

def Q2Presentation.Induction.sec7ActOnTHom {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : towerC K →* ↥(towerT K) ≃ₗ[ZMod 2] ↥(towerT K)

The restricted action as a monoid hom into linear automorphisms of T.

Equations

• Q2Presentation.Induction.sec7ActOnTHom chief K = { toFun := fun (c : Q2Presentation.Induction.towerC K) => Q2Presentation.Induction.sec7ActOnT chief K c, map_one' := ⋯, map_mul' := ⋯ }

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

The ambient subgroup of Y attached to a submodule U ≤ M: elements of K ∩ S whose Frattini image lies in U.

Equations

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

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

theorem Q2Presentation.Induction.sec7ChainAct_ofMul {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (y : p.fst.Y) (k : ↥K.Ksub) : ((towerActM K) ((QuotientGroup.mk' K.Ksub) y)) (Additive.ofMul ((QuotientGroup.mk' (frattini ↥K.Ksub)) k)) = Additive.ofMul ((QuotientGroup.mk' (frattini ↥K.Ksub)) ((kernelConjAut K y) k))

Multiplicative-to-additive bridge for the conjugation action on M.

theorem Q2Presentation.Induction.sec7ChainAmbient_normal {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (U : Submodule (ZMod 2) (towerM K)) (hstab : ∀ (c : towerC K), ∀ m ∈ U, ((towerActM K) c) m ∈ U) : (sec7ChainAmbient chief K U).Normal

The ambient of a C-stable submodule is normal in Y.

theorem Q2Presentation.Induction.sec7_exists_fixed_mod {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (U : Submodule (ZMod 2) (towerM K)) (hUT : U ≤ towerT K) (hstab : ∀ (c : towerC K), ∀ m ∈ U, ((towerActM K) c) m ∈ U) (hne : U ≠ towerT K) : ∃ w ∈ towerT K, w ∉ U ∧ ∀ (c : towerC K), ((towerActM K) c) w - w ∈ U

The step lemma (all below_scalar content): a proper stable submodule of T admits a vector of T outside it that is fixed modulo it.

def Q2Presentation.Induction.sec7ChainM {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : ℕ → Submodule (ZMod 2) (towerM K)

The augmentation filtration in M-coordinates.

Equations

• One or more equations did not get rendered due to their size.
• Q2Presentation.Induction.sec7ChainM chief K 0 = ⊥

theorem Q2Presentation.Induction.sec7ChainM_succ_mem_iff {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (i : ℕ) (m : towerM K) : m ∈ sec7ChainM chief K (i + 1) ↔ m ∈ towerT K ∧ ∀ (c : towerC K), ((towerActM K) c) m - m ∈ sec7ChainM chief K i

theorem Q2Presentation.Induction.sec7ChainM_le_towerT {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (i : ℕ) : sec7ChainM chief K i ≤ towerT K

theorem Q2Presentation.Induction.sec7ChainM_mono {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (i : ℕ) : sec7ChainM chief K i ≤ sec7ChainM chief K (i + 1)

theorem Q2Presentation.Induction.sec7ChainM_stable {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (i : ℕ) (c : towerC K) (m : towerM K) : m ∈ sec7ChainM chief K i → ((towerActM K) c) m ∈ sec7ChainM chief K i

theorem Q2Presentation.Induction.sec7ChainM_top_of_fix {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : sec7ChainM chief K (Module.finrank (ZMod 2) ↥(towerT K) + 1) = towerT K

Slice F12-e: crux clause (i) lowered to pure chain existence

structure Q2Presentation.Induction.Sec7TrivialChainData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Type

A finite C-stable trivial chain on T (pure finite group theory; the manuscript source is below_scalar: all chief factors below S are trivial).

• actWhom : towerC K →* ↥(towerT K) ≃ₗ[ZMod 2] ↥(towerT K)
• hact (c : towerC K) (t : ↥(towerT K)) : ↑((self.actWhom c) t) = ((towerActM K) c) ↑t
• n : ℕ
• chain : ℕ → Submodule (ZMod 2) ↥(towerT K)
• hbot : self.chain 0 = ⊥
• htop : self.chain self.n = ⊤
• htriv (i : ℕ) : i < self.n → ∀ w ∈ self.chain (i + 1), ∀ (c : towerC K), (self.actWhom c) w - w ∈ self.chain i

theorem Q2Presentation.Induction.sec7_trivialChainData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Nonempty (Sec7TrivialChainData chief K)

F12-b (PROVED): the trivial chain on T exists — below_scalar transported through the Frattini quotient via the augmentation filtration.

structure Q2Presentation.Induction.Sec7SimpleHeadCruxData3 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Prop

The final crux for leaf #1: only the shear/H¹ clause (ii) remains as manuscript-analytic content; clause (i) is THEOREM-level from the chain.

• form_zero_on_T (lam : Module.Dual (ZMod 2) (towerR chief K)) : lam ≠ 0 → (∀ (c : towerC K), lam ∘ₗ ↑((towerActR chief K) c) = lam) → ∀ t ∈ towerT K, (sec7SquareFamily chief K lam).form t = 0

def Q2Presentation.Induction.sec7SimpleHeadCruxData2_of3 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (ch : Sec7TrivialChainData chief K) (c3 : Sec7SimpleHeadCruxData3 chief K) : Sec7SimpleHeadCruxData2 chief K

The two-fact crux, theorem-level from the chain + clause (ii).

Equations

• ⋯ = ⋯