Documentation

Q2Presentation.Induction.Section7KernelRoute197Closers

Route197 Section 7 kernel/raw closers #

This sidecar targets exactly the Route196 Section 7 kernel/raw frontier.

The five Route67 Lemma 7.2 Frattini packets are routed through the lower Route72 candidate/universal, internal-element, Hall-image, fourth-power, and square/commutator packets. The two compact Route167 raw quotient/simple-head packets are routed through the opened Route180/Route43 raw object, action, and simple-head packets.

Route196 Frattini leaves through Route72 #

theorem Q2Presentation.Induction.Section7KernelRoute197Closers.leastKernelSelectionData_from_route197Kernel {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockKernelRoute67FrattiniClosers.LeastKernelSelectionData chief)

Route197 lowering of the Route196 least-kernel selection leaf.

theorem Q2Presentation.Induction.Section7KernelRoute197Closers.leastOverChiefData_from_route197Kernel {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockKernelLeastOverChiefData chief)

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

theorem Q2Presentation.Induction.Section7KernelRoute197Closers.frattiniInternalNonidentityData_from_route197Kernel {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelRoute67FrattiniClosers.FrattiniInternalNonidentityData K)

Route197 lowering of the Route196 internal Frattini nonidentity leaf.

theorem Q2Presentation.Induction.Section7KernelRoute197Closers.frattiniCentralizerHallCommutatorData_from_route197Kernel {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelRoute67FrattiniClosers.FrattiniCentralizerHallCommutatorData K)

Route197 lowering of the Route196 Hall-commutator centralizer leaf.

theorem Q2Presentation.Induction.Section7KernelRoute197Closers.fourthPowerKernelCommutatorData_from_route197Kernel {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelRoute67FrattiniClosers.FourthPowerKernelCommutatorData K)

Route197 lowering of the Route196 fourth-power commutator-kernel leaf.

theorem Q2Presentation.Induction.Section7KernelRoute197Closers.frattiniSquareCommutatorLayerData_from_route197Kernel {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelRoute67FrattiniClosers.FrattiniSquareCommutatorLayerData K)

Route197 lowering of the Route196 square/commutator layer leaf.

theorem Q2Presentation.Induction.Section7KernelRoute197Closers.frattiniData_from_route197Kernel {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelModuleConcreteFrattiniData K)

Concrete Frattini packet assembled through the Route72 lower frontier.

Route196 raw leaves through Route180/Route43 #

theorem Q2Presentation.Induction.Section7KernelRoute197Closers.rawQuotientTowerData_from_route197Kernel {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) :

Nonempty (MinimalBlockKernelRawQuotientTowerData K F)

Route197 lowering of Section7KernelRoute167Closers.rawQuotientTowerData.

theorem Q2Presentation.Induction.Section7KernelRoute197Closers.rawSimpleHeadSemanticData_from_route197Kernel {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Q : MinimalBlockKernelRawQuotientTowerData K F) :

Nonempty (MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData Q.rawData.rawTowerData)

Route197 lowering of Section7KernelRoute167Closers.rawSimpleHeadSemanticData.

Drop-in kernel provider #

structure Q2Presentation.Induction.Section7KernelRoute197Closers.KernelRoute197ModuleLayerData {p : FramedPair} (chief : NonScalarChiefFactor p) :

Route197 module-layer packet with Route72 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

Instances For

def Q2Presentation.Induction.Section7KernelRoute197Closers.KernelRoute197ModuleLayerData.concreteProvenanceData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute197ModuleLayerData chief) :

MinimalBlockKernelModuleConcreteProvenanceData chief

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

Equations

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

Instances For

def Q2Presentation.Induction.Section7KernelRoute197Closers.KernelRoute197ModuleLayerData.lowerGroupModuleData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute197ModuleLayerData chief) :

MinimalBlockLowerGroupModuleData chief

Lower group/module data selected by the Route197 packet.

Equations

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

Instances For

def Q2Presentation.Induction.Section7KernelRoute197Closers.KernelRoute197ModuleLayerData.invariantActualData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute197ModuleLayerData chief) :

MinimalBlockInvariantActualProofs2Data D.lowerGroupModuleData.rawTowerData

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

Equations

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

Instances For

def Q2Presentation.Induction.Section7KernelRoute197Closers.KernelRoute197ModuleLayerData.groupTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute197ModuleLayerData chief) :

MinimalBlockGroupTowerData p chief

The group tower consumed by the Section 7 Fourier branch.

Equations

D.groupTowerData = D.lowerGroupModuleData.groupTowerData ⋯ ⋯

Instances For

theorem Q2Presentation.Induction.Section7KernelRoute197Closers.kernelRoute197ModuleLayerData_from_section7KernelRoute197Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (KernelRoute197ModuleLayerData chief)

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

theorem Q2Presentation.Induction.Section7KernelRoute197Closers.minimalBlock_kernelModuleConcreteProvenanceData_from_section7KernelRoute197Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Concrete kernel/module provenance through Route197.

theorem Q2Presentation.Induction.Section7KernelRoute197Closers.minimalBlock_lowerGroupModuleData_from_section7KernelRoute197Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockLowerGroupModuleData chief)

Lower group/module data through Route197.

theorem Q2Presentation.Induction.Section7KernelRoute197Closers.minimalBlock_groupTowerData_from_section7KernelRoute197Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockGroupTowerData p chief)

Drop-in Route197 Section 7 kernel provider.