Route23 minimal-block kernel/module close-out

Route22 exposed twelve independent Section 7 kernel/module residual calls: least-candidate and least-universal data, split Frattini-collapse conclusions, split raw object/action packets, the concrete K/R ~= M bridge, and four route21 raw head/invariant leaves.

This sidecar keeps the integration files untouched and replaces that exposed surface by four coherent manuscript-shaped packets on one selected tower:

• minimalBlock_kernelLeastOverChiefData, the least K <= P with K S = P;
• minimalBlock_kernelFrattiniCollapseFullData, the full Frattini--centralizer collapse for R = Phi(K);
• minimalBlock_kernelRawQuotientTowerData, the raw R,M,T,C quotient tower, transported actions, concrete K/R ~= M bridge, and nonzero head;
• minimalBlock_headInvariantSemanticRoute12Data, the same-raw-tower simple-head/invariant packet behind the four route21 leaves.

These are not new axioms; they are existing Section 7 packet boundaries already present in the tree. The remaining frontier maps directly to manuscript Section 7: choice of the minimal normal kernel, lem:collapse, eq:targettower, and lem:simplehead.

Forget a coherent raw tower to route22's split raw interface

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute23.moduleObjectsOfRawObjects {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (O : MinimalBlockKernelModuleConcreteRawObjectsData K F) : MinimalBlockKernelModuleConcreteRawModuleObjectsData K F

Split route-independent raw objects into route22's module-object part.

Equations

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

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute23.subquotientObjectsOfRawObjects {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (O : MinimalBlockKernelModuleConcreteRawObjectsData K F) : MinimalBlockKernelModuleConcreteRawSubquotientObjectsData (moduleObjectsOfRawObjects O)

Split route-independent raw objects into route22's subquotient-object part.

Equations

• Q2Presentation.Induction.MinimalBlockKernelConcreteRoute23.subquotientObjectsOfRawObjects O = { T := O.T, C := O.C, grpC := O.grpC, finC := ⋯ }

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute23.frattiniActionOfRawActions {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} {O : MinimalBlockKernelModuleConcreteRawObjectsData K F} (A : MinimalBlockKernelModuleConcreteRawActionsData O) : MinimalBlockKernelModuleConcreteRawFrattiniActionData (moduleObjectsOfRawObjects O) (subquotientObjectsOfRawObjects O)

Project the coherent raw action on R to route22's Frattini-action field.

Equations

• Q2Presentation.Induction.MinimalBlockKernelConcreteRoute23.frattiniActionOfRawActions A = { actR := A.actR }

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute23.moduleActionOfRawActions {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} {O : MinimalBlockKernelModuleConcreteRawObjectsData K F} (A : MinimalBlockKernelModuleConcreteRawActionsData O) : MinimalBlockKernelModuleConcreteRawModuleActionData (moduleObjectsOfRawObjects O) (subquotientObjectsOfRawObjects O)

Project the coherent raw action on M to route22's module-action field.

Equations

• Q2Presentation.Induction.MinimalBlockKernelConcreteRoute23.moduleActionOfRawActions A = { actM := A.actM }

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute23.tStableOfRawActions {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} {O : MinimalBlockKernelModuleConcreteRawObjectsData K F} (A : MinimalBlockKernelModuleConcreteRawActionsData O) : MinimalBlockKernelModuleConcreteRawTStableData (moduleActionOfRawActions A)

Project coherent T-stability to route22's explicit stability field.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute23.rawSplitOfRawQuotient {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Q : MinimalBlockKernelRawQuotientTowerData K F) : MinimalBlockKernelConcreteRoute22RawSplit K F

Route22 raw split recovered from one coherent raw quotient tower.

Equations

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

Route23 packet and projections

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

Route23 coherent Section 7 kernel packet.

Compared with route22, this ties the split residuals back to the manuscript's single tower: one least K, one full Frattini collapse, one raw quotient tower, and one simple-head/invariant packet on that raw tower.

• least : MinimalBlockKernelLeastOverChiefData chief
• frattiniFull : MinimalBlockKernelFrattiniCollapseFullData self.least
• rawQuotient : MinimalBlockKernelRawQuotientTowerData self.least ⋯
• headInvariant : MinimalBlockHeadInvariantSemanticRoute12Data self.rawQuotient.rawData.rawTowerData

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

The concrete Frattini packet carried by route23.

Equations

• ⋯ = ⋯

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

The coherent raw data carried by route23.

Equations

• P.rawData = P.rawQuotient.rawData

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute23Data.rawSplit {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute23Data chief) : MinimalBlockKernelConcreteRoute22RawSplit P.least ⋯

Route22 raw split recovered from route23's coherent raw quotient tower.

Equations

• P.rawSplit = Q2Presentation.Induction.MinimalBlockKernelConcreteRoute23.rawSplitOfRawQuotient P.rawQuotient

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

Route22-compatible packet recovered from route23.

Equations

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

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute23Data.route21Data {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute23Data chief) : MinimalBlockKernelConcreteRoute21Data chief

Route21-compatible packet recovered from route23 via route22.

Equations

• P.route21Data = P.route22Data.route21Data

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

Lower group/module data selected by route23.

Equations

• P.lowerGroupModuleData = P.route22Data.lowerGroupModuleData

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

Head/invariant semantic packet selected by route23.

Equations

• ⋯ = ⋯

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

Route23 group-tower data.

Equations

• P.groupTowerData = P.route22Data.groupTowerData

Route23 assembly theorems

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

Coherent route23 packet from existing Section 7 manuscript-shaped packets.

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

Route22-compatible replacement theorem with route23's smaller axiom surface.

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

Route23 replacement for the route22 group-tower provider.