1. Introduction and main theorem🔗

Theorem1.1

✓L∃∀Nused by 0

Theorem 1.2 of the paper (Presentation theorem).

The absolute Galois group \GQ is isomorphic to the profinite group topologically generated by

\sigma,\tau,x_0,x_1,

for which the closed normal subgroup generated by x_0,x_1 is pro-2, and which is subject to the two relations

\tau^\sigma=\tau^2

and

h_0u_1^{-1}x_1^\sigma c_0=1,

where the auxiliary words are defined in (1)–(3).

Lean code for Theorem1.1●1 theorem

theoremdefined in Q2Presentation/PresentationCorrect.lean

complete

theorem Q2Presentation.presentation_correct :
  NonemptyNonempty.{u} (α : Sort u) : Prop`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.
 (CategoryTheory.Iso.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : C) : Type vAn isomorphism (a.k.a. an invertible morphism) between two objects of a category.
The inverse morphism is bundled.

See also `CategoryTheory.Core` for the category with the same objects and isomorphisms playing
the role of morphisms. Q2Presentation.GammaAQ2Presentation.GammaA : ProfiniteGrp.{0}The candidate profinite group `Γ_A`, the cofiltered inverse limit (in
`ProfiniteGrp`) of all admissible finite marked quotients (manuscript
eq. `candidateinverse`).  ≅CategoryTheory.Iso.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : C) : Type vAn isomorphism (a.k.a. an invertible morphism) between two objects of a category.
The inverse morphism is bundled.

See also `CategoryTheory.Core` for the category with the same objects and isomorphisms playing
the role of morphisms.  Q2Presentation.GQ2ProfiniteQ2Presentation.GQ2Profinite : ProfiniteGrp.{0}The absolute Galois group `G_{ℚ₂} = Gal(Q̄₂/ℚ₂)` of the `2`-adic field
`ℚ₂ = ℚ_[2]`, as a profinite group.

Concretely it is `Gal(SeparableClosure ℚ_[2] / ℚ_[2])`, packaged as an object of
`ProfiniteGrp` by `InfiniteGalois.profiniteGalGrp`.  Since `ℚ_[2]` has
characteristic `0` its separable closure is an algebraic closure, so this is the
absolute Galois group in the usual sense, matching the manuscript's `G_{ℚ₂}`. )CategoryTheory.Iso.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : C) : Type vAn isomorphism (a.k.a. an invertible morphism) between two objects of a category.
The inverse morphism is bundled.

See also `CategoryTheory.Core` for the category with the same objects and isomorphisms playing
the role of morphisms.

theorem Q2Presentation.presentation_correct :
  NonemptyNonempty.{u} (α : Sort u) : Prop`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.

    (CategoryTheory.Iso.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : C) : Type vAn isomorphism (a.k.a. an invertible morphism) between two objects of a category.
The inverse morphism is bundled.

See also `CategoryTheory.Core` for the category with the same objects and isomorphisms playing
the role of morphisms. Q2Presentation.GammaAQ2Presentation.GammaA : ProfiniteGrp.{0}The candidate profinite group `Γ_A`, the cofiltered inverse limit (in
`ProfiniteGrp`) of all admissible finite marked quotients (manuscript
eq. `candidateinverse`).  ≅CategoryTheory.Iso.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : C) : Type vAn isomorphism (a.k.a. an invertible morphism) between two objects of a category.
The inverse morphism is bundled.

See also `CategoryTheory.Core` for the category with the same objects and isomorphisms playing
the role of morphisms. 
      Q2Presentation.GQ2ProfiniteQ2Presentation.GQ2Profinite : ProfiniteGrp.{0}The absolute Galois group `G_{ℚ₂} = Gal(Q̄₂/ℚ₂)` of the `2`-adic field
`ℚ₂ = ℚ_[2]`, as a profinite group.

Concretely it is `Gal(SeparableClosure ℚ_[2] / ℚ_[2])`, packaged as an object of
`ProfiniteGrp` by `InfiniteGalois.profiniteGalGrp`.  Since `ℚ_[2]` has
characteristic `0` its separable closure is an algebraic closure, so this is the
absolute Galois group in the usual sense, matching the manuscript's `G_{ℚ₂}`. )CategoryTheory.Iso.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : C) : Type vAn isomorphism (a.k.a. an invertible morphism) between two objects of a category.
The inverse morphism is bundled.

See also `CategoryTheory.Core` for the category with the same objects and isomorphisms playing
the role of morphisms.

**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.