A five-generator presentation with at most six relations

The initial arithmetic group admits an actual finite minimal pro-2 presentation.

The counts leave room for additional splitting conditions: at $t=5/12$, one has $1-5t+6t^2=-1/24$. Minimality puts the existing relators at depth at least two, and sufficiently deep new relations can fit within that margin. This is the generator–relation strategy originating in Golod and Shafarevich’s class field tower argument, applied to the six-prime construction appearing in Remarks on the disproof of the unit distance conjecture.

Mathematical statement

Here $M_{2,S}$ denotes the maximal totally real pro-$2$ extension of $\mathbb Q$ unramified at finite primes outside $S$.

For $G=\operatorname{Gal}(M_{2,S}/\mathbb Q)$ with $S=\{3,5,7,11,13,17\}$, there exist a free pro-$2$ source, a natural number $r\le6$, and an actual presentation $$G\cong F_5/\overline{\langle\!\langle\rho_1,\ldots,\rho_r\rangle\!\rangle}$$ that is minimal on its five generators.

The formal object includes the continuous surjection and the displayed relators presenting its kernel. Minimality gives Zassenhaus depth at least two for these relators. The theorem says at most six relations, not exactly six.

Lean code

`ClassFieldTower.Sawin.exists_sawinInitialProTwo_minimalPresentation`

Published library source ↗Same source in NYLL ↗

theorem exists_sawinInitialProTwo_minimalPresentation :
    ∃ sourceData : FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{0, 0}
      (FiniteGroupClass.pGroup 2),
      ∃ r : ℕ, ∃ P : FiniteProPPresentation 2 5 r sourceData
        (maximalRealProPOutside 2 sawinRationalPrimeSupport ≃ₐ[ℚ]
          maximalRealProPOutside 2 sawinRationalPrimeSupport),
        P.IsMinimal ∧ r ≤ 6

In-scope Lean context

namespace ClassFieldTower.Sawin

open ProCGroups ClassFieldTower.ProP

private local instance initialPresentationPrimeTwo : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩

private local instance initialPresentationIsGalois :
    IsGalois ℚ (maximalRealProPOutside 2 sawinRationalPrimeSupport) :=
  maximalRealProPOutside_isGalois 2 sawinRationalPrimeSupport

Full declaration and proof

/-- The initial arithmetic group has an actual minimal presentation on five
generators and at most six relators. The chosen relator count attains the
least relation rank supplied by S1. -/
theorem exists_sawinInitialProTwo_minimalPresentation :
    ∃ sourceData : FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{0, 0}
      (FiniteGroupClass.pGroup 2),
      ∃ r : ℕ, ∃ P : FiniteProPPresentation 2 5 r sourceData
        (maximalRealProPOutside 2 sawinRationalPrimeSupport ≃ₐ[ℚ]
          maximalRealProPOutside 2 sawinRationalPrimeSupport),
        P.IsMinimal ∧ r ≤ 6 := by
  obtain ⟨hG, hr, _, _⟩ := sawinInitialProTwoGroup_structure.2.2.2
  obtain ⟨sourceData, d, P, hP⟩ := exists_presentation_relationCard_eq_minimal hG
  have hd : d = 5 :=
    (P.target_topologicalGeneratorRank_eq hP).symm.trans maximalRealProTwo_generatorRank.2
  subst d
  exact ⟨sourceData, _, P, hP, hr⟩

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.

E. S. Golod and I. R. Shafarevich. On the class field tower. Izvestiya Akademii Nauk SSSR. Seriya Matematicheskaya, 28 (2), 261–272, 1964. Original article in Russian.