Route82 kernel closers for the minimal-block route

This sidecar advances the Route82 kernel frontier without editing the integrated Route82 proof. It keeps the Route81 least/Frattini lowering for the selected K, but routes the raw tower and simple-head layer through smaller Section 7 manuscript packets:

• the raw R, M, T, C objects are selected as the literal Route43 objects R = Phi(K), M = K/Phi(K), T = (K cap S)/Phi(K), and C = Y/K;
• the raw actions are selected as the Route43 transported actions on R and M, plus T-stability;
• the bridge K/Phi(K) ~= M is theorem-level from the selected literal quotient object, so no separate Route81 bridge atom is used;
• the four Route81 simple-head fields are supplied by Route43 proof-step packets: maximal-submodule containment, orbit spanning, a nontrivial-action witness, and a chosen invariant lower character.

The public provider is a drop-in replacement for minimalBlock_groupTowerData_from_kernelRoute81Closers, but it is intentionally not imported by the integrated route.

Raw object/action/bridge lowering

theorem Q2Presentation.Induction.MinimalBlockKernelRoute82Closers.rawObjectActionBridgeData_from_route82 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelRoute78RawObjectClosers.RawObjectActionBridgeData K F)

Route82 raw object/action/bridge packet from Route43 literal and transported same-tower data.

This replaces the three Route81 raw atoms rawObjectsData, rawActionsData, and rawBridgeData by the literal Section 7 objects/actions. The bridge is recovered from the literal M = K/Phi(K) packet selected in the same construction.

Simple-head semantic lowering

theorem Q2Presentation.Induction.MinimalBlockKernelRoute82Closers.rawSimpleHeadSemanticData_from_route82 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData D)

Route82 simple-head semantic packet assembled from Route43 proof-step packets.

This replaces the four Route81 simple-head atoms by the lower manuscript forms already present in Route43.

Route55-shaped provider

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

Route55-shaped packet using Route81 least/Frattini lowerings and Route82 raw/simple-head lowerings on one selected tower.

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

Route54 coherent data supplied through the Route82 kernel path.

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

Route53 consumed data supplied through Route82.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute82Closers.groupInvariantRouteData_from_route82 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantRouteData chief)

Route53 group/invariant route data supplied through Route82.

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

Group-tower provider using Route82 raw/simple-head lowerings.

Public provider

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

Drop-in kernel provider using Route82 raw/simple-head lowerings.