Route161 Section 7 kernel/provenance closers

This sidecar leaves the integrated route files untouched. It gives a Route157-shaped kernel provider, but routes the kernel/provenance construction through the Route145 concrete actual chain:

• least-over-chief data from the concrete least-over-chief closer;
• Frattini collapse from the split concrete Frattini fields;
• raw R, M, T, C tower and transported actions from Route43 atoms;
• raw simple-head/invariant data from Route43 atoms and Route112 assembly.

The replayed finite-count theorem below keeps the Route160 candidate, target, and pushout lowerings, replacing only the kernel provider used in the nonterminal Fourier branch.

Route161 kernel provider bridge

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

Concrete kernel/module provenance through the Route161 bridge.

The closure is inherited from Route145's concrete actual provider and avoids the Route160 Route141-Frattini and Route143 raw-actual aggregate atoms.

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

Lower group/module data through the Route161 kernel bridge.

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

Drop-in replacement for Section7KernelRoute157Closers.minimalBlock_groupTowerData_from_section7KernelRoute157Closers.

It has the same target, but the dependency frontier is lowered to the Route145 concrete chief-series/Frattini/raw-module atoms.

Route160 replay with the Route161 kernel provider

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

Route160 nonterminal Fourier branch with only the kernel provider swapped to Route161.

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated161KernelRoute145 (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_currentIntegrated161KernelRoute145 (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_currentIntegrated161KernelRoute145 (p : FramedPair) : framedCountA p = framedCountQ p

theorem Q2Presentation.Induction.finite_surjection_counts_equal_currentIntegrated161KernelRoute145 (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 Route160 with the Route161 kernel lowering.