Route84 kernel closers for the minimal-block route

This sidecar advances the Route86 kernel frontier without editing the integrated Route86 file. Route83 already projects the simple-head fields from the coherent actual invariant packet minimalBlock_invariantActualProofs2Data; the remaining raw tower part still used seven separate Route43 literal/object/action leaves.

Route84 replaces those seven leaves by one same-tower literal packet containing the Section 7 objects

• R = Phi(K),
• M = K/Phi(K),
• T = (K cap S)/Phi(K),
• C = Y/K,

together with the transported actions and T-stability on those same objects. The downstream Route55 consumer still sees the same raw object/action/bridge shape, so the public provider is a drop-in replacement for minimalBlock_groupTowerData_from_kernelRoute83Closers.

Coherent raw object/action tower

structure Q2Presentation.Induction.MinimalBlockKernelRoute84Closers.RawLiteralObjectActionTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Type 1

Route84 coherent literal raw tower packet.

The seven Route43 residual packets for literal objects, transported actions, and T-stability are recorded here as one dependent same-tower datum. The dependency of the action fields on the selected literal R,M,T,C objects prevents mixing data from different raw towers.

• Rlit : MinimalBlockKernelConcreteRoute43.RawFrattiniLiteralModuleObjectData K F
• Mlit : MinimalBlockKernelConcreteRoute43.RawQuotientLiteralModuleObjectData K F
• Tlit : MinimalBlockKernelConcreteRoute43.RawSubmoduleLiteralObjectData self.Mlit.toObject
• Clit : MinimalBlockKernelConcreteRoute43.RawLowerLiteralQuotientGroupData K F
• actR : MinimalBlockKernelConcreteRoute43.RawFrattiniTransportActionData self.Rlit.toObject self.Clit.toObject
• actM : MinimalBlockKernelConcreteRoute43.RawModuleTransportActionData self.Mlit.toObject self.Clit.toObject
• stable : MinimalBlockKernelConcreteRoute43.RawSubmoduleTransportStableData self.Tlit.toObject self.actM

axiom Q2Presentation.Induction.MinimalBlockKernelRoute84Closers.rawLiteralObjectActionTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (RawLiteralObjectActionTowerData K F)

Residual coherent literal raw tower packet for Route84.

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

Route78-shaped raw object/action/bridge packet from the coherent Route84 literal tower.

This is theorem-level repacking: the selected literal M = K/Phi(K) equivalence supplies the bridge, while the transported actions and T-stability supply the current raw action API.

Route55-shaped provider

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

Route55-shaped packet using Route81 least/Frattini data, the coherent Route84 raw tower packet, and Route83 actual simple-head projections.

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

Route54 coherent data supplied through Route84.

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

Route53 consumed data supplied through Route84.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute84Closers.groupInvariantRouteData_from_route84 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantRouteData chief)

Route53 group/invariant route data supplied through Route84.

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

Group-tower provider using Route84 coherent raw tower lowering.

Public provider

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

Drop-in kernel provider using Route84 coherent raw tower lowering.