The corrected nonterminal branch (first chief + ⊆-minimal kernel + R case split)

This file replaces the unsound §7 kernel provider (see PROGRESS.md "SOUNDNESS FINDINGS": unconditional 1 < |Φ(K)|, least-form minimal_K, chief factor without the first condition, and unconditional 𝒳_R ≠ 0) by a manuscript-faithful branch:

• the chief factor is chosen first (FirstNonScalarChiefFactor, proven to exist);
• the kernel is the manuscript's ⊆-minimal K (KernelMinimal, proven to exist);
• the R = Φ(K) dichotomy of thm:closedrecursion is split honestly:
  • R = 1: "B = Y and the induction closes at the elementary stage" (l.4437, l.4542);
  • R ≠ 1: the closed recursion eq:Mstage + eq:recursionR1–eq:phasecovertransform (valid for any 𝒳_R, including 𝒳_R = 0 — prop:finalfourier assumes only R ≠ 1).

The two branch packets are recorded as residual axioms whose statements are exactly the manuscript's two cases of thm:closedrecursion — each strictly weaker than the previous unconditional providers, and each TRUE in the manuscript. They are the current honest §7/§8 frontier, to be decomposed further on this corrected foundation (the granular candidate/target/pushout machinery all re-applies over a block-and-concrete pair).

The corrected integrated route at the end reruns the strong induction and the §10 passage over the corrected branch.

The two manuscript-true branch residuals

The corrected nonterminal branch

theorem Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch_corrected (p : FramedPair) (h : ¬ScalarTerminal p) : Nonempty (FourierBranchData p)

The corrected nonterminal Fourier branch. From non-scalar-terminality alone: choose a first non-scalar chief factor (proven), a ⊆-minimal kernel (proven), and split on the R = Φ(K) dichotomy (proven) — exactly the shape of thm:closedrecursion. No unconditional |Φ(K)| > 1, no least-form kernel, no 𝒳_R ≠ 0.

The corrected integrated route

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

The recursive branch over the corrected nonterminal packet.

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

The corrected recursion step (terminal base unchanged — it is already proven).

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

Boundary-framed counts equal, over the corrected branch.

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

The corrected count theorem — |Sur(Γ_A, G)| = |Sur(G_{ℚ₂}, G)| for every finite G, through the manuscript-faithful §7 foundation.