Integrated current route, sixteenth refinement

Route16 keeps route15's assembly shape but swaps in the newest de-axiomatization sidecars:

• target K/R via the recovered Pro sidecar TargetKmodRRoute15BridgeProofs, replacing the two transport-final target leaves by the narrower same-tower bridge leaves;
• candidate scalar/Frattini via CandidateScalarFrattiniRoute16Proofs, replacing the two broad route15 candidate leaves by five smaller manuscript-shaped scalar/Frattini leaves;
• Section 7 kernel/head via MinimalBlockKernelConcreteRoute16Proofs, replacing the route15 independent kernel/head leaves by one coherent same-tower minimalBlock_kernelConcreteRoute16Data package;
• pushout/determinant via MinimalBlockPushoutRoute16Proofs, replacing the four independent determinant semantic leaves by one actual same-family determinant packet plus the semantic central-pushout family.

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

Route16 group tower: one coherent kernel/head package.

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

Route16 cover realization: target bridge from Pro, candidate scalar/Frattini route16, kernel route16, and the route15/16 structural target wiring.

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

Route16 nonterminal branch.

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

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

Route16 finite-surjection equality.