Route55 minimal-block kernel/provenance sidecar

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

Route54 packages the Section 7 kernel/raw work into four non-local leaves:

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

Route55 keeps Route54's consumed packet shape, but rebuilds it from the sharper same-tower APIs already present in the tree:

• the Route26 upper-candidate least-kernel route, so the least-universal field remains the only least-kernel frontier;
• the Route40 field-level Frattini-collapse split;
• the Route39 raw object/action/bridge/head transport split;
• the Route45 same-lower-tower simple-head split.

Thus the Route55 provider removes the Route54 Frattini, raw quotient, and Route44 simple-head aggregate axiom names from the kernel closure. The least-universal packet is deliberately not replaced by the broader minimalBlock_kernelLeastOverChiefData axiom: the current NonScalarChiefFactor structure records a non-scalar chief factor, but not the manuscript's full "all factors below S are scalar" first-layer datum needed to prove the strong universal leastness theorem-level.

Exact old-shape projections from sharper packets

def Q2Presentation.Induction.MinimalBlockKernelRoute55.frattiniCollapseFullDataOfConcrete {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : MinimalBlockKernelFrattiniCollapseFullData K

Repack concrete Frattini data as the old Route54 full-collapse shape.

This is theorem-level glue only; the constructor stores the five concrete Frattini conclusions already present in MinimalBlockKernelModuleConcreteFrattiniData.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.MinimalBlockKernelRoute55.frattiniCollapseFullData_from_route55Split {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelFrattiniCollapseFullData K)

Route55 replacement for the old full Frattini-collapse leaf, sourced from the Route40 field-level split.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute55.rawQuotientTowerData_from_route55Transport {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelRawQuotientTowerData K F)

Route55 replacement for the old raw quotient tower leaf, sourced from the Route39 object/action/bridge/head transport split.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute55.rawSimpleHeadSemanticData_from_route55Lower {p : FramedPair} {chief : NonScalarChiefFactor p} (lower : MinimalBlockLowerGroupModuleData chief) : Nonempty (MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData lower.rawTowerData)

Route55 replacement for the old arbitrary Route44 simple-head semantic leaf, restricted to the same lower tower actually consumed by Route54.

Route55 coherent packet

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

Route55's smaller same-tower Section 7 packet.

Unlike MinimalBlockKernelRoute54.KernelRoute54Data, this stores the concrete Frattini packet and the split raw quotient fields, not the two old Route54 aggregate leaves. The simpleHead field is attached to the same raw tower selected by the split raw quotient data.

• least : MinimalBlockKernelLeastOverChiefData chief
• frattiniData : MinimalBlockKernelModuleConcreteFrattiniData self.least
• rawObjects : MinimalBlockKernelModuleConcreteRawObjectsData self.least ⋯
• rawActions : MinimalBlockKernelModuleConcreteRawActionsData self.rawObjects
• rawBridge : MinimalBlockKernelModuleConcreteBridgeData (MinimalBlockKernelModuleConcreteRawData.ofObjectsActions self.rawObjects self.rawActions)
• rawHead : MinimalBlockKernelModuleConcreteHeadData (MinimalBlockKernelModuleConcreteRawData.ofObjectsActions self.rawObjects self.rawActions)
• simpleHead : MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData (MinimalBlockKernelModuleConcreteRawData.ofObjectsActions self.rawObjects self.rawActions).rawTowerData

def Q2Presentation.Induction.MinimalBlockKernelRoute55.KernelRoute55Data.frattiniFull {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute55Data chief) : MinimalBlockKernelFrattiniCollapseFullData D.least

The old full Frattini-collapse packet recovered from Route55 concrete data.

Equations

• ⋯ = ⋯

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

The concrete raw quotient data carried by Route55.

Equations

• D.rawData = Q2Presentation.Induction.MinimalBlockKernelModuleConcreteRawData.ofObjectsActions D.rawObjects D.rawActions

def Q2Presentation.Induction.MinimalBlockKernelRoute55.KernelRoute55Data.rawQuotient {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute55Data chief) : MinimalBlockKernelRawQuotientTowerData D.least ⋯

The old raw quotient tower packet recovered from Route55 split data.

Equations

• D.rawQuotient = { objects := D.rawObjects, actions := D.rawActions, bridge := D.rawBridge, head := ⋯ }

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

Aggregate actual kernel/module data projected from Route55.

Equations

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

def Q2Presentation.Induction.MinimalBlockKernelRoute55.KernelRoute55Data.toRoute54Data {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute55Data chief) : MinimalBlockKernelRoute54.KernelRoute54Data chief

Route54's coherent packet recovered from Route55's smaller packet.

Equations

• D.toRoute54Data = { least := D.least, frattiniFull := ⋯, rawQuotient := id D.rawQuotient, simpleHead := ⋯ }

Route55 packet assembly

theorem Q2Presentation.Induction.MinimalBlockKernelRoute55.kernelRoute55Data_from_splitPackets {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (KernelRoute55Data chief)

Assemble Route55 data from the sharper Section 7 APIs.

The axiom closure of this theorem keeps the Route26 least-universal residual, but avoids the old Route54 aggregate leaves for Frattini collapse, raw quotient, and Route44 simple-head semantics.

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

Route54 coherent data supplied by Route55's smaller packet.

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

Route53 consumed data supplied through Route55.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute55.groupInvariantRouteData_from_route55 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantRouteData chief)

Route53 group/invariant route data supplied through Route55.

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

Route53-compatible group tower supplied through Route55.

Public Route55 kernel provider

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

Drop-in kernel provider replacing minimalBlock_groupTowerData_from_kernelRoute54.

Its target is identical to Route54's public provider, while its Section 7 closure refines the Frattini/raw/simple-head Route54 aggregate leaves through Route40/39/45 split APIs. The Route26 least-universal residual remains.