Route28 minimal-block kernel/head refinement

Route27 keeps the concrete K, Phi(K), R, M, T, C tower split into the current Section 7 kernel/module leaves, and uses the monolithic same-raw-tower packet minimalBlock_invariantActualProofs2Data to obtain the final head/invariant interface.

This sidecar keeps the downstream shape of route27 but replaces that monolithic invariant call by theorem-level assembly from the manuscript-shaped head split:

• minimalBlock_rawHeadQuotientNoTrivialData;
• minimalBlock_rawHeadSimplicityActualData;
• minimalBlock_rawLowerScalarQuotientData;
• the nonzero head already carried by the selected lower tower.

Manuscript anchors: Section 7, pages 40--42, especially eq:targettower, lem:simplehead, and the paragraph after the choice of the least normal K <= P with K S = P.

No new axioms are introduced here.

Actual invariant packet from the smaller same-lower-tower split

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute28.invariantActualOfLowerHeadSplit {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockLowerGroupModuleData chief) (H : MinimalBlockRawHeadQuotientNoTrivialData D.rawTowerData) (S : MinimalBlockRawHeadSimplicityActualData D.rawTowerData) (Q : MinimalBlockRawLowerScalarQuotientData D.rawTowerData) : MinimalBlockInvariantActualProofs2Data D.rawTowerData

Assemble the route27 actual invariant packet from the smaller Section 7 simple-head/lower-character data on the same selected lower tower.

Equations

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

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute28.minimalBlock_invariantActualProofs2Data_from_route28HeadSplit {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockLowerGroupModuleData chief) : Nonempty (MinimalBlockInvariantActualProofs2Data D.rawTowerData)

Route28 replacement for the route27 monolithic actual invariant residual.

The nonzero-head witness is taken from the same lower tower, so this adapter does not call the standalone minimalBlock_headNontrivialData residual and does not call minimalBlock_invariantActualProofs2Data.

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute28.headInvariantOfRoute28Actual {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (A : MinimalBlockInvariantActualProofs2Data D) : MinimalBlockHeadInvariantSemanticRoute12Data D

Route12 head/invariant semantic data from the route28 actual packet.

Equations

• ⋯ = ⋯

Route28 packet and projections

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

Route28 coherent Section 7 kernel/head packet.

The lower concrete tower is the same route27 tower. The final head/invariant component is stored as the actual same-tower packet, but route28 constructs it from the smaller head split above rather than from the route27 monolithic axiom.

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

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

The concrete Frattini packet carried by Route28.

Equations

• ⋯ = ⋯

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

The coherent raw data carried by Route28.

Equations

• P.rawData = P.rawQuotient.rawData

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute28Data.actualProofs {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute28Data chief) : MinimalBlockKernelModuleActualProofs chief

The actual lower kernel/module packet selected by Route28.

Equations

• P.actualProofs = Q2Presentation.Induction.MinimalBlockKernelConcreteRoute24.actualProofsOfRawQuotient P.least ⋯ P.rawQuotient

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

Lower group/module data selected by Route28.

Equations

• P.lowerGroupModuleData = P.actualProofs.lowerGroupModuleData

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

Route12 semantic head/invariant packet recovered from Route28.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute28Data.route20Data {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute28Data chief) : MinimalBlockKernelConcreteRoute20Data chief

Route20-compatible same-tower packet recovered from Route28.

Equations

• P.route20Data = { lower := P.lowerGroupModuleData, headInvariant := ⋯ }

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

Route28 group-tower data.

Equations

• P.groupTowerData = P.route20Data.groupTowerData

Route28 assembly theorems

theorem Q2Presentation.Induction.minimalBlock_kernelConcreteRoute28Data_from_headSplit {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelConcreteRoute28Data chief)

Route28 packet from the route27 lower tower and the smaller same-tower simple-head/lower-character split.

This keeps the concrete kernel/module construction on the same selected tower, but the axiom closure replaces minimalBlock_invariantActualProofs2Data by the finer Section 7 head split used by MinimalBlockKernelConcreteRoute28.minimalBlock_invariantActualProofs2Data_from_route28HeadSplit.

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

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