Documentation

Q2Presentation.Induction.CountsEqual

Stage H — the boundary-framed induction: finite surjection counts are equal (manuscript §9–§10) #

This is the culmination of the presentation theorem. It proves that the candidate group Γ_A (GammaA) and the local Galois group G_{ℚ₂} (GQ2Profinite) admit the same number of continuous surjections onto every finite group G:

  |Sur(Γ_A, G)| = |Sur(G_{ℚ₂}, G)|        (manuscript eq:allcounts, l.4589)

This single statement — finite_surjection_counts_equal — is THE deliverable fed to the one-sided profinite reconstruction lemma (Profinite/Reconstruction.lean, profinite_reconstruction_of_surj_counts), which then concludes Γ_A ≅ G_{ℚ₂} (thm:main).

The logical architecture (manuscript §9 sec:induction, §10 sec:allquotients) #

The proof has two layers, matching the manuscript exactly.

Layer 1 — the boundary-framed exact-image induction (Theorem 4.2, thm:fixedframe) #

The deepest object is the boundary-framed surjection count e_Γ^β(𝒴) = |boundaryFramedSurj B 𝒴 F| (manuscript Definition 4.1, Boundary/FramedTarget.lean). Theorem 4.2 asserts e_{Γ_A}^β(𝒴) = e_{G_{ℚ₂}}^β(𝒴) for every boundary-framed marked target 𝒴, proved by strong induction on the order of the marked 2-kernel |L_Y| (framedMeasure). The manuscript's induction is a dichotomy (subsec:exactimagerecursion):

boundaryFramed_counts_equal is this theorem, with the structural strong induction proved here, sorry-free (Nat.strong_induction_on on framedMeasure).

Layer 2 — passage to all finite quotients (§10, eq:allcounts) #

lem:tameframeexhaustion (l.4561) writes Sur(Γ, G) as the disjoint union, over the finite set of tame boundary frames T_A ↠ G/O₂(G), of the fixed-frame boundary-framed surjection sets with decoration E = 0 (using prop:epi-semantics). The frame set and the per-frame framed target depend only on G — not on the source. Summing the per-frame equalities from Layer 1 over the shared frame index gives finite_surjection_counts_equal. This passage is proved here (Cardinal.sum congruence) on top of the exhaustion decomposition.

What is proved vs. what is an isolated documented axiom #

Per the Stage-H mandate, the structural induction is genuinely proven; the irreducible local/combinatorial inputs are isolated as two heavily documented axioms, exactly as the §5/§6 local-CFT inputs (q2_local_tate_duality, q2_local_euler_poincare, q2_local_base_zeroCount, candidate_base_zeroCount) already are.

Neither axiom assumes the conclusion: the terminal branch of the recursion is the genuine base case (lem:scalarterminal, proved in the manuscript from the marked pro-2 identification), and the equality of the two surjection counts is derived from the per-frame equalities, themselves derived by the proven induction.

The framed-target index of the induction #

source
@[reducible, inline]
abbrev Q2Presentation.Induction.FramedPair :
Type 1

A framed pair (𝒴, F): a boundary-framed marked target together with a boundary frame for it (manuscript Definition 4.1 + eq:beta). This is the index of Theorem 4.2: the boundary-framed surjection count e_Γ^β is a function of the pair. The induction of sec:induction ranges over all such pairs simultaneously ("the induction is stated globally", l.1213), ordered by |L_Y|.

Equations
Instances For
    source
    noncomputable def Q2Presentation.Induction.framedMeasure (p : FramedPair) :
    ℕ

    The induction measure |L_Y|: the order of the marked 2-kernel of the framed target (manuscript: the strong induction of thm:fixedframe is on |L_Y|).

    Equations
    Instances For
      source
      noncomputable def Q2Presentation.Induction.framedCountA (p : FramedPair) :
      Cardinal.{0}

      The candidate boundary-framed surjection count e_{Γ_A}^β(𝒴) (eq:eGamma), as a cardinal |boundaryFramedSurj boundaryPackage_GammaA 𝒴 F|.

      Equations
      Instances For
        source
        noncomputable def Q2Presentation.Induction.framedCountQ (p : FramedPair) :
        Cardinal.{0}

        The local boundary-framed surjection count e_{G_{ℚ₂}}^β(𝒴) (eq:eGamma), as a cardinal |boundaryFramedSurj boundaryPackage_GQ2 𝒴 F|.

        Equations
        Instances For

          The closed exact-image recursion and the terminal base (manuscript §8–§9) #

          The single isolated combinatorial input of Stage H. See the module docstring for the full justification; in brief it is the manuscript dichotomy thm:closedrecursion ∨ lem:scalarterminal, with the recursion's source-independence supplied by cor:sourceinterface.

          source
          axiom Q2Presentation.Induction.boundaryFramed_recursion_step (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 closed exact-image recursion with terminal base (manuscript thm:closedrecursion l.4427, lem:strictdecrease l.4399, lem:scalarterminal l.4471, cor:sourceinterface l.3411). For every boundary-framed target p = (𝒴, F) one of two manuscript alternatives holds:

          • (terminal, lem:scalarterminal) the two boundary-framed counts are already equal — L_Y has only trivial-module chief factors, the count reduces through Y ≅ H ×_{H₂} Q to compatible maps Π → Q, and the fully marked pro-2 identification (prop:pro2) makes the candidate and local counts coincide; or

          • (recursive, thm:closedrecursion) there is a finite list of strictly smaller framed targets children (each with marked 2-kernel of order < |L_Y|, by lem:strictdecrease) and a single source-independent functional combine : List Cardinal → Cardinal — built from the common lift multiplicities, perfect pairings, cup–Bockstein form and base Gauss sums of cor:sourceinterface, together with the finite Fourier inversion eq:fourier and the central-cover transforms eq:recursionR1–eq:phasecovertransform — such that both counts are obtained by applying combine to that source's children counts: e_Γ(𝒴) = combine [e_Γ(𝒥) : 𝒥 ∈ children].

          The two sources share the same combine and children precisely because the source interface (cor:sourceinterface) is an equality of all the inputs — this is where the lifting comparison (E–F: q2_local_Z1_dim, lift_torsor_card, isAdjointBoundary_unique) and the quadratic comparison (G: candidate_gauss_eq_local_gauss, candidate_numZeros_eq_local) enter.

          This axiom isolates the §6/§8 Fourier–Gauss–Evens machinery and the central-cover combinatorics, which are not in mathlib; everything structural — the strong induction that turns this local step into the global equality — is proved in boundaryFramed_counts_equal below. The terminal alternative is a genuine base case, not an assumption of the theorem: the recursive alternative derives its equality from strictly smaller targets.

          Theorem 4.2: the boundary-framed counts are equal (PROVEN by strong induction) #

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

          Boundary-framed exact-image theorem (manuscript Theorem 4.2, thm:fixedframe, l.1205): for every boundary-framed marked target 𝒴 with frame F,

            e_{Γ_A}^β(𝒴) = e_{G_{ℚ₂}}^β(𝒴).

          Proved here, sorry-free, by strong induction on the marked 2-kernel order |L_Y| (framedMeasure), exactly the manuscript's induction of sec:induction.

          The structural heart of Stage H: the dichotomy of boundaryFramed_recursion_step is dispatched by the induction. In the terminal case the counts are directly equal. In the recursive case the same source-independent functional combine is applied to the two sources' children-count lists; those lists are equal entrywise by the induction hypothesis (each child has strictly smaller |L_Y|), hence combine returns equal values. Well-foundedness of < on ℕ (via Nat.strong_induction_on) makes this a complete, sorry-free structural induction.

          §10: passage to all finite quotients (sec:allquotients) #

          source
          axiom Q2Presentation.Induction.tameFrameExhaustion (G : Type) [Group G] [Finite G] [Nonempty G] :
          ∃ (Frames : Type) (Y : Frames → FramedPair), (Cardinal.mk (Profinite.SurjContHom GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))) = Cardinal.sum fun (φ : Frames) => framedCountA (Y φ)) ∧ Cardinal.mk (Profinite.SurjContHom GQ2Profinite (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))) = Cardinal.sum fun (φ : Frames) => framedCountQ (Y φ)

          Tame-frame exhaustion (manuscript lem:tameframeexhaustion, l.4561, with prop:epi-semantics). For a finite group G, every continuous surjection Γ ↠ G determines a unique tame boundary frame T_A ↠ G/O₂(G), and a boundary-framed surjection with decoration E = 0 and a fixed tame frame is exactly an ordinary surjection inducing that frame. Distinct tame frames give disjoint sets. Hence Sur(Γ, G) is the disjoint union over the tame frames of the fixed-frame boundary-framed counts:

            |Sur(Γ, G)| = Σ_{frame φ} e_Γ^β(𝒴_{G,φ})          (eq:allcounts derivation).

          The frame index Frames and the per-frame framed target Y φ depend only on G — the wild subgroup maps into O₂(G) and the frame T_A ↠ G/O₂(G) is a source-independent datum (lem:tameframeexhaustion). We therefore quantify the shared Frames/Y once, before the per-source decompositions: this is the formal record of "the fixed-frame sets are indexed by the same set of frames for both sources".

          This decomposition is the §10 finite-group / profinite bookkeeping (O₂(G), the characteristic marked wild subgroup, disjointness of frames, prop:epi-semantics), not in mathlib; it is isolated here as a documented axiom. The equality of the two surjection counts is then derived (not assumed) from Theorem 4.2 applied frame-by-frame.

          source
          theorem Q2Presentation.Induction.finite_surjection_counts_equal (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 DELIVERABLE — equality of all finite surjection counts (manuscript eq:allcounts, l.4589): for every finite group G,

            |Sur(Γ_A, G)| = |Sur(G_{ℚ₂}, G)|.

          This is the hypothesis of the one-sided profinite reconstruction lemma (profinite_reconstruction_of_surj_counts), the final input to Γ_A ≅ G_{ℚ₂} (thm:main).

          Proved here by combining the §10 tame-frame exhaustion with Theorem 4.2: both sides decompose, over the same finite set of tame frames, into fixed-frame boundary-framed counts (tameFrameExhaustion); each such per-frame pair has equal candidate and local counts by boundaryFramed_counts_equal; summing the equal summands over the shared index gives the result (Cardinal.sum congruence).

          Source interface — the comparison theorems justifying source-independence #

          The source-independence of the recursion functional combine (the single nontrivial hypothesis hidden inside boundaryFramed_recursion_step) is cor:sourceinterface, whose four items are equalities of the candidate and local source data. We record the corresponding already-proved comparison theorems here, to make explicit which results carry the recursion's source-independence:

          Acceptance checks #