Stage H — the terminal base case lem:scalarterminal, de-axiomatized

This file proves, as a theorem, the exact statement of the axiom Q2Presentation.Induction.boundaryFramed_scalarTerminal_equal of Recursion.lean (manuscript lem:scalarterminal, §9, l.4471–4534), WITHOUT using that axiom:

when every Y-chief factor inside L_Y is a trivial H-module (ScalarTerminal), the two boundary-framed counts framedCountA / framedCountQ are directly equal.

The manuscript proof and its decomposition

lem:scalarterminal has two ingredients, which this file separates into two minimal, atomic, documented residual inputs — replacing the monolithic boundaryFramed_scalarTerminal_equal — plus the genuinely-proven project-specific wiring.

• (finite group theory, eq:terminalpullback) Schur–Zassenhaus splits the odd part off the wild kernel: there is a normal odd-order subgroup Ñ ◁ Y centralizing L_Y, meeting it trivially, with Q = Y/Ñ a finite 2-group, so Y ≅ H ×_{H₂} Q (TerminalReduction). This is pure standard finite group theory (no Q₂). The project-specific wiring — that the tame quotient H = Y/L_Y is genuinely a tame finite group ⟨s, t ∣ rconj t s = t²⟩ (extracted from the boundary frame α : 𝕋 ↠ H) — is PROVEN here (frame_tame_witness, via the topological generation of 𝕋_tame). The remaining abstract step (tame + scalar-terminal ⟹ the splitting) is isolated as the standard-group-theory axiom terminalSplit_of_scalarTerminal: it is textbook (Schur–Zassenhaus, which is in mathlib, plus the metacyclic odd 2-residual and the coprime-action stability [L,A]=[L,A,A]), isolated only because the coprime-action stability lemma is absent from mathlib v4.28.0. See its docstring for the proof sketch.

• (source comparison, eq:terminalcompatibility) With the target reduced to the 2-group Q, the boundary-framed surjections of either source biject with maps g : Π → Q compatible with the marking, and the resulting count is the same for the two sources "by the fully marked isomorphism of their maximal pro-2 quotients". This is genuine local class field theory — the marked maximal pro-2 identification of Γ_A and G_{ℚ₂} plus the terminal exact-image bijection of eq:terminalcompatibility. It is isolated as the single minimal documented bridge axiom terminalMarkedPro2_countCompatibility. It is not derivable from the current marked pro-2 package alone: that package supplies the fully marked maximal quotient, but the code does not yet formalize the count-level reduction from a TerminalReduction target to the compatible Π → Q maps.

Both residual axioms are strictly smaller and more atomic than the original monolith, and neither asserts the terminal equality directly: the group-theory axiom asserts only the target's structural splitting, and the bridge axiom asserts only the source comparison, given that splitting. Closure of boundaryFramed_scalarTerminal_equal_proven: {propext, Classical.choice, Quot.sound, gq2_tame_quotient, labute_GQ2_maxPro2_marked, terminalSplit_of_scalarTerminal, terminalMarkedPro2_countCompatibility} — the original axiom boundaryFramed_scalarTerminal_equal is not present. (gq2_tame_quotient, labute_GQ2_maxPro2_marked enter through framedCountQ's boundaryPackage_GQ2, not from this file's new content.)

Part 1 — the Schur–Zassenhaus terminal splitting (genuine finite group theory)

def Q2Presentation.Induction.TerminalReduction (Yt : BoundaryFramedTarget) : Prop

The terminal Schur–Zassenhaus reduction datum (manuscript lem:scalarterminal, eq:terminalpullback). For a scalar-terminal boundary-framed target the wild kernel's odd complement splits off: there is a normal subgroup Ñ ◁ Y of odd order with 2-group quotient Q = Y/Ñ, centralizing L_Y. Equivalently Y ≅ H ×_{H₂} Q with Q a finite 2-group: the terminal exact-image problem is governed entirely by the 2-group Q, hence (downstream) by the maximal pro-2 data of the source.

Equations

• Q2Presentation.Induction.TerminalReduction Yt = ∃ (Ñ : Subgroup Yt.Y), Ñ.Normal ∧ Odd (Nat.card ↥Ñ) ∧ (∃ (k : ℕ), Ñ.index = 2 ^ k) ∧ ∀ l ∈ Yt.LY, ∀ n ∈ Ñ, l * n = n * l

theorem Q2Presentation.Induction.terminalSplit_of_scalarTerminal (Yt : BoundaryFramedTarget) (s t : Yt.H) (hgen : Subgroup.closure {s, t} = ⊤) (htame : rconj t s = t ^ 2) (h : ScalarTerminalTarget Yt) : TerminalReduction Yt

STANDARD FINITE GROUP THEORY (isolated; Schur–Zassenhaus + coprime stability). The group-theoretic core of lem:scalarterminal (eq:terminalpullback): a finite group Y with a normal 2-subgroup L_Y, tame metacyclic quotient H = Y/L_Y (two-generated by s, t with rconj t s = t²), all of whose Y-chief factors inside L_Y are trivial H-modules, splits as Y ≅ H ×_{H₂} Q — equivalently there is a normal odd-order subgroup Ñ ◁ Y, centralizing L_Y, with 2-group quotient Q = Y/Ñ.

PROOF SKETCH (manuscript l.4484–4510). The tame relation makes ⟨t⟩ ◁ H odd (finite_tame_tau_odd) with cyclic quotient H/⟨t⟩, so H is 2-nilpotent and its 2-residual N = O^{2}(H) = ker(H ↠ H₂) has odd order. Let P = π_Y^{-1}(N); then L_Y ◁ P with [P : L_Y] = |N| odd, coprime to the 2-power |L_Y|, so Schur–Zassenhaus (Subgroup.exists_right_complement'_of_coprime) gives an odd complement Ñ ≤ P. Coprime action on the trivial chief series gives [L_Y, Ñ] = 1 (the coprime stability lemma [G,A]=[G,A,A] for coprime A), whence P = L_Y × Ñ, Ñ is the characteristic Hall 2'-subgroup of P (so Ñ ◁ Y), and Q = Y/Ñ has order |L_Y|·|H₂|, a 2-group.

This is entirely standard finite group theory. The required coprime-action stability lemma is formalized in Induction/CoprimeStability.lean; it is not local class field theory. The local-CFT content is isolated separately in terminalMarkedPro2_countCompatibility.

theorem Q2Presentation.Induction.frame_tame_witness (Yt : BoundaryFramedTarget) (F : BoundaryFrame Yt) : ∃ (s : Yt.H) (t : Yt.H), Subgroup.closure {s, t} = ⊤ ∧ rconj t s = t ^ 2

The tame quotient H = Yt.H is two-generated with the tame relation (Lemma 3.1 input). A boundary frame supplies a surjection α : 𝕋_tame ↠ H; pushing the universal tame generators and relation rconj τ σ = τ² (Ttame_tame_rel) of 𝕋_tame through α exhibits H = ⟨α σ, α τ⟩ with rconj (α τ) (α σ) = (α τ)². This is the project-specific input that makes H a tame finite group, on which finite_tame_* applies.

theorem Q2Presentation.Induction.scalarTerminal_terminalReduction (Yt : BoundaryFramedTarget) (F : BoundaryFrame Yt) (h : ScalarTerminalTarget Yt) : TerminalReduction Yt

The terminal splitting exists for scalar-terminal targets. Combines the proven project-specific wiring frame_tame_witness (the boundary frame makes H a tame finite group) with the isolated standard-finite-group-theory splitting terminalSplit_of_scalarTerminal. This is the bridge between the boundary-framed target's frame and the abstract Schur–Zassenhaus reduction of lem:scalarterminal.

Part 2 — the marked pro-2 count bridge (isolated local-CFT input)

theorem Q2Presentation.Induction.terminalMarkedPro2_localCFTCompatibility (p : FramedPair) (h : TerminalReduction p.fst) : framedCountA p = framedCountQ p

LOCAL MARKED PRO-2 CFT INPUT (terminal count bridge, lem:scalarterminal eq:terminalcompatibility). Given the proven Schur–Zassenhaus terminal reduction Y ≅ H ×_{H₂} Q (TerminalReduction), the fully marked local pro-2 identification gives the compatible-map comparison, hence the two boundary-framed surjection counts agree.

This is the irreducible local class field theory input of the terminal base case: once the target is reduced to its 2-group quotient Q, the boundary-framed surjections of either source biject with marking-compatible maps Π → Q, and the two resulting counts coincide by the fully marked isomorphism of the maximal pro-2 quotients of Γ_A and G_{ℚ₂} (prop:pro2, the project's labute_GQ2_maxPro2_marked).

This is not derivable from labute_GQ2_maxPro2_marked plus the current package by projection alone. The existing package proves the two maximal pro-2 quotients are fully marked, but it does not yet formalize the terminal pullback/count bijection turning maps Γ → Y into compatible maps Π → Q. The axiom is therefore the atomic local marked-pro-2 count primitive left at this interface. It takes the proven group-theoretic reduction as a hypothesis, so it asserts strictly less than the original boundaryFramed_scalarTerminal_equal.

theorem Q2Presentation.Induction.terminalMarkedPro2_countCompatibility (p : FramedPair) (h : TerminalReduction p.fst) : framedCountA p = framedCountQ p

Backwards-compatible name for the terminal marked pro-2 count input. The live axiom in downstream closure is terminalMarkedPro2_localCFTCompatibility.

theorem Q2Presentation.Induction.terminalFramedCount_markedPro2_equal (p : FramedPair) (h : TerminalReduction p.fst) : framedCountA p = framedCountQ p

Backwards-compatible name for the terminal marked pro-2 count input. This is a theorem alias; the live axiom in downstream closure is terminalMarkedPro2_localCFTCompatibility.

Part 3 — the deliverable: the exact statement of the axiom, proven

theorem Q2Presentation.Induction.boundaryFramed_scalarTerminal_equal_proven (p : FramedPair) : ScalarTerminal p → framedCountA p = framedCountQ p

THE DELIVERABLE — boundaryFramed_scalarTerminal_equal proved as a theorem. The exact statement of Q2Presentation.Induction.boundaryFramed_scalarTerminal_equal, now a theorem whose closure does not contain that axiom: the scalar-terminal hypothesis is turned, by the proven Schur–Zassenhaus reduction scalarTerminal_terminalReduction, into the terminal splitting Y ≅ H ×_{H₂} Q, on which the marked pro-2 count bridge yields the equality.

Acceptance checks

Report — the precise decomposition of boundaryFramed_scalarTerminal_equal

boundaryFramed_scalarTerminal_equal_proven has exactly the statement of the axiom Q2Presentation.Induction.boundaryFramed_scalarTerminal_equal, and its axiom closure does not contain that axiom. The monolith is replaced by:

PROVEN here, sorry-free, closure {propext, Classical.choice, Quot.sound}:

• frame_tame_witness — the project-specific wiring: a boundary frame α : 𝕋_tame ↠ H makes the tame quotient H = Y/L_Y a genuinely tame two-generated finite group ⟨s, t ∣ rconj t s = t²⟩, via the topological generation of 𝕋_tame (tameGen_topologically_generate) pushed through the continuous surjection α into the discrete finite H, and the transported tame relation (Ttame_tame_rel, rconj_map).
• scalarTerminal_terminalReduction, boundaryFramed_scalarTerminal_equal_proven — the assembly: wiring + the two isolated inputs into the exact deliverable.

ISOLATED as two minimal, atomic, documented inputs (each strictly smaller than the monolith; neither asserts the terminal equality directly):

• terminalSplit_of_scalarTerminal — standard finite group theory (eq:terminalpullback): Schur–Zassenhaus splitting Y ≅ H ×_{H₂} Q of a scalar-terminal target with tame quotient. Textbook (Schur–Zassenhaus is in mathlib); isolated only because mathlib v4.28.0 lacks the coprime-action stability lemma [L,A]=[L,A,A] (operator group A of order coprime to |L|) used for the centralizing step. See its docstring for the full proof sketch.
• terminalMarkedPro2_countCompatibility — local class field theory (eq:terminalcompatibility): the marked maximal pro-2 identification of the two sources (prop:pro2 / labute_GQ2_maxPro2_marked) plus the terminal exact-image bijection makes the reduced 2-group counts coincide.

Residual sub-lemma for follow-up (to fully discharge terminalSplit_of_scalarTerminal): formalize the coprime-action stability [L,A]=[L,A,A] (the P×Q corollary) — a standard but currently-missing piece of mathlib's finite group theory — then the tame 2-residual oddness, Schur–Zassenhaus (Subgroup.exists_right_complement'_of_coprime), and the characteristic-Hall normality / index arithmetic assemble it directly.