Route199 Section 7 raw-module/head lowering

This sidecar keeps the Route198/197 Section 7 kernel shape fixed except for the raw module/head provider. The Route72 least-kernel and Frattini-collapse packets are retained, while the Route180/Route43 raw tower is replaced by the older Route146 raw/head decomposition:

• Route141 raw object/equivalence/action-family packets assemble the literal R, M, T, and C tower and transported actions;
• the simple-head fields are obtained from the no-trivial-dual, head simplicity/nontriviality, and lower scalar quotient packets.

The integrated Route199 audit should therefore remove the eleven MinimalBlockKernelConcreteRoute43.* raw object/action/head atoms exposed by Route198.

Route198 raw leaves through Route146 raw/head lowerers

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

Route199 raw object/action bridge through the Route146 raw decomposition.

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

Route199 replacement for the Route180/43 raw quotient tower.

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

Route199 same-tower simple-head semantic packet through Route146's head/lower-scalar split.

Drop-in Route198/197 kernel provider with the raw tower swapped

structure Q2Presentation.Induction.Section7KernelRoute199RawClosers.KernelRoute199RawLayerData {p : FramedPair} (chief : NonScalarChiefFactor p) : Type 1

Route199 module-layer packet: Route72 Frattini data plus the Route146 raw/head lowering.

• least : MinimalBlockKernelLeastOverChiefData chief
• frattini : MinimalBlockKernelModuleConcreteFrattiniData self.least
• rawTower : MinimalBlockKernelRawQuotientTowerData self.least ⋯
• rawSimple : MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData self.rawTower.rawData.rawTowerData

def Q2Presentation.Induction.Section7KernelRoute199RawClosers.KernelRoute199RawLayerData.concreteProvenanceData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute199RawLayerData chief) : MinimalBlockKernelModuleConcreteProvenanceData chief

Forget the Route199 module-layer packet to concrete kernel provenance.

Equations

• D.concreteProvenanceData = Q2Presentation.Induction.Section7KernelRoute167Closers.concreteProvenanceDataOfRawQuotientTower D.least ⋯ D.rawTower

def Q2Presentation.Induction.Section7KernelRoute199RawClosers.KernelRoute199RawLayerData.lowerGroupModuleData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute199RawLayerData chief) : MinimalBlockLowerGroupModuleData chief

Lower group/module data selected by the Route199 packet.

Equations

• D.lowerGroupModuleData = Q2Presentation.Induction.minimalBlock_lowerFromConcreteProvenance D.concreteProvenanceData

def Q2Presentation.Induction.Section7KernelRoute199RawClosers.KernelRoute199RawLayerData.invariantActualData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute199RawLayerData chief) : MinimalBlockInvariantActualProofs2Data D.lowerGroupModuleData.rawTowerData

Same-tower invariant packet from the Route199 simple-head semantics.

Equations

• D.invariantActualData = id (Q2Presentation.Induction.MinimalBlockInvariantRoute112Closers.invariantActualProofs2Data_of_rawSimpleHeadSemanticData ⋯)

def Q2Presentation.Induction.Section7KernelRoute199RawClosers.KernelRoute199RawLayerData.groupTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute199RawLayerData chief) : MinimalBlockGroupTowerData p chief

The group tower consumed by the Section 7 Fourier branch.

Equations

• D.groupTowerData = D.lowerGroupModuleData.groupTowerData ⋯ ⋯

theorem Q2Presentation.Induction.Section7KernelRoute199RawClosers.kernelRoute199RawLayerData_from_section7KernelRoute199RawClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (KernelRoute199RawLayerData chief)

Route199 module-layer packet through Route72 and Route146 raw/head data.

theorem Q2Presentation.Induction.Section7KernelRoute199RawClosers.minimalBlock_kernelModuleConcreteProvenanceData_from_section7KernelRoute199RawClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Concrete kernel/module provenance through Route199.

theorem Q2Presentation.Induction.Section7KernelRoute199RawClosers.minimalBlock_lowerGroupModuleData_from_section7KernelRoute199RawClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockLowerGroupModuleData chief)

Lower group/module data through Route199.

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

Drop-in Route199 Section 7 kernel provider for the integrated raw audit.