Route54 minimal-block kernel/provenance sidecar

This file is route-neutral: it does not edit the current integrated route.

Route53 exposes thirteen independent Section 7 kernel/raw leaves. Route54 replaces that surface by one coherent same-tower packet assembled from the existing Route44 manuscript packets:

• least-kernel data via the Route26 upper-candidate leastness route;
• one full Frattini--centralizer collapse packet for the selected K;
• one raw quotient tower packet for R = Phi(K), M = K/R, T, C, actions, bridge, and head nontriviality;
• one same-raw-tower simple-head/scalar semantic packet.

The key compatibility point is the projection KernelRoute54Data.toRoute53ConsumedData: it rebuilds the exact consumed packet used by MinimalBlockKernelRoute53.groupTowerData_from_route53, but without calling the Route53 kernel/raw residuals.

Coherent Route54 packet

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

Route54's coherent Section 7 kernel/provenance packet.

The fields are attached to one selected minimal-block tower, matching the manuscript tower R = Phi(K), M = K/R, T = (K cap S)/R, and C = Y/K.

• least : MinimalBlockKernelLeastOverChiefData chief
• frattiniFull : MinimalBlockKernelFrattiniCollapseFullData self.least
• rawQuotient : MinimalBlockKernelRawQuotientTowerData self.least ⋯
• simpleHead : MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData self.rawQuotient.rawData.rawTowerData

def Q2Presentation.Induction.MinimalBlockKernelRoute54.KernelRoute54Data.frattiniData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute54Data chief) : MinimalBlockKernelModuleConcreteFrattiniData D.least

The concrete Frattini packet carried by Route54.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelRoute54.KernelRoute54Data.rawData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute54Data chief) : MinimalBlockKernelModuleConcreteRawData D.least ⋯

The coherent raw quotient data carried by Route54.

Equations

• D.rawData = D.rawQuotient.rawData

def Q2Presentation.Induction.MinimalBlockKernelRoute54.KernelRoute54Data.actualProofs {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute54Data chief) : MinimalBlockKernelModuleActualProofs chief

The actual kernel/module packet projected from Route54 data.

Equations

• D.actualProofs = Q2Presentation.Induction.MinimalBlockKernelConcreteRoute24.actualProofsOfRawQuotient D.least ⋯ D.rawQuotient

def Q2Presentation.Induction.MinimalBlockKernelRoute54.KernelRoute54Data.lower {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute54Data chief) : MinimalBlockLowerGroupModuleData chief

The lower tower selected by the Route54 packet.

Equations

• D.lower = D.actualProofs.lowerGroupModuleData

def Q2Presentation.Induction.MinimalBlockKernelRoute54.KernelRoute54Data.headInvariantSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute54Data chief) : MinimalBlockHeadInvariantSemanticRoute12Data D.rawData.rawTowerData

Route12-shaped simple-head/invariant data projected from Route54's same-raw-tower semantic packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelRoute54.KernelRoute54Data.invariantFunctionalsKillTData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute54Data chief) : MinimalBlockRawInvariantFunctionalsKillTData D.rawData.rawTowerData

Invariant functionals on M kill T, projected from the Route54 hyperplane-containment field.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelRoute54.KernelRoute54Data.rawHeadDualInvariantZeroData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute54Data chief) : MinimalBlockRawHeadDualInvariantZeroData D.rawData.rawTowerData

Vanishing of dual invariants on the quotient head, projected from Route54's irreducibility and nontrivial-action fields.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelRoute54.KernelRoute54Data.dualInvariantData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute54Data chief) : MinimalBlockDualInvariantVanishesData D.rawData.rawTowerData

Direct dual-invariant vanishing on the selected raw tower.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelRoute54.KernelRoute54Data.rawLowerScalarQuotientData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute54Data chief) : MinimalBlockRawLowerScalarQuotientData D.rawData.rawTowerData

The lower scalar quotient projected from the Route54 invariant-character existence field.

Equations

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

def Q2Presentation.Induction.MinimalBlockKernelRoute54.KernelRoute54Data.rawInvariantCharacterData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute54Data chief) : MinimalBlockRawInvariantCharacterData D.rawData.rawTowerData

A raw invariant character on the selected Frattini layer.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelRoute54.KernelRoute54Data.toRoute53ConsumedData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute54Data chief) : MinimalBlockKernelRoute53.ConsumedData chief

Projection from the Route54 packet to the exact consumed packet used by the Route53 provider.

Equations

• D.toRoute53ConsumedData = { kernel := D.actualProofs, dualInvariant := ⋯, rawInvariantCharacter := ⋯ }

def Q2Presentation.Induction.MinimalBlockKernelRoute54.KernelRoute54Data.groupTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute54Data chief) : MinimalBlockGroupTowerData p chief

The group tower projected through Route53's consumed-packet API.

Equations

• D.groupTowerData = D.toRoute53ConsumedData.groupTowerData

Route54 packet from existing coherent Route44 packets

theorem Q2Presentation.Induction.MinimalBlockKernelRoute54.kernelRoute54Data_from_route44Packets {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (KernelRoute54Data chief)

Assemble Route54 data from the existing coherent Route44 manuscript packets.

The closure has four nonstandard Section 7 leaves:

• minimalBlock_kernelLeastUniversalData;
• minimalBlock_kernelFrattiniCollapseFullData;
• minimalBlock_kernelRawQuotientTowerData;
• MinimalBlockKernelConcreteRoute44.rawSimpleHeadSemanticData.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute54.consumedData_from_route54 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelRoute53.ConsumedData chief)

Route53 consumed data supplied by the Route54 packet.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute54.groupInvariantRouteData_from_route54 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantRouteData chief)

Route53 group/invariant route data supplied by Route54.

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

Route53-compatible group tower supplied by Route54.

Public Route54 kernel provider

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

Drop-in kernel provider replacing minimalBlock_groupTowerData_from_kernelRoute53.

Its target is identical to Route53's public provider, while its Section 7 closure avoids the thirteen independent Route53 kernel/raw leaves and retains only the four coherent Route44 manuscript packets.