Five generators for the initial arithmetic group

Mathematical statement

Let $$S=\{3,5,7,11,13,17\},\qquad M=M_{2,S},\qquad G=\operatorname{Gal}(M/\mathbb Q),$$ where $S$ is viewed as the corresponding finite places. The theorem proves both that $G$ can be topologically generated by at most five elements and that its topological generator rank is exactly five. Here $M_{2,S}$ is the maximal totally real pro-$2$ extension of $\mathbb Q$ unramified at finite primes outside $S$.

The generator count is for the actual Galois group of the maximal real extension unramified outside $S$. It is not an assumed parameter of an abstract pro-$2$ group. In particular, ramification at $2$ is excluded by this support.

Lean code

`ClassFieldTower.Sawin.maximalRealProTwo_generatorRank`

Published library source ↗Same source in NYLL ↗

theorem maximalRealProTwo_generatorRank :
    TopologicallyGeneratedByAtMost 5
      (maximalRealProPOutside 2 sawinRationalPrimeSupport ≃ₐ[ℚ]
        maximalRealProPOutside 2 sawinRationalPrimeSupport) ∧
    topologicalGeneratorRank
      (maximalRealProPOutside 2 sawinRationalPrimeSupport ≃ₐ[ℚ]
        maximalRealProPOutside 2 sawinRationalPrimeSupport) = 5

In-scope Lean context

open scoped IsMulCommutative

namespace ClassFieldTower.Sawin

open ClassFieldTower.ProP ProCGroups.Generation ProCGroups.FiniteGeneration

Full declaration and proof

/-- The actual maximal real pro-two group is generated by five elements,
and five is its topological generator rank. -/
theorem maximalRealProTwo_generatorRank :
    TopologicallyGeneratedByAtMost 5
      (maximalRealProPOutside 2 sawinRationalPrimeSupport ≃ₐ[ℚ]
        maximalRealProPOutside 2 sawinRationalPrimeSupport) ∧
    topologicalGeneratorRank
      (maximalRealProPOutside 2 sawinRationalPrimeSupport ≃ₐ[ℚ]
        maximalRealProPOutside 2 sawinRationalPrimeSupport) = 5 := by
  classical
  let M : IntermediateField ℚ (AlgebraicClosure ℚ) :=
    maximalRealProPOutside 2 sawinRationalPrimeSupport
  let G : Type := M ≃ₐ[ℚ] M
  let : IsGalois ℚ M := maximalRealProPOutside_isGalois 2 sawinRationalPrimeSupport
  let : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
  let : (closedPowerCommutator 2 G).Normal := closedPowerCommutator_normal 2 G
  let : IsClosed (closedPowerCommutator 2 G : Set G) :=
    isClosed_closedPowerCommutator 2 G
  let Q : Type := powerCommutatorQuotient 2 G
  let : IsMulCommutative Q := powerCommutatorQuotient_isMulCommutative 2 G
  let : Module (ZMod 2) (Additive Q) := AddCommGroup.zmodModule (fun x ↦ by
    change (Additive.toMul x) ^ 2 = 1
    exact powerCommutatorQuotient_pow_eq_one 2 G (Additive.toMul x))
  have hCard : Nat.card Q = 32 := maximalRealProTwo_powerCommutatorQuotient_card
  let : Finite Q := Nat.finite_of_card_ne_zero (by rw [hCard]; decide)
  let : Module.Finite (ZMod 2) (Additive Q) := Module.Finite.of_finite
  have hCardAdd : Nat.card (Additive Q) = 32 :=
    (Nat.card_congr (Additive.toMul : Additive Q ≃ Q)).trans hCard
  have hDim : Module.finrank (ZMod 2) (Additive Q) = 5 := by
    have hPow : 2 ^ Module.finrank (ZMod 2) (Additive Q) = 2 ^ 5 := by
      rw [Module.natCard_eq_pow_finrank (K := ZMod 2), Nat.card_zmod] at hCardAdd
      exact hCardAdd
    exact Nat.pow_right_injective (by decide : 2 ≤ 2) hPow
  have hQuot : TopologicallyGeneratedByAtMost 5 Q := by
    rw [← hDim]
    exact topologicallyGeneratedByAtMost_finrank_zmod
  obtain ⟨s, hsCard, hsGen⟩ := hQuot
  let liftQ : Q → G := Function.surjInv (powerCommutatorQuotientMk_surjective 2 G)
  let t : Finset G := s.image liftQ
  have hImage : powerCommutatorQuotientMk 2 G '' (t : Set G) = (s : Set Q) := by
    apply Set.Subset.antisymm
    · rintro y ⟨x, hx, rfl⟩
      obtain ⟨q, hq, rfl⟩ := Finset.mem_image.mp hx
      have hLift : powerCommutatorQuotientMk 2 G (liftQ q) = q :=
        Function.surjInv_eq (powerCommutatorQuotientMk_surjective 2 G) q
      rw [hLift]
      exact hq
    · intro q hq
      refine ⟨liftQ q, Finset.mem_image.mpr ⟨q, hq, rfl⟩, ?_⟩
      exact Function.surjInv_eq (powerCommutatorQuotientMk_surjective 2 G) q
  have hProTwo : ProCGroups.ProC.HasPGroupOpenNormalBasis 2 G :=
    maximalRealProPOutside_galoisGroup_hasPGroupOpenNormalBasis
      2 sawinRationalPrimeSupport
  have hGen : TopologicallyGenerates (G := G) (t : Set G) := by
    apply (topologicallyGenerates_iff_powerCommutatorQuotient_image hProTwo).mpr
    rw [hImage]
    exact hsGen
  have hFiniteGeneration : TopologicallyFinitelyGenerated G := ⟨t, hGen⟩
  refine ⟨⟨t, Finset.card_image_le.trans hsCard, hGen⟩, ?_⟩
  exact (topologicalGeneratorRank_eq_powerCommutatorQuotient_finrank
    hProTwo hFiniteGeneration).trans hDim

Source credits and license

Copyright (c) 2026 Naganori Yamaguchi (https://github.com/n-yamaguchi-0729). All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Naganori Yamaguchi (assisted by OpenAI Codex)

References

Noga Alon, Thomas F. Bloom, W. T. Gowers, Daniel Litt, Will Sawin, Arul Shankar, Jacob Tsimerman, Victor Wang, and Melanie Matchett Wood. Remarks on the disproof of the unit distance conjecture. 2026. Proposition 2.3 states the bounded-root-discriminant totally real tower with infinitely many completely split primes congruent to one modulo four.
Luis Ribes and Pavel Zalesskii. Profinite Groups. Springer-Verlag Berlin Heidelberg, 2010. Second edition; background for Frattini quotients, generator rank, and pro-p presentations.