Route167 Section 7 kernel/provenance closers

This sidecar leaves Route166 untouched and replays its finite-count theorem with only the Section 7 kernel provider swapped.

The least-kernel and Frattini-collapse part is routed through the existing Route146/Route78 lower bridge. The remaining raw quotient tower and same-tower simple-head fields are exposed as Route167 manuscript-stage atoms, so the new routed theorem does not depend on the Route164 wrapper atoms.

def Q2Presentation.Induction.Section7KernelRoute167Closers.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.

axiom Q2Presentation.Induction.Section7KernelRoute167Closers.rawQuotientTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelRawQuotientTowerData K F)

Route167 raw quotient tower for the manuscript layer R = Phi(K), M = K/R, T, and C = Y/K, including the quotient bridge and nontrivial head on that same tower.

axiom Q2Presentation.Induction.Section7KernelRoute167Closers.rawSimpleHeadSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Q : MinimalBlockKernelRawQuotientTowerData K F) : Nonempty (MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData Q.rawData.rawTowerData)

Route167 same-tower raw simple-head semantic packet for the selected raw quotient tower.

structure Q2Presentation.Induction.Section7KernelRoute167Closers.KernelRoute167ModuleLayerData {p : FramedPair} (chief : NonScalarChiefFactor p) : Type 1

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

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

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

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

Equations

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

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

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

Equations

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

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

The group tower consumed by the Fourier branch.

Equations

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

theorem Q2Presentation.Induction.Section7KernelRoute167Closers.kernelRoute167ModuleLayerData_from_section7KernelRoute167Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (KernelRoute167ModuleLayerData chief)

Route167 module-layer packet through the lowered least/Frattini provider.

theorem Q2Presentation.Induction.Section7KernelRoute167Closers.minimalBlock_kernelModuleConcreteProvenanceData_from_section7KernelRoute167Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Concrete kernel/module provenance through Route167.

theorem Q2Presentation.Induction.Section7KernelRoute167Closers.minimalBlock_lowerGroupModuleData_from_section7KernelRoute167Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockLowerGroupModuleData chief)

Lower group/module data through Route167.

theorem Q2Presentation.Induction.Section7KernelRoute167Closers.minimalBlock_groupTowerData_from_section7KernelRoute167Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupTowerData p chief)

Drop-in Route167 replacement for Section7KernelRoute164Closers.minimalBlock_groupTowerData_from_section7KernelRoute164Closers.

Route166 replay with the Route167 kernel provider

theorem Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch_currentIntegrated167AllRoute164Kernel167 (p : FramedPair) : ¬ScalarTerminal p → Nonempty (FourierBranchData p)

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated167AllRoute164Kernel167 (p : FramedPair) (h : ¬ScalarTerminal p) : ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_currentIntegrated167AllRoute164Kernel167 (p : FramedPair) : framedCountA p = framedCountQ p ∨ ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

theorem Q2Presentation.Induction.boundaryFramed_counts_equal_currentIntegrated167AllRoute164Kernel167 (p : FramedPair) : framedCountA p = framedCountQ p

theorem Q2Presentation.Induction.finite_surjection_counts_equal_currentIntegrated167AllRoute164Kernel167 (G : Type) [Group G] [Finite G] [Nonempty G] : Cardinal.mk (Profinite.SurjContHom GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))) = Cardinal.mk (Profinite.SurjContHom GQ2Profinite (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G)))

Finite-surjection equality for Route166 with only the Section 7 kernel provider replaced by Route167.