Actual kernel/module construction packet for Section 7

This sidecar isolates the manuscript construction on pages 40--42 without editing routed files. The current route through MinimalBlockLowerGroupProofs still closes the lower group/module packet by independently invoking six residuals:

• minimalBlock_kernelLeastOverChiefData;
• minimalBlock_frattiniCollapseData;
• minimalBlock_rawModuleData;
• minimalBlock_rawActionData;
• minimalBlock_kmodRBridgeData;
• minimalBlock_headNontrivialData.

The packet below replaces those six independent choices by one actual kernel/module construction: choose the least K over the selected non-scalar chief factor, use the literal Frattini subgroup Phi(K), include the Frattini-collapse facts from lem:collapse, extract M = K/R, T, C, the induced actions, the K/R ~= M bridge, and the nontriviality of the head.

One manuscript-shaped kernel/module construction

structure Q2Presentation.Induction.MinimalBlockKernelModuleActualProofs {p : FramedPair} (chief : NonScalarChiefFactor p) : Type 1

The actual Section 7 kernel/module construction for one non-scalar chief factor.

Unlike MinimalBlockLowerGroupModuleData, this records the subgroup-level Frattini-collapse content directly on the literal subgroup Subgroup.map Ksub.subtype (frattini Ksub). The centrality and exponent fields are not needed to assemble the current route packet, but they are part of the manuscript's lem:collapse content and prevent this residual from being merely a renaming of the older lower packet.

• Ksub : Subgroup p.fst.Y

  The selected least normal subgroup K <= P.

• Ksub_normal : self.Ksub.Normal
• Ksub_le_upper : self.Ksub ≤ chief.upper
• KS_eq_upper : self.Ksub ⊔ chief.lower = chief.upper
• minimal_K (K' : Subgroup p.fst.Y) : K'.Normal → K' ≤ chief.upper → K' ⊔ chief.lower = chief.upper → self.Ksub ≤ K'
• frattini_normal : (Subgroup.map self.Ksub.subtype (frattini ↥self.Ksub)).Normal

  The literal Frattini subgroup R = Phi(K) is normal in Y.

• frattini_card_gt_one : 1 < Nat.card ↥(Subgroup.map self.Ksub.subtype (frattini ↥self.Ksub))

  The Frattini layer is nontrivial.

• frattini_central_in_K (r : p.fst.Y) : r ∈ Subgroup.map self.Ksub.subtype (frattini ↥self.Ksub) → ∀ k ∈ self.Ksub, r * k = k * r

  Manuscript lem:collapse: R centralizes K.

• K_fourth_eq_one (k : p.fst.Y) : k ∈ self.Ksub → k ^ 4 = 1

  Manuscript lem:collapse: K^4 = 1.

• frattini_square_eq_one (r : p.fst.Y) : r ∈ Subgroup.map self.Ksub.subtype (frattini ↥self.Ksub) → r ^ 2 = 1

  Manuscript lem:collapse: the Frattini layer is elementary abelian.

• R : Type

  The additive Frattini layer used by the raw tower.

• acgR : AddCommGroup self.R
• modR : Module (ZMod 2) self.R
• finR : Fintype self.R
• deqR : DecidableEq self.R
• M : Type

  The elementary quotient M = K/R.

• acgM : AddCommGroup self.M
• modM : Module (ZMod 2) self.M
• finM : Fintype self.M
• deqM : DecidableEq self.M
• T : Submodule (ZMod 2) self.M

  The lower scalar part T = (K cap S)/R.

• C : Type

  The lower quotient group C = Y/K.

• grpC : Group self.C
• finC : Finite self.C
• actR : self.C →* self.R ≃ₗ[ZMod 2] self.R

  The induced C-action on the Frattini layer.

• actM : self.C →* self.M ≃ₗ[ZMod 2] self.M

  The induced C-action on M.

• T_stable (c : self.C) (m : self.M) : m ∈ self.T → (self.actM c) m ∈ self.T

  T is a C-submodule of M.

• KmodR_equivM : ↥(Subgroup.map (QuotientGroup.mk' (Subgroup.map self.Ksub.subtype (frattini ↥self.Ksub))) self.Ksub) ≃* Multiplicative self.M

  The literal quotient K/Phi(K) realizes the raw module M.

• head_nontrivial : Nontrivial (self.M ⧸ self.T)

  The first non-scalar head M/T is nonzero.

def Q2Presentation.Induction.MinimalBlockKernelModuleActualProofs.leastKernelData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockKernelModuleActualProofs chief) : MinimalBlockKernelLeastOverChiefData chief

The least-kernel packet projected from the actual construction.

Equations

• D.leastKernelData = { Ksub := D.Ksub, Ksub_normal := ⋯, Ksub_le_upper := ⋯, KS_eq_upper := ⋯, minimal_K := ⋯ }

def Q2Presentation.Induction.MinimalBlockKernelModuleActualProofs.kernelChoice {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockKernelModuleActualProofs chief) : MinimalBlockKernelChoiceSemanticData p chief

The selected semantic kernel K.

Equations

• D.kernelChoice = Q2Presentation.Induction.MinimalBlockKernelChoiceSemanticData.ofLeastOverChief D.leastKernelData

def Q2Presentation.Induction.MinimalBlockKernelModuleActualProofs.frattiniCollapseData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockKernelModuleActualProofs chief) : MinimalBlockFrattiniCollapseData D.kernelChoice

The Frattini-collapse packet for the selected literal Phi(K).

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelModuleActualProofs.frattiniKernel {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockKernelModuleActualProofs chief) : MinimalBlockFrattiniKernelSemanticData D.kernelChoice

The selected semantic Frattini subgroup R = Phi(K).

Equations

• D.frattiniKernel = Q2Presentation.Induction.MinimalBlockFrattiniKernelSemanticData.ofFrattiniCollapse ⋯

def Q2Presentation.Induction.MinimalBlockKernelModuleActualProofs.rawModuleData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockKernelModuleActualProofs chief) : MinimalBlockRawModuleData p chief

The raw finite F_2-module objects extracted from the actual construction.

Equations

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

def Q2Presentation.Induction.MinimalBlockKernelModuleActualProofs.rawActionData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockKernelModuleActualProofs chief) : MinimalBlockRawActionData D.rawModuleData

The induced quotient actions extracted from the actual construction.

Equations

• D.rawActionData = { actR := D.actR, actM := D.actM, T_stable := ⋯ }

def Q2Presentation.Induction.MinimalBlockKernelModuleActualProofs.rawTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockKernelModuleActualProofs chief) : MinimalBlockRawTowerData p chief

The raw tower associated to the actual construction.

Equations

• D.rawTowerData = Q2Presentation.Induction.MinimalBlockRawTowerData.ofModuleAction D.rawModuleData D.rawActionData

def Q2Presentation.Induction.MinimalBlockKernelModuleActualProofs.kmodRBridgeData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockKernelModuleActualProofs chief) : MinimalBlockKmodRBridgeData D.kernelChoice D.frattiniKernel D.rawModuleData

The quotient bridge K/Phi(K) ~= M for the selected construction.

Equations

• D.kmodRBridgeData = { KmodR_equiv_rawM := id D.KmodR_equivM }

def Q2Presentation.Induction.MinimalBlockKernelModuleActualProofs.headNontrivialData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockKernelModuleActualProofs chief) : MinimalBlockHeadNontrivialData D.rawTowerData

The nontrivial-head packet for the selected raw tower.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelModuleActualProofs.lowerGroupModuleData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockKernelModuleActualProofs chief) : MinimalBlockLowerGroupModuleData chief

Assemble the existing coherent lower packet from the actual construction.

Equations

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

Residual and route projections

axiom Q2Presentation.Induction.minimalBlock_kernelModuleActualProofs {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleActualProofs chief)

Remaining finite group/module proof obligation for manuscript Section 7.

This is intentionally one packet, not six independently chosen packets. Its fields are the actual least-kernel, Frattini-collapse, module-extraction, quotient-bridge, and simple-head construction described in the manuscript.

theorem Q2Presentation.Induction.minimalBlock_lowerGroupModuleData_from_kernelModuleActualProofs {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockLowerGroupModuleData chief)

Route theorem replacing the six lower kernel/module residuals by the one actual construction packet.

theorem Q2Presentation.Induction.minimalBlock_kernelLeastOverChiefData_from_kernelModuleActualProofs {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelLeastOverChiefData chief)

Projection to the old least-kernel packet, for closure comparison.

theorem Q2Presentation.Induction.minimalBlock_frattiniCollapseData_from_kernelModuleActualProofs {p : FramedPair} (chief : NonScalarChiefFactor p) : ∃ (K : MinimalBlockKernelChoiceSemanticData p chief), Nonempty (MinimalBlockFrattiniCollapseData K)

Projection to the old Frattini-collapse packet on the canonical selected K.

theorem Q2Presentation.Induction.minimalBlock_rawModuleData_from_kernelModuleActualProofs {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockRawModuleData p chief)

Projection to the old raw-module packet.

theorem Q2Presentation.Induction.minimalBlock_rawActionData_from_kernelModuleActualProofs {p : FramedPair} (chief : NonScalarChiefFactor p) : ∃ (D : MinimalBlockRawModuleData p chief), Nonempty (MinimalBlockRawActionData D)

Projection to the old raw-action packet on the canonical raw module.

theorem Q2Presentation.Induction.minimalBlock_kmodRBridgeData_from_kernelModuleActualProofs {p : FramedPair} (chief : NonScalarChiefFactor p) : ∃ (K : MinimalBlockKernelChoiceSemanticData p chief) (R : MinimalBlockFrattiniKernelSemanticData K) (D : MinimalBlockRawModuleData p chief), Nonempty (MinimalBlockKmodRBridgeData K R D)

Projection to the old K/R ~= M bridge packet on the canonical tower.

theorem Q2Presentation.Induction.minimalBlock_headNontrivialData_from_kernelModuleActualProofs {p : FramedPair} (chief : NonScalarChiefFactor p) : ∃ (D : MinimalBlockRawTowerData p chief), Nonempty (MinimalBlockHeadNontrivialData D)

Projection to the old head-nontrivial packet on the canonical raw tower.