Route21 minimal-block kernel concrete semantic split

This sidecar is route-neutral: it does not edit the integrated routes or any existing route file. Route20 exposes the Section 7 kernel contribution through two aggregate residuals:

• minimalBlock_lowerGroupModuleData;
• minimalBlock_headInvariantSemanticRoute12Data.

Route21 replaces those aggregate uses by a same-tower fine packet. The lower tower is assembled from the six manuscript-shaped lower inputs already present in the tree, and the head/invariant semantic packet is split into its four field-level Section 7 statements on the selected raw tower.

Four field-level head/invariant residuals

axiom Q2Presentation.Induction.minimalBlock_route21_rawInvariantHyperplanesContainTData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawInvariantHyperplanesContainTData D)

Route21 head leaf: invariant hyperplanes in M contain the lower layer T.

Manuscript anchor: the minimality argument in lem:simplehead, used to show that invariant functionals on M vanish on T.

axiom Q2Presentation.Induction.minimalBlock_route21_rawHeadNonzeroStableEqTopData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadNonzeroStableEqTopData D)

Route21 head leaf: every nonzero stable submodule of the quotient head is the whole head.

Manuscript anchor: the simple-head assertion in lem:simplehead.

axiom Q2Presentation.Induction.minimalBlock_route21_rawHeadActionNotPointwiseTrivialData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadActionNotPointwiseTrivialData D)

Route21 head leaf: the quotient-head action is not pointwise trivial.

Manuscript anchor: the first non-scalar chief factor in Section 7.

axiom Q2Presentation.Induction.minimalBlock_route21_rawLowerInvariantCharacterExistsData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawLowerInvariantCharacterExistsData D)

Route21 lower-Frattini leaf: the lower Frattini layer has a nonzero C-invariant character.

Manuscript anchor: the scalar lower layer used in the determinant pushout.

Same-tower route21 packet

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

Route21 coherent Section 7 kernel packet.

The fields are deliberately finer than the two route20 residuals. The first six fields build the lower tower K, R = Phi(K), M, T, C and the literal K/R ~= M bridge. The last four fields are exactly the route12 head/invariant semantic facts, but attached to the raw tower selected by those lower fields.

• leastKernel : MinimalBlockKernelLeastOverChiefData chief
• frattiniCollapse : MinimalBlockFrattiniCollapseData (MinimalBlockKernelChoiceSemanticData.ofLeastOverChief self.leastKernel)
• rawModuleData : MinimalBlockRawModuleData p chief
• rawActionData : MinimalBlockRawActionData self.rawModuleData
• kmodRBridgeData : MinimalBlockKmodRBridgeData (MinimalBlockKernelChoiceSemanticData.ofLeastOverChief self.leastKernel) (MinimalBlockFrattiniKernelSemanticData.ofFrattiniCollapse ⋯) self.rawModuleData
• headNontrivialData : MinimalBlockHeadNontrivialData (MinimalBlockRawTowerData.ofModuleAction self.rawModuleData self.rawActionData)
• invariantHyperplanesContainT : MinimalBlockRawInvariantHyperplanesContainTData (MinimalBlockRawTowerData.ofModuleAction self.rawModuleData self.rawActionData)
• headNonzeroStableEqTop : MinimalBlockRawHeadNonzeroStableEqTopData (MinimalBlockRawTowerData.ofModuleAction self.rawModuleData self.rawActionData)
• headActionNotPointwiseTrivial : MinimalBlockRawHeadActionNotPointwiseTrivialData (MinimalBlockRawTowerData.ofModuleAction self.rawModuleData self.rawActionData)
• lowerInvariantCharacterExists : MinimalBlockRawLowerInvariantCharacterExistsData (MinimalBlockRawTowerData.ofModuleAction self.rawModuleData self.rawActionData)

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

The selected semantic K obtained from the route21 least-kernel leaf.

Equations

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

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

The selected semantic Frattini subgroup R = Phi(K).

Equations

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

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

The raw tower selected by the route21 lower fields.

Equations

• P.rawTowerData = Q2Presentation.Induction.MinimalBlockRawTowerData.ofModuleAction P.rawModuleData P.rawActionData

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

Route20's lower aggregate, reconstructed from route21's six lower leaves.

Equations

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

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

Route20's head/invariant aggregate, reconstructed from route21's four field-level head leaves on the same selected raw tower.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute21Data.invariantFunctionalsKillTData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute21Data chief) : MinimalBlockRawInvariantFunctionalsKillTData P.rawTowerData

Invariant functionals on M kill T, derived from route21's head leaf.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute21Data.headDualInvariantZeroData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute21Data chief) : MinimalBlockRawHeadDualInvariantZeroData P.rawTowerData

The quotient head has no invariant dual, derived from route21's irreducibility and nontrivial-action leaves.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute21Data.dualInvariantData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute21Data chief) : MinimalBlockDualInvariantVanishesData P.rawTowerData

Dual-invariant vanishing on the selected raw tower.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute21Data.rawInvariantCharacterData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute21Data chief) : MinimalBlockRawInvariantCharacterData P.rawTowerData

Raw invariant Frattini character on the selected raw tower.

Equations

• ⋯ = ⋯

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

Route21 group-tower data from the fine same-tower packet.

Equations

• P.groupTowerData = P.lowerGroupModuleData.groupTowerData ⋯ ⋯

Route21 assembly theorems

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

Route21 same-tower packet assembled from ten finer manuscript-shaped leaves.

This theorem does not call minimalBlock_lowerGroupModuleData or minimalBlock_headInvariantSemanticRoute12Data.

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

Route21 replacement for the route20 lower aggregate.

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

Route21 replacement for the route20 head/invariant aggregate, tied to the route21-selected raw tower.

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

Route21 group-tower provider, suitable for later integration in place of minimalBlock_groupTowerData_from_kernelConcreteRoute20.