Route25 minimal-block kernel/head refinement

Route24 keeps the lower kernel/module tower concrete, but its group-tower provider still closes the simple-head/lower-character layer through three route24 residuals:

• minimalBlock_rawHeadQuotientNoTrivialData;
• minimalBlock_rawHeadSimplicityActualData;
• minimalBlock_rawLowerScalarQuotientData.

This sidecar keeps the same concrete lower tower as Route24 and replaces that head/invariant layer by the finer route10 semantic split already present in the tree:

• invariant functionals on M kill T;
• the quotient head has no invariant dual;
• every nonzero stable quotient-head submodule is top;
• the Frattini layer has a raw nonzero invariant character.

It also avoids Route24's direct concrete head-nonzero residual by deriving the head nontriviality from the same raw tower's not-pointwise-trivial head action, using the existing Route22 theorem-level conversion.

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute25.headDataOfNotPointwiseTrivial {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (D : MinimalBlockKernelModuleConcreteRawData K F) (A : MinimalBlockRawHeadActionNotPointwiseTrivialData D.rawTowerData) : MinimalBlockKernelModuleConcreteHeadData D

Concrete head data from a not-pointwise-trivial quotient-head action on the same raw tower.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute25.rawQuotientOfSplitHeadAction {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (O : MinimalBlockKernelModuleConcreteRawModuleObjectsData K F) (S : MinimalBlockKernelModuleConcreteRawSubquotientObjectsData O) (AR : MinimalBlockKernelModuleConcreteRawFrattiniActionData O S) (AM : MinimalBlockKernelModuleConcreteRawModuleActionData O S) (TS : MinimalBlockKernelModuleConcreteRawTStableData AM) (B : MinimalBlockKernelModuleConcreteBridgeData (MinimalBlockKernelModuleConcreteRawData.ofObjectsActions (MinimalBlockKernelModuleConcreteRawObjectsData.ofModuleSubquotient O S) (MinimalBlockKernelModuleConcreteRawActionsData.ofSplit AR AM TS))) (A : MinimalBlockRawHeadActionNotPointwiseTrivialData (MinimalBlockKernelModuleConcreteRawData.ofObjectsActions (MinimalBlockKernelModuleConcreteRawObjectsData.ofModuleSubquotient O S) (MinimalBlockKernelModuleConcreteRawActionsData.ofSplit AR AM TS)).rawTowerData) : MinimalBlockKernelRawQuotientTowerData K F

Assemble the coherent raw quotient tower while deriving the head-nonzero field from the route21/route22 nontrivial-action leaf, rather than from minimalBlock_kernelModuleConcreteHeadNonzeroData.

Equations

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

Route25 packet and projections

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

Route25 coherent Section 7 kernel/head packet.

The lower tower is the same concrete K, Phi(K), R, M, T, C tower used by Route24. The invariant packet is produced through the route10 semantic split, so the route24 head quotient/simplicity/lower-scalar residual names are not in the final provider's closure.

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

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

The concrete Frattini packet carried by Route25.

Equations

• ⋯ = ⋯

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

The coherent raw data carried by Route25.

Equations

• P.rawData = P.rawQuotient.rawData

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute25Data.route24Data {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute25Data chief) : MinimalBlockKernelConcreteRoute24Data chief

Route24-compatible packet recovered from Route25.

Equations

• P.route24Data = { least := P.least, frattiniFull := ⋯, rawQuotient := id P.rawQuotient, invariantActual := id P.invariantActual }

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

Route25 group-tower data.

Equations

• P.groupTowerData = P.route24Data.groupTowerData

Route25 assembly theorems

theorem Q2Presentation.Induction.minimalBlock_kernelConcreteRoute25Data_from_route10HeadSplit {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelConcreteRoute25Data chief)

Route25 packet from the Route24 concrete tower and the route10 head/invariant semantic split.

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

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