Route78 raw object/action closers for the minimal-block kernel

This sidecar is route-neutral. It keeps the current Route76 least/Frattini assembly, but replaces the Route77 raw object/action/head frontier by two same-tower manuscript packets.

• rawObjectActionBridgeData records exactly the raw R,M,T,C objects, the transported actions, T-stability, and the K/Phi(K) ~= M bridge consumed by Route55. It deliberately does not expose the stronger Route43 literal-object equivalences, because the current kernel assembly does not consume them.
• rawSimpleHeadSemanticData is the Route44 lem:simplehead interface on the same raw tower: invariant hyperplanes contain T, nonzero stable submodules of M/T are all of M/T, the head action is not pointwise trivial, and the lower Frattini layer has a nonzero invariant character.

The exported provider has the same target as minimalBlock_groupTowerData_from_kernelRoute76RawClosers, so it can be used as a drop-in kernel provider in a later integrated route.

Same-tower raw object/action/bridge packet

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

Route78 same-tower raw object/action/bridge packet.

This is the exact raw quotient surface consumed by Route55: raw objects, raw actions, and the concrete bridge tying the selected quotient K/Phi(K) to the raw module M. It is narrower than the Route43 literal-object surface for this route, because it does not ask for unused literal equivalences for R and C.

• rawObjects : MinimalBlockKernelModuleConcreteRawObjectsData K F
• rawActions : MinimalBlockKernelModuleConcreteRawActionsData self.rawObjects
• rawBridge : MinimalBlockKernelModuleConcreteBridgeData (MinimalBlockKernelModuleConcreteRawData.ofObjectsActions self.rawObjects self.rawActions)

def Q2Presentation.Induction.MinimalBlockKernelRoute78RawObjectClosers.RawObjectActionBridgeData.rawData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (D : RawObjectActionBridgeData K F) : MinimalBlockKernelModuleConcreteRawData K F

The raw data selected by the Route78 packet.

Equations

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

axiom Q2Presentation.Induction.MinimalBlockKernelRoute78RawObjectClosers.rawObjectActionBridgeData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (RawObjectActionBridgeData K F)

Residual Route78 raw object/action/bridge extraction for the selected Section 7 tower.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute78RawObjectClosers.rawSimpleHeadSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData D)

Route78 same-raw-tower simple-head packet, in the Route44 semantic form.

Projections for the lowered head leaves

theorem Q2Presentation.Induction.MinimalBlockKernelRoute78RawObjectClosers.rawInvariantHyperplanesContainTData_from_route78 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawInvariantHyperplanesContainTData D)

Route78 direct hyperplane form replacing the Route43 maximal-submodule detour.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute78RawObjectClosers.rawHeadOrbitSpansData_from_route78 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadOrbitSpansData D)

Route78 orbit-span packet from the same-tower nonzero-stable criterion.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute78RawObjectClosers.rawHeadActionNotPointwiseTrivialData_from_route78 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadActionNotPointwiseTrivialData D)

Route78 closes the Route76 not-pointwise-trivial head-action leaf by projection from the same-tower semantic packet.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute78RawObjectClosers.rawLowerInvariantCharacterExistsData_from_route78 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawLowerInvariantCharacterExistsData D)

Route78 closes the Route76 lower-character existential leaf by projection from the same-tower semantic packet.

Raw quotient and Route55 assembly

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

The raw quotient tower selected by Route78.

The head nontriviality field is obtained theorem-level from the semantic not-pointwise-trivial head action, so it does not require a separate raw-head leaf.

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

Route55-shaped kernel packet using Route72 least/Frattini data and Route78 raw object/action/head lowerings.

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

Route54 coherent data supplied through Route78.

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

Route53 consumed data supplied through Route78.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute78RawObjectClosers.groupInvariantRouteData_from_route78 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantRouteData chief)

Route53 group/invariant route data supplied through Route78.

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

Group-tower provider using Route72 least/Frattini data and Route78 raw object/action/head lowerings.

Public provider

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

Drop-in replacement for minimalBlock_groupTowerData_from_kernelRoute76RawClosers, with the Route43 literal object/action leaves and the Route76 raw-head leaves replaced by Route78 same-tower packets.