Route66 combined kernel provider

Route65 used the Route63 least/Frattini lowering, but its kernel provider still obtained the raw/head transport through the Route60 raw/head closer, whose closure exposed the twelve Route42 atoms.

This sidecar keeps the same final MinimalBlockGroupTowerData surface, but combines:

• Route63 least/Frattini lowerings from MinimalBlockKernelFrattiniRoute63Closers; and
• Route63 raw/head lowerings from MinimalBlockKernelConcreteRoute63RawHeadClosers.

The public provider is minimalBlock_groupTowerData_from_kernelRoute66CombinedClosers.

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

Route55-shaped kernel packet using both Route63 Frattini and Route63 raw/head closers.

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

Route54 coherent data supplied through the Route66 kernel packet.

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

Route53 consumed data supplied through Route66.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute66CombinedClosers.groupInvariantRouteData_from_route66 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantRouteData chief)

Route53 group/invariant route data supplied through Route66.

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

Group-tower provider using Route63 least/Frattini and raw/head lowerings.

Public provider

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

Drop-in replacement for the active minimal-block group-tower provider with both the Frattini and raw/head Route63 lowerings integrated.