Section 7 kernel/Frattini/raw tower refinement

This sidecar is deliberately route-neutral. It does not use the retired one-point/PUnit shortcut, and it does not replace the P3 frontier by the broad minimalBlock_kernelModuleActualProofs axiom.

Instead it records the literal manuscript tower in two coherent residual packets:

• minimalBlock_kernelFrattiniCollapseFullData: the complete Frattini--centralizer collapse for the selected least K;
• minimalBlock_kernelRawQuotientTowerData: the quotient objects/actions, the K/R ≃ M bridge, and the nonzero head for the same K and R.

Together with the still-explicit least-kernel choice packet minimalBlock_kernelLeastOverChiefData, this removes the ten independent P3 residual calls from downstream route theorems and replaces them by manuscript- shaped same-tower obligations. The remaining proof work is exactly the finite §7 group theory: least K, the Hall/coprime-action Frattini collapse, and the quotient/action transport construction.

Frattini--centralizer collapse for the selected least K

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

The full manuscript lem:collapse package for the literal Frattini subgroup Phi(K) of the selected least kernel K.

This is narrower than MinimalBlockKernelModuleActualProofs: it contains only the five Frattini-collapse facts for the already-selected K, and no raw module, bridge, or head data.

• normalData : MinimalBlockKernelModuleConcreteFrattiniNormalData K
• nontrivialData : MinimalBlockKernelModuleConcreteFrattiniNontrivialData K
• centralData : MinimalBlockKernelModuleConcreteFrattiniCentralData K
• fourthPowerData : MinimalBlockKernelModuleConcreteFourthPowerData K
• exponentData : MinimalBlockKernelModuleConcreteFrattiniExponentData K

def Q2Presentation.Induction.MinimalBlockKernelFrattiniCollapseFullData.frattiniData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (F : MinimalBlockKernelFrattiniCollapseFullData K) : MinimalBlockKernelModuleConcreteFrattiniData K

Forget the coherent Frattini-collapse package to the current concrete Frattini packet.

Equations

• ⋯ = ⋯

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

Residual finite-group input: prove the complete Frattini--centralizer collapse for the selected least K.

This is the Lean frontier corresponding to manuscript lem:collapse: R is central elementary abelian in K, and K^4 = 1.

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

Route-ready Frattini packet from the coherent collapse package.

Raw quotient objects/actions, bridge, and head on the same tower

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

The raw quotient/action/head construction for the same selected tower.

For fixed K and F : Phi(K), this contains exactly the quotient-transport part of manuscript eq:targettower: raw R,M,T,C, induced C-actions, stability of T, the literal K/R ≃ M bridge, and nontriviality of M/T. It is intentionally dependent, so the bridge and head cannot be taken from a different raw object/action choice.

• objects : MinimalBlockKernelModuleConcreteRawObjectsData K F
• actions : MinimalBlockKernelModuleConcreteRawActionsData self.objects
• bridge : MinimalBlockKernelModuleConcreteBridgeData (MinimalBlockKernelModuleConcreteRawData.ofObjectsActions self.objects self.actions)
• head : MinimalBlockKernelModuleConcreteHeadData (MinimalBlockKernelModuleConcreteRawData.ofObjectsActions self.objects self.actions)

def Q2Presentation.Induction.MinimalBlockKernelRawQuotientTowerData.rawData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Q : MinimalBlockKernelRawQuotientTowerData K F) : MinimalBlockKernelModuleConcreteRawData K F

Forget the raw quotient/action package to the current concrete raw-data packet.

Equations

• Q.rawData = Q2Presentation.Induction.MinimalBlockKernelModuleConcreteRawData.ofObjectsActions Q.objects Q.actions

def Q2Presentation.Induction.MinimalBlockKernelRawQuotientTowerData.bridgeData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Q : MinimalBlockKernelRawQuotientTowerData K F) : MinimalBlockKernelModuleConcreteBridgeData Q.rawData

The bridge field, restated over rawData.

Equations

• Q.bridgeData = id Q.bridge

def Q2Presentation.Induction.MinimalBlockKernelRawQuotientTowerData.headData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Q : MinimalBlockKernelRawQuotientTowerData K F) : MinimalBlockKernelModuleConcreteHeadData Q.rawData

The head field, restated over rawData.

Equations

• ⋯ = ⋯

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

Residual finite-group/module input: construct the raw quotient objects/actions, the literal K/R ≃ M bridge, and the nonzero head by quotient-transported conjugation for the same selected tower.

This is the Lean frontier corresponding to manuscript eq:targettower and the nonzero part of lem:simplehead.

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

Route-ready raw-data packet from the coherent raw quotient/action package.

theorem Q2Presentation.Induction.minimalBlock_kernelModuleConcreteBridgeData_from_frattiniRawProofs {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (D : MinimalBlockKernelModuleConcreteRawData K F) (hD : ∃ (Q : MinimalBlockKernelRawQuotientTowerData K F), D = Q.rawData) : Nonempty (MinimalBlockKernelModuleConcreteBridgeData D)

Route-ready bridge packet from the same raw quotient package.

theorem Q2Presentation.Induction.minimalBlock_kernelModuleConcreteHeadData_from_frattiniRawProofs {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (D : MinimalBlockKernelModuleConcreteRawData K F) (hD : ∃ (Q : MinimalBlockKernelRawQuotientTowerData K F), D = Q.rawData) : Nonempty (MinimalBlockKernelModuleConcreteHeadData D)

Route-ready head packet from the same raw quotient package.

Route-level assembly avoiding the ten independent P3 residuals

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

Assemble the current actual kernel/module packet through the P3 refinement.

Axiom closure of this theorem should contain only:

• minimalBlock_kernelLeastOverChiefData,
• minimalBlock_kernelFrattiniCollapseFullData,
• minimalBlock_kernelRawQuotientTowerData,

and not the ten independent P3 packet names from MinimalBlockKernelModuleConcreteClosers2.

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

Lower group/module data through the P3 refinement.

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

Group-tower data through the P3 refinement, leaving the P4 invariant/head refinement exactly where route6 currently leaves it.