Kernel-side Section 7 semantic proof packets

This sidecar closes/decomposes the first half of the remaining Section 7 semantic packets:

• minimalBlock_kernelChoiceSemanticData;
• minimalBlock_frattiniKernelSemanticData;
• minimalBlock_moduleExtractionSemanticData;
• minimalBlock_simpleHeadSemanticData.

The non-minimal part of the kernel choice is a theorem: P itself is a Y-normal candidate with P S = P, and the K <= L_Y field follows from K <= P <= L_Y. The downstream interface asks for a least such K, so that leastness is exposed as a narrower finite-group choice packet rather than hidden inside the old semantic axiom.

The remaining packets are reduced to narrower manuscript-shaped packets:

• Frattini collapse: normality and nontriviality of the literal Phi(K) = K^2 [K,K] inside Y;
• module extraction: the raw R,M,T,C objects, the induced actions, and a K/R ~= M bridge;
• simple head: nontrivial head, dual-invariant vanishing, and raw invariant determinant character.

The aggregate theorem at the end reassembles MinimalBlockGroupTowerData without using the four semantic packet axioms listed above.

Kernel choice split

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

A subgroup satisfying the non-minimal part of the manuscript kernel choice: K is Y-normal, lies in P, and maps onto P/S.

This is useful as a theorem-level sanity check: upper itself is always such a candidate. The hard part of the manuscript choice is the leastness/minimality condition, split below as MinimalBlockKernelLeastOverChiefData.

• Ksub : Subgroup p.fst.Y
• Ksub_normal : self.Ksub.Normal
• Ksub_le_upper : self.Ksub ≤ chief.upper
• KS_eq_upper : self.Ksub ⊔ chief.lower = chief.upper

theorem Q2Presentation.Induction.minimalBlock_kernelCandidateData_upper {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelCandidateData chief)

The selected chief-factor upper subgroup is always a kernel candidate.

structure Q2Presentation.Induction.MinimalBlockKernelLeastOverChiefData {p : FramedPair} (chief : NonScalarChiefFactor p) extends Q2Presentation.Induction.MinimalBlockKernelCandidateData chief : Type

Narrow kernel-choice packet: a least candidate over the selected chief factor.

The current downstream semantic packet asks for this leastness as Ksub <= K' for every other candidate K'. That is stronger than mere finite-poset minimality, so it is kept as the finite-group choice content rather than hidden behind a false finite-minimization proof.

• Ksub : Subgroup p.fst.Y
• 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'

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

Residual finite-group choice packet: choose the least Y-normal subgroup K <= P with K S = P.

def Q2Presentation.Induction.MinimalBlockKernelChoiceSemanticData.ofLeastOverChief {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : MinimalBlockKernelChoiceSemanticData p chief

Reassemble the current kernel-choice semantic packet from the least-over-chief packet. The K <= L_Y field is derived from K <= upper <= L_Y.

Equations

• Q2Presentation.Induction.MinimalBlockKernelChoiceSemanticData.ofLeastOverChief K = { Ksub := K.Ksub, Ksub_normal := ⋯, Ksub_le_upper := ⋯, Ksub_le_LY := ⋯, KS_eq_upper := ⋯, minimal_K := ⋯ }

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

Theorem-level replacement for minimalBlock_kernelChoiceSemanticData, reduced to the least-over-chief finite-group packet.

Frattini collapse for the selected kernel

structure Q2Presentation.Induction.MinimalBlockFrattiniCollapseData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelChoiceSemanticData p chief) : Prop

Narrow Frattini-collapse packet for the selected kernel.

The subgroup is not arbitrary: it is definitionally Subgroup.map K.Ksub.subtype (frattini K.Ksub), i.e. the literal Frattini subgroup of K viewed inside Y. What remains is the finite-group content needed by the downstream target tower: normality in Y and nontriviality.

• 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))

axiom Q2Presentation.Induction.minimalBlock_frattiniCollapseData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelChoiceSemanticData p chief) : Nonempty (MinimalBlockFrattiniCollapseData K)

Residual finite-group packet: the literal Frattini subgroup of the selected minimal K is normal in Y and nontrivial.

def Q2Presentation.Induction.MinimalBlockFrattiniKernelSemanticData.ofFrattiniCollapse {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelChoiceSemanticData p chief} (F : MinimalBlockFrattiniCollapseData K) : MinimalBlockFrattiniKernelSemanticData K

Reassemble the current Frattini-kernel semantic packet from the narrower Frattini-collapse packet.

Equations

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

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

Theorem-level replacement for minimalBlock_frattiniKernelSemanticData, with axiom closure reduced to the literal Frattini-collapse packet.

Module extraction from raw tower packets plus the K/R bridge

structure Q2Presentation.Induction.MinimalBlockKmodRBridgeData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelChoiceSemanticData p chief) (R : MinimalBlockFrattiniKernelSemanticData K) (D : MinimalBlockRawModuleData p chief) : Type

The concrete quotient bridge tying the selected subgroup tower to the abstract raw module M.

The raw R,M,T,C objects and the induced actions are already split in MinimalBlockResidualRefinement; this packet records only the remaining identification K/R ~= M.

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

axiom Q2Presentation.Induction.minimalBlock_kmodRBridgeData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelChoiceSemanticData p chief) (R : MinimalBlockFrattiniKernelSemanticData K) (D : MinimalBlockRawModuleData p chief) : Nonempty (MinimalBlockKmodRBridgeData K R D)

Residual finite-group/module bridge: the literal quotient K/R realizes the raw module M.

def Q2Presentation.Induction.MinimalBlockModuleExtractionSemanticData.ofRawActionBridge {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelChoiceSemanticData p chief} {R : MinimalBlockFrattiniKernelSemanticData K} {D : MinimalBlockRawModuleData p chief} (A : MinimalBlockRawActionData D) (B : MinimalBlockKmodRBridgeData K R D) : MinimalBlockModuleExtractionSemanticData K R

Reassemble module extraction from raw module objects, raw actions, and the K/R ~= M bridge.

Equations

• Q2Presentation.Induction.MinimalBlockModuleExtractionSemanticData.ofRawActionBridge A B = { rawModuleData := D, rawActionData := A, KmodR_equiv_rawM := B.KmodR_equiv_rawM }

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

Theorem-level replacement for minimalBlock_moduleExtractionSemanticData, using the existing raw module/action packets and the narrower K/R bridge.

Simple head from its representation-theoretic pieces

def Q2Presentation.Induction.MinimalBlockSimpleHeadSemanticData.ofRawPieces {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelChoiceSemanticData p chief} {R : MinimalBlockFrattiniKernelSemanticData K} {E : MinimalBlockModuleExtractionSemanticData K R} (H : MinimalBlockHeadNontrivialData E.rawTowerData) (V : MinimalBlockDualInvariantVanishesData E.rawTowerData) (X : MinimalBlockRawInvariantCharacterData E.rawTowerData) : MinimalBlockSimpleHeadSemanticData E

Reassemble the simple-head semantic packet from its three existing representation-theoretic components.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.minimalBlock_simpleHeadSemanticData_from_rawPieces {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelChoiceSemanticData p chief} {R : MinimalBlockFrattiniKernelSemanticData K} (E : MinimalBlockModuleExtractionSemanticData K R) : Nonempty (MinimalBlockSimpleHeadSemanticData E)

Theorem-level replacement for minimalBlock_simpleHeadSemanticData, reduced to the nontrivial-head, dual-invariant-vanishing, and raw-character packets.

Aggregate route for the current group-tower packet

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

Reassemble the group-tower packet without using the four semantic packet axioms minimalBlock_kernelChoiceSemanticData, minimalBlock_frattiniKernelSemanticData, minimalBlock_moduleExtractionSemanticData, or minimalBlock_simpleHeadSemanticData.