Route180 Section 7 kernel raw-tower closers

This sidecar keeps Route175's Frattini carrier lowering and lowers the Route143 raw-actual frontier by opening its three aggregate same-tower atoms into the literal Route43 manuscript packets:

• R = Phi(K), M = K/Phi(K), T = (K cap S)/Phi(K), and C = Y/K;
• the transported actions on R and M, plus T-stability;
• the four simple-head fields from lem:simplehead.

The integrated Route180 audit should therefore remove the three Section7KernelRoute143RawActualClosers.* atoms from the Route179 closure and replace them by the lower Route43 object/action/head leaves.

Route143 raw-object aggregates from Route43 literal pieces

theorem Q2Presentation.Induction.Section7KernelRoute180Closers.rawLiteralObjectTowerData_from_route180Pieces {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (Section7KernelRoute143RawActualClosers.RawLiteralObjectTowerData K F)

Route180 opens the Route143 literal object tower into the four Route43 manuscript object packets.

theorem Q2Presentation.Induction.Section7KernelRoute180Closers.rawLiteralTransportActionData_from_route180Pieces {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (O : Section7KernelRoute143RawActualClosers.RawLiteralObjectTowerData K F) : Nonempty (Section7KernelRoute143RawActualClosers.RawLiteralTransportActionData O)

Route180 opens the Route143 transport-action tower into the three Route43 transport packets.

theorem Q2Presentation.Induction.Section7KernelRoute180Closers.rawSimpleHeadActualData_from_route180Pieces {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (Section7KernelRoute143RawActualClosers.RawSimpleHeadActualData D)

Route180 opens the Route143 simple-head aggregate into the four Route43 lem:simplehead leaves.

Raw quotient tower through the opened Route180 packets

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

Route78-shaped raw object/action/bridge data with the Route143 object and transport aggregates opened into Route43 leaves.

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

Raw quotient tower with the Route143 raw aggregates opened into Route43 leaves.

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

Route175 Frattini replay with Route180 raw tower

theorem Q2Presentation.Induction.Section7KernelRoute180Closers.kernelRoute180RawActualLayerData_from_section7KernelRoute180Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (Section7KernelRoute175FrattiniClosers.KernelRoute175RawActualLayerData chief)

Route180 raw-actual module-layer packet. The Frattini half is Route175; the raw object/action/head half is opened below the Route143 aggregates.

theorem Q2Presentation.Induction.Section7KernelRoute180Closers.minimalBlock_kernelModuleConcreteProvenanceData_from_section7KernelRoute180Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

theorem Q2Presentation.Induction.Section7KernelRoute180Closers.minimalBlock_lowerGroupModuleData_from_section7KernelRoute180Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockLowerGroupModuleData chief)

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

Drop-in Route180 kernel provider for the integrated diagnostic route.