Route16 kernel/concrete sidecar for Section 7

This file is route-neutral: it does not edit IntegratedCurrentRouteProofs15, PresentationCorrect, or any existing sidecar.

Route15 removed the standalone minimalBlock_headNontrivialData leaf by deriving head nontriviality from the same-raw-tower route12 head/invariant semantic packet. Route16 pushes the same idea one layer lower: it packages the remaining kernel/concrete residuals into one manuscript-shaped same-tower construction.

The package keeps the Section 7 dependency chain explicit:

• least K;
• the full Frattini--centralizer collapse for R = Phi(K);
• raw R, M, T, C objects and induced actions;
• the literal K/R ~= M bridge;
• the head/invariant semantic packet on that very raw tower.

The exported group-tower theorem has the same shape as minimalBlock_groupTowerData_from_kernelHeadRoute15, but its axiom closure is a single route16 packet rather than the ten independent route15 kernel/head leaves.

Explicit uses of the route12 head/invariant semantic packet

def Q2Presentation.Induction.MinimalBlockHeadInvariantSemanticRoute12Data.headNontrivialData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (A : MinimalBlockHeadInvariantSemanticRoute12Data D) : MinimalBlockHeadNontrivialData D

The route12 semantic head packet implies that M/T is nontrivial.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockHeadInvariantSemanticRoute12Data.invariantFunctionalsKillTData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (A : MinimalBlockHeadInvariantSemanticRoute12Data D) : MinimalBlockRawInvariantFunctionalsKillTData D

Invariant functionals on M kill the lower scalar layer T.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockHeadInvariantSemanticRoute12Data.rawHeadDualInvariantZeroData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (A : MinimalBlockHeadInvariantSemanticRoute12Data D) : MinimalBlockRawHeadDualInvariantZeroData D

Quotient-head dual invariants vanish.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockHeadInvariantSemanticRoute12Data.dualInvariantVanishesData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (A : MinimalBlockHeadInvariantSemanticRoute12Data D) : MinimalBlockDualInvariantVanishesData D

The dual-invariant vanishing packet consumed by MinimalBlockGroupTowerData.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockHeadInvariantSemanticRoute12Data.rawInvariantCharacterData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (A : MinimalBlockHeadInvariantSemanticRoute12Data D) : MinimalBlockRawInvariantCharacterData D

The raw invariant Frattini character packet consumed by the group tower.

Equations

• ⋯ = ⋯

Route16 raw quotient core: objects/actions plus bridge, no head leaf

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

Raw quotient/action data and the K/R ~= M bridge for one fixed Section 7 kernel tower.

This deliberately omits head nontriviality: route16 derives that from the same-tower head/invariant semantic packet, as route15 did.

• objects : MinimalBlockKernelModuleConcreteRawObjectsData K F
• actions : MinimalBlockKernelModuleConcreteRawActionsData self.objects
• bridge : MinimalBlockKernelModuleConcreteBridgeData (MinimalBlockKernelModuleConcreteRawData.ofObjectsActions self.objects self.actions)

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

Forget the route16 raw core to the existing concrete raw-data packet.

Equations

• Q.rawData = Q2Presentation.Induction.MinimalBlockKernelModuleConcreteRawData.ofObjectsActions Q.objects Q.actions

def Q2Presentation.Induction.MinimalBlockKernelRawQuotientCoreRoute16Data.bridgeData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Q : MinimalBlockKernelRawQuotientCoreRoute16Data K F) : MinimalBlockKernelModuleConcreteBridgeData Q.rawData

The route16 bridge, restated over rawData.

Equations

• Q.bridgeData = id Q.bridge

One same-tower route16 package

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

The route16 manuscript-shaped kernel/concrete package for the Section 7 minimal-block tower.

It is stronger than the independent route15 leaves because all fields are tied to one selected K, one literal Phi(K), one raw quotient/action construction, and one head/invariant packet on the resulting raw tower.

• least : MinimalBlockKernelLeastOverChiefData chief
• collapse : MinimalBlockKernelFrattiniCollapseFullData self.least
• rawCore : MinimalBlockKernelRawQuotientCoreRoute16Data self.least ⋯
• headInvariant : MinimalBlockHeadInvariantSemanticRoute12Data self.rawCore.rawData.rawTowerData

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

The concrete Frattini packet projected from the full collapse package.

Equations

• ⋯ = ⋯

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

The concrete raw-data packet selected by the route16 package.

Equations

• P.rawData = P.rawCore.rawData

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

The same-tower concrete bridge selected by the route16 package.

Equations

• P.bridgeData = P.rawCore.bridgeData

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

Head nontriviality derived from the explicit route16 head/invariant packet.

Equations

• ⋯ = ⋯

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

Dual-invariant vanishing derived from the explicit route16 head/invariant packet.

Equations

• ⋯ = ⋯

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

Raw invariant Frattini character derived from the explicit route16 head/invariant packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute16Data.actualProofs {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute16Data chief) : MinimalBlockKernelModuleActualProofs chief

The aggregate actual kernel/module packet recovered from route16 data.

Equations

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

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

The route-ready group tower recovered from route16 data.

Equations

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

Route16 residual boundary and exported route-ready theorems

axiom Q2Presentation.Induction.minimalBlock_kernelConcreteRoute16Data {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelConcreteRoute16Data chief)

Route16 residual boundary: one same-tower manuscript construction replacing the independent route15 kernel/head residual leaves.

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

Aggregate actual kernel/module packet through the route16 package.

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

Lower group/module data through the route16 package.

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

Route16 replacement with the same shape as minimalBlock_groupTowerData_from_kernelHeadRoute15.