Lower group/module proof packet for Section 7

This sidecar refines the lower GROUP-TOWER/MODULE part of the Section 7 minimal-block closure. It does not edit the routed proof files.

Manuscript anchors: reference/q2_manuscript.tex, Section 7, pages 40--42: eq:targettower, the choice of minimal K, R = Phi(K) = K^2 [K,K], M = K/R, T = (K cap S)/R, the lower quotient C = Y/K, and lem:simplehead.

The current final closure exposes six independent residuals:

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

The packet below replaces those by one coherent finite group/module object for the canonical chain: the same least K supplies the literal Frattini subgroup, the raw module/action data, the K/R ~= M bridge, and the nonzero simple head. This is stricter than the previous split because downstream users cannot mix unrelated choices of K, R, M, actions, and head data.

One coherent lower tower/module packet

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

Coherent lower Section 7 group/module data for one non-scalar chief factor.

The fields are exactly the lower tower/module facts from eq:targettower and lem:simplehead, but tied to the same canonical dependency chain:

• a least Y-normal K <= P with K S = P;
• the literal Frattini subgroup R = Phi(K) with collapse facts;
• the finite F_2 objects R, M = K/R, T, C;
• the induced C-actions and stability of T;
• the quotient bridge from the literal K/R to the raw module M;
• nontriviality of the simple head M/T.

• leastKernel : MinimalBlockKernelLeastOverChiefData chief
• frattiniCollapse : MinimalBlockFrattiniCollapseData (MinimalBlockKernelChoiceSemanticData.ofLeastOverChief self.leastKernel)
• rawModuleData : MinimalBlockRawModuleData p chief
• rawActionData : MinimalBlockRawActionData self.rawModuleData
• kmodRBridgeData : MinimalBlockKmodRBridgeData (MinimalBlockKernelChoiceSemanticData.ofLeastOverChief self.leastKernel) (MinimalBlockFrattiniKernelSemanticData.ofFrattiniCollapse ⋯) self.rawModuleData
• headNontrivialData : MinimalBlockHeadNontrivialData (MinimalBlockRawTowerData.ofModuleAction self.rawModuleData self.rawActionData)

axiom Q2Presentation.Induction.minimalBlock_lowerGroupModuleData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockLowerGroupModuleData chief)

Residual lower Section 7 finite group/module packet.

This single packet is the new target for the six lower residuals. It is coherent by construction: all components are fields of one tower rather than separately chosen axioms.

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

The selected semantic K obtained from the least-kernel field.

Equations

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

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

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

Equations

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

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

The raw tower assembled from the coherent raw module and action fields.

Equations

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

def Q2Presentation.Induction.MinimalBlockLowerGroupModuleData.moduleExtraction {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockLowerGroupModuleData chief) : MinimalBlockModuleExtractionSemanticData D.kernelChoice D.frattiniKernel

The semantic module extraction M = K/R, T, C, actions, and bridge.

Equations

• D.moduleExtraction = { rawModuleData := D.rawModuleData, rawActionData := D.rawActionData, KmodR_equiv_rawM := D.kmodRBridgeData.KmodR_equiv_rawM }

def Q2Presentation.Induction.MinimalBlockLowerGroupModuleData.simpleHeadSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockLowerGroupModuleData chief) (V : MinimalBlockDualInvariantVanishesData D.rawTowerData) (X : MinimalBlockRawInvariantCharacterData D.rawTowerData) : MinimalBlockSimpleHeadSemanticData D.moduleExtraction

Install the remaining simple-head representation pieces over the coherent lower tower. The head nontriviality comes from this packet; dual-invariant vanishing and the determinant character are still separate Section 7 residuals outside the lower group/module list handled here.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockLowerGroupModuleData.groupTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockLowerGroupModuleData chief) (V : MinimalBlockDualInvariantVanishesData D.rawTowerData) (X : MinimalBlockRawInvariantCharacterData D.rawTowerData) : MinimalBlockGroupTowerData p chief

Reassemble the existing MinimalBlockGroupTowerData from the coherent lower packet plus the two still-separate simple-head/character residuals.

Equations

• D.groupTowerData V X = Q2Presentation.Induction.MinimalBlockGroupTowerData.ofSemantic D.kernelChoice D.frattiniKernel D.moduleExtraction ⋯

Projection/replacement theorems for the six lower residuals

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

Replacement for the least-kernel residual.

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

Replacement for the Frattini-collapse residual, with the canonical K exposed existentially.

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

Replacement for the raw module residual.

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

Replacement for the raw action residual, with the canonical raw module exposed existentially.

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

Replacement for the literal K/R ~= M bridge residual, with the canonical K, R, and raw module exposed existentially.

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

Replacement for the nontrivial simple-head residual, with the canonical raw tower exposed existentially.

Canonical semantic lower packets from the same data

theorem Q2Presentation.Induction.minimalBlock_kernelChoiceSemanticData_from_lowerGroupModuleData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelChoiceSemanticData p chief)

The kernel-choice semantic packet from the coherent lower packet.

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

The Frattini-kernel semantic packet from the coherent lower packet.

theorem Q2Presentation.Induction.minimalBlock_moduleExtractionSemanticData_from_lowerGroupModuleData {p : FramedPair} (chief : NonScalarChiefFactor p) : ∃ (K : MinimalBlockKernelChoiceSemanticData p chief) (R : MinimalBlockFrattiniKernelSemanticData K), Nonempty (MinimalBlockModuleExtractionSemanticData K R)

The module-extraction semantic packet from the coherent lower packet.

theorem Q2Presentation.Induction.minimalBlock_groupTowerData_from_lowerGroupModuleData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupTowerData p chief)

Reassemble MinimalBlockGroupTowerData while avoiding all six lower group/module residual axioms. The closure still contains the two separate simple-head/character packets not targeted by this sidecar: minimalBlock_dualInvariantVanishesData and minimalBlock_rawInvariantCharacterData.

Acceptance checks