Stage H capstone count theorem, routed through the de-axiomatized sidecars

This file keeps CountsEqual.lean intact as the original structural induction module, but reproves the final count equality through the proven sidecar replacements:

• boundaryFramed_scalarTerminal_equal_proven for the scalar-terminal branch;
• centralCover_realization_proven_fine_integrated for the §8 central-cover realization;
• tameFrameExhaustion_proven for the §10 frame exhaustion.

The remaining axioms in this route are therefore the finer manuscript-backed residuals, not the old monolithic boundaryFramed_recursion_step and tameFrameExhaustion.

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

The nonterminal Fourier packet, routed through the refined §8 central-cover data.

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

Recursive branch using the refined nonterminal packet.

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

Exact replacement for boundaryFramed_recursion_step, using sidecar theorems.

theorem Q2Presentation.Induction.boundaryFramed_counts_equal_refined (p : FramedPair) : framedCountA p = framedCountQ p

Boundary-framed counts equal, with the recursion step routed through sidecars.

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

Equal finite surjection counts, using the refined frame exhaustion and count theorem.