Route20 minimal-block kernel concrete packet sidecar

This route-neutral sidecar leaves integrated routes and existing route files untouched. Route19 exposes four Section 7 kernel/head packets:

• minimalBlock_kernelLeastOverChiefData;
• minimalBlock_kernelFrattiniCollapseFullData;
• minimalBlock_kernelRawQuotientTowerData;
• minimalBlock_headInvariantSemanticRoute12Data.

Route20 weakens that surface to two same-tower packets:

• minimalBlock_lowerGroupModuleData, containing the coherent lower K, R = Phi(K), raw M,T,C, action, bridge, and nonzero-head data;
• minimalBlock_headInvariantSemanticRoute12Data on the raw tower supplied by that same lower packet.

The exported minimalBlock_groupTowerData_from_kernelConcreteRoute20 theorem has the same supervisor-facing shape as the route19 hook.

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

Route20 coherent packet for the Section 7 minimal-block kernel tower.

The lower tower and the head/invariant data are tied to the same raw tower, so downstream assembly cannot mix unrelated K, R, M, T, C, and simple-head choices.

• lower : MinimalBlockLowerGroupModuleData chief
• headInvariant : MinimalBlockHeadInvariantSemanticRoute12Data self.lower.rawTowerData

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

Invariant functionals on M kill T, from the same route20 head packet.

Equations

• ⋯ = ⋯

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

The quotient head has no invariant dual, from the same route20 head packet.

Equations

• ⋯ = ⋯

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

Dual-invariant vanishing for the same lower raw tower.

Equations

• ⋯ = ⋯

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

Raw invariant Frattini character for the same lower raw tower.

Equations

• ⋯ = ⋯

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

Route20 group-tower data from the coherent lower/head packet.

Equations

• P.groupTowerData = P.lower.groupTowerData ⋯ ⋯

Route20 assembly theorems

theorem Q2Presentation.Induction.minimalBlock_kernelConcreteRoute20Data_from_lowerHeadPackets {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelConcreteRoute20Data chief)

Coherent Route20 packet from the lower group/module packet and the head-invariant semantic packet on its raw tower.

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

Lower group/module data through Route20.

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

Route20 group-tower provider, suitable for supervisor integration in place of minimalBlock_groupTowerData_from_kernelConcreteRoute19.