Integrated current route, fourth refinement

This route combines the two latest independent refinements:

• MinimalBlockKernelModuleSemanticClosers3 refines the §7 kernel/invariant route to the concrete kernel-module and raw-head/lower-scalar packets.
• MinimalBlockExtraspecialRoute4Closers refines the §7 central-pushout determinant route to a single actual scalar central-extension pushout family.

The capstone theorem below is the strongest current route: candidate and target §8 already flow through IntegratedCurrentRouteProofs2, while this file layers the kernel/invariant and extraspecial route4 refinements on top.

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

Nonterminal Fourier branch using the current candidate/target route, the kernel-module semantic split, and the route4 actual scalar central-extension pushout packet.

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

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

Current strongest finite-surjection equality route, combining the candidate scalar/Frattini split, target bridge split, kernel/invariant split, and extraspecial route4 refinement.