Route24 minimal-block kernel/head close-out

Route23 reduced the current Section 7 minimal-block frontier to four coherent manuscript packets:

• minimalBlock_kernelLeastOverChiefData: choose the least normal K <= P with K S = P;
• minimalBlock_kernelFrattiniCollapseFullData: lem:collapse, the Frattini--centralizer collapse for R = Phi(K);
• minimalBlock_kernelRawQuotientTowerData: eq:targettower, the raw quotient tower R, M = K/R, T, C, transported actions, bridge, and nonzero head;
• minimalBlock_headInvariantSemanticRoute12Data: lem:simplehead, the simple-head and invariant-character consequences on that same raw tower.

This Route24 sidecar keeps the integration/root files untouched and does not add new axioms. It proves the Route23-shaped packet from finer current APIs already present in the tree, so the exported group-tower theorem no longer has the four Route23 aggregate residual names in its axiom closure. The remaining residuals are the narrower Section 7 leaves for least K, lem:collapse, eq:targettower, and the simple-head/lower-scalar layer.

Convert the actual same-tower invariant packet to Route12 semantics

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute24.headInvariantOfInvariantActual {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (S : MinimalBlockInvariantActualProofs2Data D) : MinimalBlockHeadInvariantSemanticRoute12Data D

Route12 head/invariant semantic data from the actual same-raw-tower invariant packet.

Manuscript anchors:

• lem:simplehead: invariant kernels contain T, and every nonzero stable quotient-head submodule is the whole head;
• first non-scalar head: the quotient-head action is not pointwise trivial;
• lower scalar layer: the Frattini layer has a nonzero invariant character.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute24.actualProofsOfRawQuotient {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (Ffull : MinimalBlockKernelFrattiniCollapseFullData K) (Q : MinimalBlockKernelRawQuotientTowerData K ⋯) : MinimalBlockKernelModuleActualProofs chief

Assemble the aggregate actual kernel/module packet from one Route24-selected least kernel, Frattini-collapse packet, and raw quotient tower.

This helper is theorem-level glue only; it introduces no residual boundary of its own.

Equations

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

Route24 packet and projections

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

Route24 coherent Section 7 kernel/head packet.

Compared with Route23, the fourth field records the actual invariant packet on the selected raw tower. The Route12 semantic head/invariant packet is then derived theorem-level by headInvariantOfInvariantActual.

• least : MinimalBlockKernelLeastOverChiefData chief
• frattiniFull : MinimalBlockKernelFrattiniCollapseFullData self.least
• rawQuotient : MinimalBlockKernelRawQuotientTowerData self.least ⋯
• invariantActual : MinimalBlockInvariantActualProofs2Data self.rawQuotient.rawData.rawTowerData

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute24Data.frattiniData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute24Data chief) : MinimalBlockKernelModuleConcreteFrattiniData P.least

The concrete Frattini packet carried by Route24.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute24Data.rawData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute24Data chief) : MinimalBlockKernelModuleConcreteRawData P.least ⋯

The coherent raw data carried by Route24.

Equations

• P.rawData = P.rawQuotient.rawData

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute24Data.headInvariantSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute24Data chief) : MinimalBlockHeadInvariantSemanticRoute12Data P.rawData.rawTowerData

The Route12 head/invariant semantic packet derived from Route24's actual same-tower invariant packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute24Data.route23Data {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute24Data chief) : MinimalBlockKernelConcreteRoute23Data chief

Route23-compatible packet recovered from Route24.

Equations

• P.route23Data = { least := P.least, frattiniFull := ⋯, rawQuotient := id P.rawQuotient, headInvariant := ⋯ }

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute24Data.route22Data {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute24Data chief) : MinimalBlockKernelConcreteRoute22Data chief

Route22-compatible packet recovered from Route24 through Route23.

Equations

• P.route22Data = P.route23Data.route22Data

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute24Data.lowerGroupModuleData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute24Data chief) : MinimalBlockLowerGroupModuleData chief

Lower group/module data selected by Route24.

Equations

• P.lowerGroupModuleData = P.route23Data.lowerGroupModuleData

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute24Data.groupTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute24Data chief) : MinimalBlockGroupTowerData p chief

Route24 group-tower data.

Equations

• P.groupTowerData = P.route23Data.groupTowerData

Route24 assembly theorems

theorem Q2Presentation.Induction.minimalBlock_kernelConcreteRoute24Data_from_finerPackets {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelConcreteRoute24Data chief)

Route24 packet from finer/current Section 7 APIs.

This proves the Route23-shaped close-out without using the four Route23 aggregate residual names. Remaining residuals are finer manuscript-shaped packets:

• least K: candidate plus universal leastness;
• lem:collapse: centrality, fourth-power, exponent, and nonidentity Frattini facts;
• eq:targettower: raw module/subquotient objects, transported actions, T-stability, quotient bridge, and head nonzero witness;
• lem:simplehead: no-trivial-dual, head simplicity, and lower scalar quotient on the same raw tower.

theorem Q2Presentation.Induction.minimalBlock_kernelConcreteRoute23Data_from_kernelConcreteRoute24 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelConcreteRoute23Data chief)

Route23-compatible replacement theorem proved through Route24's finer current APIs.

theorem Q2Presentation.Induction.minimalBlock_kernelConcreteRoute22Data_from_kernelConcreteRoute24 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelConcreteRoute22Data chief)

Route22-compatible replacement theorem proved through Route24.

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

Route24 replacement for the current minimal-block group-tower provider.