Route22 minimal-block kernel concrete close-out

Route21 exposed the Section 7 kernel/head contribution as ten field-level residuals. This sidecar keeps the route21 head leaves, but replaces the lower kernel/module part by the sharper concrete tower already present in the tree:

• least K is split into a candidate plus universal leastness;
• the Frattini collapse is the literal Phi(K) collapse packet;
• raw R, M, T, C objects/actions are quotient-transported pieces;
• the K/R ~= M bridge is the concrete quotient equivalence.

The standalone route21 minimalBlock_headNontrivialData residual is removed: nontriviality of M/T follows from the route21 quotient-head action not being pointwise trivial.

Route22 raw split for the lower concrete tower

structure Q2Presentation.Induction.MinimalBlockKernelConcreteRoute22RawSplit {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Type 1

The quotient-object/action split for the selected concrete K, Phi(K) tower.

• moduleObjects : MinimalBlockKernelModuleConcreteRawModuleObjectsData K F
• subquotientObjects : MinimalBlockKernelModuleConcreteRawSubquotientObjectsData self.moduleObjects
• frattiniAction : MinimalBlockKernelModuleConcreteRawFrattiniActionData self.moduleObjects self.subquotientObjects
• moduleAction : MinimalBlockKernelModuleConcreteRawModuleActionData self.moduleObjects self.subquotientObjects
• tStable : MinimalBlockKernelModuleConcreteRawTStableData self.moduleAction

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute22RawSplit.rawObjects {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (S : MinimalBlockKernelConcreteRoute22RawSplit K F) : MinimalBlockKernelModuleConcreteRawObjectsData K F

Raw R, M, T, C objects for the split.

Equations

• S.rawObjects = Q2Presentation.Induction.MinimalBlockKernelModuleConcreteRawObjectsData.ofModuleSubquotient S.moduleObjects S.subquotientObjects

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute22RawSplit.rawActions {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (S : MinimalBlockKernelConcreteRoute22RawSplit K F) : MinimalBlockKernelModuleConcreteRawActionsData S.rawObjects

Induced raw actions for the split.

Equations

• S.rawActions = id (Q2Presentation.Induction.MinimalBlockKernelModuleConcreteRawActionsData.ofSplit S.frattiniAction S.moduleAction ⋯)

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute22RawSplit.rawData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (S : MinimalBlockKernelConcreteRoute22RawSplit K F) : MinimalBlockKernelModuleConcreteRawData K F

Concrete raw tower data assembled from the split.

Equations

• S.rawData = Q2Presentation.Induction.MinimalBlockKernelModuleConcreteRawData.ofObjectsActions S.rawObjects S.rawActions

Head nontriviality is forced by nontrivial action

theorem Q2Presentation.Induction.minimalBlock_route22_headNontrivialData_from_notPointwiseTrivial {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) (A : MinimalBlockRawHeadActionNotPointwiseTrivialData D) : MinimalBlockHeadNontrivialData D

Route22 closes the standalone route21 head-nontrivial residual from the not-pointwise-trivial head-action leaf.

Route22 packet and projections

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

Route22 coherent Section 7 kernel packet.

Compared with route21, the lower six fields are replaced by the concrete same-tower split above. The four head/invariant leaves remain field-level and are attached to the raw tower determined by that lower split.

• least : MinimalBlockKernelLeastOverChiefData chief
• frattiniFull : MinimalBlockKernelFrattiniCollapseFullData self.least
• rawSplit : MinimalBlockKernelConcreteRoute22RawSplit self.least ⋯
• bridgeData : MinimalBlockKernelModuleConcreteBridgeData self.rawSplit.rawData
• invariantHyperplanesContainT : MinimalBlockRawInvariantHyperplanesContainTData self.rawSplit.rawData.rawTowerData
• headNonzeroStableEqTop : MinimalBlockRawHeadNonzeroStableEqTopData self.rawSplit.rawData.rawTowerData
• headActionNotPointwiseTrivial : MinimalBlockRawHeadActionNotPointwiseTrivialData self.rawSplit.rawData.rawTowerData
• lowerInvariantCharacterExists : MinimalBlockRawLowerInvariantCharacterExistsData self.rawSplit.rawData.rawTowerData

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

The concrete Frattini packet carried by route22.

Equations

• ⋯ = ⋯

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

The concrete raw-data packet selected by route22.

Equations

• P.rawData = P.rawSplit.rawData

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute22Data.rawModuleData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute22Data chief) : MinimalBlockRawModuleData p chief

Forget the concrete raw objects to the route21 raw-module interface.

Equations

• P.rawModuleData = P.rawData.rawModuleData

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute22Data.rawActionData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute22Data chief) : MinimalBlockRawActionData P.rawModuleData

Forget the concrete actions to the route21 raw-action interface.

Equations

• P.rawActionData = P.rawData.rawActionData

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute22Data.rawTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute22Data chief) : MinimalBlockRawTowerData p chief

The raw tower forced by the route22 concrete lower split.

Equations

• P.rawTowerData = P.rawData.rawTowerData

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute22Data.kernelChoice {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute22Data chief) : MinimalBlockKernelChoiceSemanticData p chief

The selected semantic K.

Equations

• P.kernelChoice = Q2Presentation.Induction.MinimalBlockKernelChoiceSemanticData.ofLeastOverChief P.least

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute22Data.frattiniCollapseData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute22Data chief) : MinimalBlockFrattiniCollapseData P.kernelChoice

The semantic Frattini-collapse data obtained from the concrete full collapse.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute22Data.frattiniKernel {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute22Data chief) : MinimalBlockFrattiniKernelSemanticData P.kernelChoice

The selected semantic R = Phi(K).

Equations

• P.frattiniKernel = Q2Presentation.Induction.MinimalBlockFrattiniKernelSemanticData.ofFrattiniCollapse ⋯

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute22Data.kmodRBridgeData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute22Data chief) : MinimalBlockKmodRBridgeData P.kernelChoice P.frattiniKernel P.rawModuleData

Route21's semantic K/R ~= M bridge, projected from the concrete quotient equivalence on the same raw tower.

Equations

• P.kmodRBridgeData = { KmodR_equiv_rawM := id P.bridgeData.KmodR_equiv_rawM }

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute22Data.headNontrivialData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute22Data chief) : MinimalBlockHeadNontrivialData P.rawTowerData

Route21's nontrivial-head field, derived rather than assumed.

Equations

• ⋯ = ⋯

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

Route21-compatible packet recovered from route22.

Equations

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

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

Lower group/module data selected by route22.

Equations

• P.lowerGroupModuleData = P.route21Data.lowerGroupModuleData

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

Head/invariant semantic packet selected by route22.

Equations

• ⋯ = ⋯

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

Route22 group-tower data.

Equations

• P.groupTowerData = P.route21Data.groupTowerData

Route22 assembly theorems

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

Route22 same-tower packet assembled from concrete lower packets and the four route21 head leaves.

theorem Q2Presentation.Induction.minimalBlock_kernelConcreteRoute21Data_from_kernelConcreteRoute22 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelConcreteRoute21Data chief)

Route22 replacement for route21's packet target.

theorem Q2Presentation.Induction.minimalBlock_lowerGroupModuleData_from_kernelConcreteRoute22 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockLowerGroupModuleData chief)

Lower group/module data through route22.

theorem Q2Presentation.Induction.minimalBlock_headInvariantSemanticRoute12Data_from_kernelConcreteRoute22 {p : FramedPair} (chief : NonScalarChiefFactor p) : ∃ (D : MinimalBlockRawTowerData p chief), Nonempty (MinimalBlockHeadInvariantSemanticRoute12Data D)

Route21 head/invariant semantic target, tied to the route22-selected raw tower.

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

Route22 group-tower provider, suitable for later route integration in place of minimalBlock_groupTowerData_from_kernelConcreteRoute21.