Integrated current route, fourteenth refinement

Route14 is the first fully-composed route after the route12/route13 sidecar batch. It keeps the same finite-count theorem shape as route13, but routes the nonterminal Fourier branch through the strongest current manuscript-shaped providers:

• candidate scalar/Frattini data via CandidateScalarFrattiniSemanticRoute12Proofs;
• target same-tower quotient/action data via TargetKmodRSameTowerActualRoute12Proofs;
• kernel/Frattini lower tower data via MinimalBlockKernelFrattiniCoherentRoute13Proofs;
• head/invariant data via MinimalBlockHeadInvariantSemanticRoute12Proofs;
• determinant/pushout data via MinimalBlockCentralPushoutRoute12Proofs.

This intentionally exposes finer non-local packet leaves in the final axiom closure instead of hiding them behind older coarse residual names.

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

Route14 group tower: the route13 coherent kernel/Frattini lower tower plus the route12 same-raw-tower head/invariant semantic packet.

theorem Q2Presentation.Induction.centralCover_realization_proven_fine_from_selfGroupTowerCurrentIntegrated14 {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))

Route14 cover realization: route12 target and candidate refinements wired into one realization provider.

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

Route14 nonterminal branch.

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

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

Route14 finite-surjection equality.