Route61 combined kernel closers

The two Route60 kernel sidecars lower complementary parts of the Section 7 minimal-block tower:

• MinimalBlockKernelRoute60FrattiniClosers supplies the least kernel and Frattini-collapse data from lower proof-step packets.
• MinimalBlockKernelRoute60RawHeadClosers supplies the raw module, K/R bridge, head, and lower-scalar data from Route42-style raw/head packets.

This file combines them into the same drop-in provider shape as minimalBlock_groupTowerData_from_kernelRoute55, without adding any axioms.

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

Route55-shaped data assembled from the Route60 Frattini side and the Route60 raw/head side.

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

Route54 coherent data supplied through the combined Route61 kernel packet.

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

Route53 consumed data supplied through the combined Route61 kernel packet.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute61CombinedClosers.groupInvariantRouteData_from_route61Combined {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantRouteData chief)

Route53 group/invariant route data supplied through the combined Route61 kernel packet.

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

Group-tower provider using both Route60 kernel sidecars.

Public provider

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

Drop-in replacement for minimalBlock_groupTowerData_from_kernelRoute55, using the combined Route60 least/Frattini and raw/head lowerings.