Route151 Section 7 kernel closers

This sidecar leaves the integrated route files and root imports untouched. It strictly lowers the Route150 Section 7 kernel frontier by replacing the selected least/Frattini atoms, Route141 raw object/action atoms, and the compact invariant packet with one coherent same-tower selected packet.

The packet follows the manuscript Section 7 tower:

• a selected minimal K over the first non-scalar chief factor;
• the Frattini-collapse data for R = Phi(K);
• the selected raw R, M = K/R, T, C objects/actions and quotient bridge;
• the actual simple-head/lower-character invariant facts on that same raw tower.

The exported providers project this packet back to the Route150-consumed kernel interfaces and then replay the Route150 finite-count route with only the kernel source swapped.

Coherent selected kernel packet

structure Q2Presentation.Induction.Section7KernelRoute151Closers.KernelRoute151SelectedPackageData {p : FramedPair} (chief : NonScalarChiefFactor p) : Type 1

Route151 coherent selected Section 7 kernel packet.

Compared with the Route150 kernel frontier, this is one same-tower residual: the least subgroup, its Frattini collapse, the raw quotient/action bridge, and the invariant facts are selected together.

• least : MinimalBlockKernelLeastOverChiefData chief
• frattini : MinimalBlockKernelModuleConcreteFrattiniData self.least
• rawBridge : MinimalBlockKernelRoute78RawObjectClosers.RawObjectActionBridgeData self.least ⋯
• invariant : MinimalBlockInvariantActualProofs2Data self.rawBridge.rawData.rawTowerData

def Q2Presentation.Induction.Section7KernelRoute151Closers.KernelRoute151SelectedPackageData.rawQuotientTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute151SelectedPackageData chief) : MinimalBlockKernelRawQuotientTowerData D.least ⋯

The raw quotient/head packet recovered from the coherent Route151 data.

Equations

• D.rawQuotientTowerData = { objects := D.rawBridge.rawObjects, actions := D.rawBridge.rawActions, bridge := id (id D.rawBridge.rawBridge), head := ⋯ }

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

Forget the coherent Route151 packet to concrete kernel/module provenance.

Equations

• D.concreteProvenanceData = Q2Presentation.Induction.Section7KernelRoute147CombinedClosers.concreteProvenanceDataOfRawQuotientTower D.least ⋯ D.rawQuotientTowerData

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

The lower group/module tower selected by the coherent Route151 packet.

Equations

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

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

The group tower consumed by the Section 7 Fourier branch.

Equations

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

axiom Q2Presentation.Induction.Section7KernelRoute151Closers.kernelRoute151SelectedPackageData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (KernelRoute151SelectedPackageData chief)

Residual Route151 coherent selected Section 7 kernel packet.

Route150-compatible projections

theorem Q2Presentation.Induction.Section7KernelRoute151Closers.minimalBlock_kernelModuleConcreteProvenanceData_from_section7KernelRoute151Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Route151 concrete kernel/module provenance provider.

Its axiom closure replaces the Route150 kernel frontier with the single Route151 coherent selected packet.

theorem Q2Presentation.Induction.Section7KernelRoute151Closers.minimalBlock_lowerGroupModuleData_from_section7KernelRoute151Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockLowerGroupModuleData chief)

Route151 lower group/module provider.

theorem Q2Presentation.Induction.Section7KernelRoute151Closers.minimalBlock_groupTowerData_from_section7KernelRoute151Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupTowerData p chief)

Route151 group-tower provider for the Route150 Fourier branch.

Integrated Route150 replay with the Route151 kernel provider

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

Route151 kernel provenance in the current integrated naming style.

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

Route151 lower group/module provider in the current integrated naming style.

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

Route151 group-tower provider in the current integrated naming style.

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

Route150 nonterminal Fourier branch replayed with the Route151 kernel provider.

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated151KernelRoute (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)

Recursive branch for the Route151-kernel replay.

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_currentIntegrated151KernelRoute (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)

Recursion step for the Route151-kernel replay.

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

Boundary-framed count equality for the Route151-kernel replay.

theorem Q2Presentation.Induction.finite_surjection_counts_equal_currentIntegrated151KernelRoute (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 the Route150 compact route with only the Section 7 kernel provider replaced by Route151.