Route19 minimal-block kernel concrete packet sidecar

This route-neutral sidecar leaves integrated routes and shared closers untouched. Route18 exposed sixteen narrow Section 7 kernel/head atoms. Route19 repackages that surface into four same-tower manuscript packets:

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

The aggregate packet below keeps the selected least K, the literal Frattini-collapse package for R = Phi(K), the raw quotient/action tower, and the simple-head/invariant package on the same raw tower. The exported minimalBlock_groupTowerData_from_kernelConcreteRoute19 theorem has the supervisor-facing shape needed for future integration.

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

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

• least : MinimalBlockKernelLeastOverChiefData chief
• collapse : MinimalBlockKernelFrattiniCollapseFullData self.least
• rawQuotient : MinimalBlockKernelRawQuotientTowerData self.least ⋯
• headInvariant : MinimalBlockHeadInvariantSemanticRoute12Data self.rawQuotient.rawData.rawTowerData

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

The concrete Frattini packet carried by the Route19 aggregate.

Equations

• ⋯ = ⋯

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

The concrete raw-data packet carried by the Route19 aggregate.

Equations

• P.rawData = P.rawQuotient.rawData

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute19Data.bridgeData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute19Data chief) : MinimalBlockKernelModuleConcreteBridgeData P.rawData

The concrete bridge packet carried by the Route19 aggregate.

Equations

• P.bridgeData = id P.rawQuotient.bridgeData

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute19Data.headData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute19Data chief) : MinimalBlockKernelModuleConcreteHeadData P.rawData

The concrete nonzero-head packet carried by the Route19 aggregate.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute19Data.kernelModuleActualProofs {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute19Data chief) : MinimalBlockKernelModuleActualProofs chief

Assemble the aggregate kernel/module actual proof packet.

Equations

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

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

The lower group/module tower determined by the same Route19 aggregate.

Equations

• P.lowerGroupModuleData = P.kernelModuleActualProofs.lowerGroupModuleData

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

Dual-invariant vanishing for the same raw tower.

Equations

• ⋯ = ⋯

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

Raw invariant Frattini character for the same raw tower.

Equations

• ⋯ = ⋯

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

Route19 group-tower data from the coherent aggregate packet.

Equations

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

Route19 assembly theorems

theorem Q2Presentation.Induction.minimalBlock_kernelConcreteRoute19Data_from_coherentPackets {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelConcreteRoute19Data chief)

Coherent Route19 packet from the four manuscript-shaped residual packets.

theorem Q2Presentation.Induction.minimalBlock_kernelModuleActualProofs_from_kernelConcreteRoute19 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleActualProofs chief)

Aggregate actual kernel/module packet through Route19.

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

Lower group/module data through Route19.

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

Route19 group-tower provider, suitable for supervisor integration.