Route169 Section 7 kernel/provenance closers

This sidecar leaves all integrated route files untouched. It supplies a Route167-shape kernel provider, but replaces the two Route167 raw/head atoms

• Section7KernelRoute167Closers.rawQuotientTowerData;
• Section7KernelRoute167Closers.rawSimpleHeadSemanticData;

by the finer Route146 raw quotient/head closers. It also replaces the five Route78 least/Frattini selected-kernel atoms by the finer Route141 manuscript-level packets for the selected least K, Frattini witness, centralizer collapse, fourth-power kernel, and square/commutator exponent layer.

def Q2Presentation.Induction.Section7KernelRoute169Closers.concreteProvenanceDataOfRawQuotientTower {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) (Q : MinimalBlockKernelRawQuotientTowerData K F) : MinimalBlockKernelModuleConcreteProvenanceData chief

Assemble concrete provenance from a selected least kernel, its Frattini collapse, and a raw quotient/head tower.

Equations

• One or more equations did not get rendered due to their size.

structure Q2Presentation.Induction.Section7KernelRoute169Closers.KernelRoute169ModuleLayerData {p : FramedPair} (chief : NonScalarChiefFactor p) : Type 1

Route169 selected module layer assembled from Route141 least/Frattini data and Route146 raw/simple-head lowering data.

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

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

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

Equations

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

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

The lower group/module tower selected by the Route169 packet.

Equations

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

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

The actual invariant packet obtained from the same raw simple-head fields.

Equations

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

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

The group tower consumed by the Fourier branch.

Equations

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

theorem Q2Presentation.Induction.Section7KernelRoute169Closers.kernelRoute169ModuleLayerData_from_section7KernelRoute169Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (KernelRoute169ModuleLayerData chief)

Route169 module-layer packet through Route141 least/Frattini and Route146 raw/head lowerings.

theorem Q2Presentation.Induction.Section7KernelRoute169Closers.minimalBlock_kernelModuleConcreteProvenanceData_from_section7KernelRoute169Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Concrete kernel/module provenance through Route169.

theorem Q2Presentation.Induction.Section7KernelRoute169Closers.minimalBlock_lowerGroupModuleData_from_section7KernelRoute169Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockLowerGroupModuleData chief)

Lower group/module data through Route169.

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

Drop-in Route169 replacement for Section7KernelRoute167Closers.minimalBlock_groupTowerData_from_section7KernelRoute167Closers.