The presentation theorem Γ_A ≅ Gal(Q̄₂/ℚ₂) (the project's final result)

This is the capstone of the whole formalization. It assembles the two prepared deliverables into the manuscript's main theorem (thm:main):

• the candidate 4-generator profinite presentation Γ_A (Q2Presentation.GammaA, Stage B) is topologically finitely generated (tfg_GammaA, from gammaGen_topologically_generate), and
• it has the same number of continuous surjections onto every finite group as the absolute Galois group G_{ℚ₂} = Gal(Q̄₂/ℚ₂) (Q2Presentation.GQ2Profinite, the Local stage) — this is Stage H's integrated semantic finite count theorem.

Feeding these to the one-sided profinite reconstruction lemma (profinite_reconstruction_of_surj_counts, Stage B6 / Lemma 2.5) yields

  presentation_correct : Nonempty (GammaA ≅ GQ2Profinite).

i.e. the candidate presentation is the absolute Galois group of ℚ₂.

Logical status

The result is unconditional modulo exactly the project's documented axioms (no sorry anywhere):

• the standard Lean axioms propext, Classical.choice, Quot.sound;
• the isolated local class-field-theory inputs (Labute's classification labute_GQ2_maxPro2_marked, the local tame quotient gq2_tame_quotient, local Tate duality / Euler–Poincaré q2_local_tate_duality / q2_local_euler_poincare, the local base zero-count q2_local_base_zeroCount); and
• the remaining manuscript-backed residual inputs exposed by the §7/§8/§10 de-axiomatization sidecars.

Run #print axioms presentation_correct (at the end of this file) for the exact closure.

A note on the two interface adjustments

• Gen (the four marked generators) is given its Fintype instance here so that Finset.univ.image gammaGen names the finite generating set required by TopologicallyFinitelyGenerated.
• The reconstruction lemma quantifies over all finite groups G with no Nonempty G hypothesis, whereas finite_surjection_counts_equal carries a (redundant) [Nonempty G]. Every group is nonempty (⟨1⟩), so surj_counts_equal bridges the two.

instance Q2Presentation.instFintypeGen : Fintype Gen

The four marked generators σ, τ, x₀, x₁ form a finite type. (Gen already carries DecidableEq; this records its four-element enumeration so that Finset.univ : Finset Gen — and hence the finite generating set Finset.univ.image gammaGen of Γ_A — is available.)

Equations

• Q2Presentation.instFintypeGen = { elems := {Q2Presentation.Gen.sigma, Q2Presentation.Gen.tau, Q2Presentation.Gen.x0, Q2Presentation.Gen.x1}, complete := Q2Presentation.instFintypeGen._proof_1 }

theorem Q2Presentation.tfg_GammaA : Profinite.TopologicallyFinitelyGenerated GammaA

Γ_A is topologically finitely generated. The finite generating set is the image of the four universal generators, Finset.univ.image gammaGen, whose coercion to a Set is exactly Set.range gammaGen; its topological closure is ⊤ by gammaGen_topologically_generate. This is the hypothesis of the one-sided profinite reconstruction lemma asserting that Γ_A is t.f.g.

theorem Q2Presentation.surj_counts_equal (G : Type) [Group G] [Finite 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, packaged for the reconstruction lemma. This is finite_surjection_counts_equal_corrected — the manuscript-faithful §7 route (first non-scalar chief factor + ⊆-minimal kernel + the R = Φ(K) dichotomy of thm:closedrecursion; see Induction/Section7ChiefKernelFoundation.lean and PROGRESS.md "SOUNDNESS FINDINGS") — with its redundant [Nonempty G] discharged: every group is nonempty via its identity ⟨1⟩. The shape now matches the hypothesis h of profinite_reconstruction_of_surj_counts, which quantifies over all finite groups without a nonemptiness assumption.

theorem Q2Presentation.presentation_correct : Nonempty (GammaA ≅ GQ2Profinite)

THE MAIN THEOREM (manuscript thm:main). The candidate 4-generator profinite presentation Γ_A is isomorphic, as a profinite group, to the absolute Galois group G_{ℚ₂} = Gal(Q̄₂/ℚ₂) of the 2-adic field.

The proof is one application of the one-sided profinite reconstruction lemma (profinite_reconstruction_of_surj_counts): Γ_A is topologically finitely generated (tfg_GammaA) and has the same number of continuous surjections onto every finite group as G_{ℚ₂} (surj_counts_equal, i.e. Stage H's integrated semantic finite count theorem), so the two profinite groups are isomorphic.

Final acceptance audit