Integrated Route201: Route200 with candidate pointwise atoms lowered to actual split

This route keeps the Route200 non-candidate surface unchanged:

• Section 7 kernel provider from Section7KernelRoute200Closers;
• Route199 determinant-semantic pushout provider;
• Route164 target projection/action surface.

It only swaps the Route200 candidate insertion point. Instead of calling centralCover_candidateLiftPartitionData_from_candidateRoute197PointwiseCurrentLowerClosers, which exposes the seven Route146 pointwise scalar/Frattini atoms, it calls the Route201 provider from CandidateRoute201ActualPointwiseClosers. The expected candidate closure is therefore the two actual Section 8 inputs

• centralCover_candidateActualMiddleRLiftObstructionMapData;
• centralCover_candidateActualFrattiniAffineFiberExactImageEquivData.

The seven Route200 candidate atoms should be absent from the axiom closure of the finite-count theorem below.

theorem Q2Presentation.Induction.centralCover_realization_proven_fine_from_selfGroupTowerCurrentIntegrated201CandidateActualKernel200Pushout199Target164 {p : FramedPair} {chief : NonScalarChiefFactor p} (G : MinimalBlockGroupTowerData p chief) (h : ¬ScalarTerminal p) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData G.preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) : Nonempty (CoverRealization (G.toMinimalBlock h Fdet A Rdet))

Route201 realization provider: Route200 target/kernel/pushout surface with the candidate source-side packet routed through the actual middle/Frattini split rather than the seven pointwise Route146 atoms.

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

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

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