Route199 Section 7 Frattini closers for the Route198 kernel frontier

This sidecar is a drop-in replacement for the Route198/Route197 Section 7 kernel provider. It keeps the Route180/Route43 raw quotient and simple-head surface unchanged, but replaces the ten Route72 Frattini/least-kernel atoms by the finer Route199 field atoms.

Route198 Frattini leaves through Route199

theorem Q2Presentation.Induction.Section7KernelRoute199FrattiniClosers.leastKernelCandidateData_from_route199Frattini {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelCandidateData chief)

Route199 lowering of the Route198 least-kernel candidate atom.

theorem Q2Presentation.Induction.Section7KernelRoute199FrattiniClosers.leastKernelUniversalData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelCandidateData chief) : Nonempty (MinimalBlockKernelLeastUniversalData K)

Route199 lowering of the Route198 least-kernel universal atom.

theorem Q2Presentation.Induction.Section7KernelRoute199FrattiniClosers.leastKernelSelectionData_from_route199Frattini {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelRoute67FrattiniClosers.LeastKernelSelectionData chief)

Route67 least-kernel packet through Route199.

theorem Q2Presentation.Induction.Section7KernelRoute199FrattiniClosers.leastOverChiefData_from_route199Frattini {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelLeastOverChiefData chief)

Route-ready least-over-chief packet through Route199.

theorem Q2Presentation.Induction.Section7KernelRoute199FrattiniClosers.frattiniInternalElementData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FrattiniInternalElementData K)

Route199 lowering of the Route198 internal Frattini element atom.

theorem Q2Presentation.Induction.Section7KernelRoute199FrattiniClosers.frattiniInternalElementNontrivialData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (E : MinimalBlockKernelRoute72FrattiniClosers.FrattiniInternalElementData K) : Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FrattiniInternalElementNontrivialData E)

Route199 lowering of the Route198 internal Frattini nontriviality atom.

theorem Q2Presentation.Induction.Section7KernelRoute199FrattiniClosers.frattiniInternalNonidentityData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute67FrattiniClosers.FrattiniInternalNonidentityData K)

Route67 internal nonidentity packet through Route199.

theorem Q2Presentation.Induction.Section7KernelRoute199FrattiniClosers.frattiniCentralizerCoreData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FrattiniCentralizerCoreData K)

Route199 lowering of the Route198 centralizer core atom.

theorem Q2Presentation.Induction.Section7KernelRoute199FrattiniClosers.frattiniCentralizerHallImageData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (C : MinimalBlockKernelRoute72FrattiniClosers.FrattiniCentralizerCoreData K) : Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FrattiniCentralizerHallImageData C)

Route199 lowering of the Route198 centralizer Hall-image atom.

theorem Q2Presentation.Induction.Section7KernelRoute199FrattiniClosers.frattiniCentralizerHallCommutatorData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute67FrattiniClosers.FrattiniCentralizerHallCommutatorData K)

Route67 Hall-commutator centralizer packet through Route199.

theorem Q2Presentation.Induction.Section7KernelRoute199FrattiniClosers.fourthPowerKernelCoreData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FourthPowerKernelCoreData K)

Route199 lowering of the Route198 fourth-power core atom.

theorem Q2Presentation.Induction.Section7KernelRoute199FrattiniClosers.fourthPowerKernelHallImageData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (P4 : MinimalBlockKernelRoute72FrattiniClosers.FourthPowerKernelCoreData K) : Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FourthPowerKernelHallImageData P4)

Route199 lowering of the Route198 fourth-power Hall-image atom.

theorem Q2Presentation.Induction.Section7KernelRoute199FrattiniClosers.fourthPowerKernelCommutatorData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute67FrattiniClosers.FourthPowerKernelCommutatorData K)

Route67 fourth-power commutator packet through Route199.

theorem Q2Presentation.Induction.Section7KernelRoute199FrattiniClosers.frattiniSquareCommutatorContainmentData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FrattiniSquareCommutatorContainmentData K)

Route199 lowering of the Route198 square/commutator containment atom.

theorem Q2Presentation.Induction.Section7KernelRoute199FrattiniClosers.frattiniSquareCommutatorExponentData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (L : MinimalBlockKernelRoute72FrattiniClosers.FrattiniSquareCommutatorContainmentData K) : Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FrattiniSquareCommutatorExponentData L)

Route199 lowering of the Route198 square/commutator exponent atom.

theorem Q2Presentation.Induction.Section7KernelRoute199FrattiniClosers.frattiniSquareCommutatorLayerData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute67FrattiniClosers.FrattiniSquareCommutatorLayerData K)

Route67 square/commutator layer packet through Route199.

theorem Q2Presentation.Induction.Section7KernelRoute199FrattiniClosers.frattiniData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniData K)

Concrete Frattini packet assembled through the Route199 lower frontier.

Route198 raw leaves retained through Route180/Route43

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

Route199 keeps the Route198 raw quotient-tower lowering unchanged.

theorem Q2Presentation.Induction.Section7KernelRoute199FrattiniClosers.rawSimpleHeadSemanticData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Q : MinimalBlockKernelRawQuotientTowerData K F) : Nonempty (MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData Q.rawData.rawTowerData)

Route199 keeps the Route198 raw simple-head lowering unchanged.

Drop-in kernel provider

structure Q2Presentation.Induction.Section7KernelRoute199FrattiniClosers.KernelRoute199FrattiniModuleLayerData {p : FramedPair} (chief : NonScalarChiefFactor p) : Type 1

Route199 module-layer packet with Route199 Frattini data and Route180/43 raw tower data.

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

def Q2Presentation.Induction.Section7KernelRoute199FrattiniClosers.KernelRoute199FrattiniModuleLayerData.concreteProvenanceData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute199FrattiniModuleLayerData 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.Section7KernelRoute199FrattiniClosers.KernelRoute199FrattiniModuleLayerData.lowerGroupModuleData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute199FrattiniModuleLayerData chief) : MinimalBlockLowerGroupModuleData chief

Lower group/module data selected by the Route199 packet.

Equations

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

def Q2Presentation.Induction.Section7KernelRoute199FrattiniClosers.KernelRoute199FrattiniModuleLayerData.invariantActualData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute199FrattiniModuleLayerData 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.Section7KernelRoute199FrattiniClosers.KernelRoute199FrattiniModuleLayerData.groupTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute199FrattiniModuleLayerData chief) : MinimalBlockGroupTowerData p chief

The group tower consumed by the Section 7 Fourier branch.

Equations

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

theorem Q2Presentation.Induction.Section7KernelRoute199FrattiniClosers.kernelRoute199FrattiniModuleLayerData_from_section7KernelRoute199FrattiniClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (KernelRoute199FrattiniModuleLayerData chief)

Route199 module-layer packet through the lowered Frattini and raw providers.

theorem Q2Presentation.Induction.Section7KernelRoute199FrattiniClosers.minimalBlock_kernelModuleConcreteProvenanceData_from_section7KernelRoute199FrattiniClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Concrete kernel/module provenance through Route199.

theorem Q2Presentation.Induction.Section7KernelRoute199FrattiniClosers.minimalBlock_lowerGroupModuleData_from_section7KernelRoute199FrattiniClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockLowerGroupModuleData chief)

Lower group/module data through Route199.

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

Drop-in Route199 Section 7 kernel provider.