Concrete kernel/module residual split for Section 7

This sidecar does not edit routed files. It strictly narrows the current aggregate packet

minimalBlock_kernelModuleActualProofs : Nonempty (MinimalBlockKernelModuleActualProofs chief)

into the manuscript-shaped obligations on pages 40--42:

• choose the least Y-normal K <= P with K S = P;
• prove the actual Frattini collapse for the literal R = Phi(K), including normality, nontriviality, centrality in K, exponent two, and K^4 = 1;
• extract the raw F_2 objects R, M = K/R, T, C = Y/K and the induced C-actions;
• identify the literal quotient K/Phi(K) with the raw module M;
• prove the simple head M/T is nontrivial.

The route theorem at the bottom is the intended replacement for minimalBlock_lowerGroupModuleData_from_kernelModuleActualProofs when the main route is ready to drop the aggregate axiom.

Narrow concrete packets

structure Q2Presentation.Induction.MinimalBlockKernelModuleConcreteFrattiniData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Prop

Manuscript lem:collapse for the literal Frattini subgroup of the chosen least kernel K.

Compared with MinimalBlockFrattiniCollapseData, this keeps the actual collapse facts that were present in the aggregate packet: centrality in K, K^4 = 1, and exponent two on Phi(K).

• frattini_normal : (Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub)).Normal
• frattini_card_gt_one : 1 < Nat.card ↥(Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub))
• frattini_central_in_K (r : p.fst.Y) : r ∈ Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub) → ∀ k ∈ K.Ksub, r * k = k * r
• K_fourth_eq_one (k : p.fst.Y) : k ∈ K.Ksub → k ^ 4 = 1
• frattini_square_eq_one (r : p.fst.Y) : r ∈ Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub) → r ^ 2 = 1

structure Q2Presentation.Induction.MinimalBlockKernelModuleConcreteRawData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Type 1

The raw quotient objects and actions extracted from the same concrete kernel tower.

This is the Lean form of R = Phi(K), M = K/R, T = (K cap S)/R, C = Y/K, and the induced C-module structures in eq:targettower.

• R : Type
• acgR : AddCommGroup self.R
• modR : Module (ZMod 2) self.R
• finR : Fintype self.R
• deqR : DecidableEq self.R
• M : Type
• acgM : AddCommGroup self.M
• modM : Module (ZMod 2) self.M
• finM : Fintype self.M
• deqM : DecidableEq self.M
• T : Submodule (ZMod 2) self.M
• C : Type
• grpC : Group self.C
• finC : Finite self.C
• actR : self.C →* self.R ≃ₗ[ZMod 2] self.R
• actM : self.C →* self.M ≃ₗ[ZMod 2] self.M
• T_stable (c : self.C) (m : self.M) : m ∈ self.T → (self.actM c) m ∈ self.T

def Q2Presentation.Induction.MinimalBlockKernelModuleConcreteRawData.rawModuleData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (D : MinimalBlockKernelModuleConcreteRawData K F) : MinimalBlockRawModuleData p chief

Forget the concrete provenance to the current raw-module interface.

Equations

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

def Q2Presentation.Induction.MinimalBlockKernelModuleConcreteRawData.rawActionData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (D : MinimalBlockKernelModuleConcreteRawData K F) : MinimalBlockRawActionData D.rawModuleData

Forget the concrete provenance to the current raw-action interface.

Equations

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

def Q2Presentation.Induction.MinimalBlockKernelModuleConcreteRawData.rawTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (D : MinimalBlockKernelModuleConcreteRawData K F) : MinimalBlockRawTowerData p chief

The raw tower assembled from the same raw objects and actions.

Equations

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

structure Q2Presentation.Induction.MinimalBlockKernelModuleConcreteBridgeData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (D : MinimalBlockKernelModuleConcreteRawData K F) : Type

The literal bridge K/Phi(K) ~= M for the same selected K and raw module objects.

• KmodR_equiv_rawM : ↥(Subgroup.map (QuotientGroup.mk' (Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub))) K.Ksub) ≃* Multiplicative D.M

structure Q2Presentation.Induction.MinimalBlockKernelModuleConcreteHeadData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (D : MinimalBlockKernelModuleConcreteRawData K F) : Prop

Nontriviality of the simple head M/T for the same raw tower.

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

Residuals

axiom Q2Presentation.Induction.minimalBlock_kernelModuleConcreteLeastData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelLeastOverChiefData chief)

Residual 1: choose the least K over the selected non-scalar chief factor.

axiom Q2Presentation.Induction.minimalBlock_kernelModuleConcreteFrattiniData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniData K)

Residual 2: prove the actual Frattini-collapse facts for that K.

axiom Q2Presentation.Induction.minimalBlock_kernelModuleConcreteRawData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelModuleConcreteRawData K F)

Residual 3: extract R, M, T, C, and the induced actions from that same subgroup tower.

axiom Q2Presentation.Induction.minimalBlock_kernelModuleConcreteBridgeData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (D : MinimalBlockKernelModuleConcreteRawData K F) : Nonempty (MinimalBlockKernelModuleConcreteBridgeData D)

Residual 4: identify the literal K/Phi(K) quotient with the raw module.

axiom Q2Presentation.Induction.minimalBlock_kernelModuleConcreteHeadData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (D : MinimalBlockKernelModuleConcreteRawData K F) : Nonempty (MinimalBlockKernelModuleConcreteHeadData D)

Residual 5: prove that the simple head M/T is nontrivial.

Assembly into the current aggregate API

theorem Q2Presentation.Induction.minimalBlock_kernelModuleActualProofs_from_concreteProofs {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleActualProofs chief)

Assemble the current aggregate actual packet from the five narrower concrete Section 7 obligations above.

This theorem is route-ready: its axiom closure contains the five concrete residuals, not minimalBlock_kernelModuleActualProofs.

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

Drop-in replacement for minimalBlock_lowerGroupModuleData_from_kernelModuleActualProofs when routing through this concrete split.

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

Least-kernel projection through the concrete route.

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

Frattini-collapse projection through the concrete route.

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

Raw-module projection through the concrete route.

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

Raw-action projection through the concrete route.

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

K/Phi(K) ~= M projection through the concrete route.

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

Simple-head projection through the concrete route.

Acceptance checks