One infinite prime set splitting in fields of unbounded degree

Mathematical statement

There are a real constant $B$ and an infinite set $Q$ of primes, all congruent to $1$ modulo $4$, such that for every $N$ there is a totally real number field $F$ with $$[F:\mathbb Q]\ge N,\qquad |\operatorname{disc}(F)|^{1/[F:\mathbb Q]}\le B,$$ and every $q\in Q$ splits completely in $F$.

The implementation chooses $B=255255$. Its explicit splitting conclusion supplies $[F:\mathbb Q]$ distinct maximal ideals of $\mathcal O_F$ containing $q$. For a rational prime in a number field, this maximal number of distinct primes above $q$ expresses complete splitting.

Lean code

`ClassFieldTower.Sawin.sawin_totally_real_tower`

Published library source ↗Same source in NYLL ↗

theorem sawin_totally_real_tower :
    ∃ (rdBound : ℝ) (Q : Set ℕ), Q.Infinite ∧ (∀ q ∈ Q, q.Prime ∧ q % 4 = 1) ∧
      ∀ N : ℕ, ∃ (F : Type) (_ : Field F) (_ : CharZero F) (_ : NumberField F)
        (_ : IsTotallyReal F),
        N ≤ Module.finrank ℚ F ∧
        (|(NumberField.discr F : ℝ)|) ^ ((1 : ℝ) / Module.finrank ℚ F) ≤ rdBound ∧
        ∀ q ∈ Q, ∃ (factors : Finset (Ideal (𝓞 F))),
          factors.card = Module.finrank ℚ F ∧
          ∀ p ∈ factors, p.IsMaximal ∧ (q : 𝓞 F) ∈ p

In-scope Lean context

open scoped NumberField

open NumberField IsDedekindDomain

namespace ClassFieldTower.Sawin

open AlgebraicNumberTheory.PrimeSelection

open AlgebraicNumberTheory.DiscriminantBounds

Full declaration and proof

/-- Sawin's totally real tower, with one prime set fixed before the degree bound. -/
theorem sawin_totally_real_tower :
    ∃ (rdBound : ℝ) (Q : Set ℕ), Q.Infinite ∧ (∀ q ∈ Q, q.Prime ∧ q % 4 = 1) ∧
      ∀ N : ℕ, ∃ (F : Type) (_ : Field F) (_ : CharZero F) (_ : NumberField F)
        (_ : IsTotallyReal F),
        N ≤ Module.finrank ℚ F ∧
        (|(NumberField.discr F : ℝ)|) ^ ((1 : ℝ) / Module.finrank ℚ F) ≤ rdBound ∧
        ∀ q ∈ Q, ∃ (factors : Finset (Ideal (𝓞 F))),
          factors.card = Module.finrank ℚ F ∧
          ∀ p ∈ factors, p.IsMaximal ∧ (q : 𝓞 F) ∈ p := by
  classical
  let instPrimeTwo : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
  obtain ⟨primes, L, hGal, _, hInfinite, hL, hprimes, _, hsplit⟩ :=
    exists_sawinInfinite_totallyReal_split_field
  let Q : Set ℕ := Set.range (fun n : ℕ ↦ (primes n).val)
  have hQ : Q.Infinite :=
    Set.infinite_of_forall_exists_gt
      (fun a ↦ ⟨(primes a).val, ⟨a, rfl⟩, (hprimes a).1⟩)
  refine ⟨255255, Q, hQ, ?_, ?_⟩
  · rintro q ⟨n, rfl⟩
    exact ⟨(primes n).property, (hprimes n).2.2⟩
  · intro N
    obtain ⟨E, hE, hN⟩ :=
      @AlgebraicNumberTheory.exists_finiteGaloisIntermediateField_le_finrank_ge_of_infinite_aut
        ℚ (AlgebraicClosure ℚ) _ _ _ L hGal hInfinite N
    let instNumberFieldE : NumberField E := NumberField.of_module_finite ℚ E
    let instGalE : IsGalois ℚ E := E.isGalois
    have hAdm :=
      (isAdmissibleFiniteLayer_iff_le_maximalRealProPOutside
        2 sawinRationalPrimeSupport E).mpr (hE.trans hL)
    let instTotallyRealE : IsTotallyReal E :=
      (isUnramifiedAtInfinitePlaces_rat_iff_isTotallyReal E).mp hAdm.2.2
    have hdiscr := discr_natAbs_le_of_sawin_ramification E hAdm.1 hAdm.2.1
    have hroot := rootDiscr_le_of_natAbs_discr_le_pow E 255255 hdiscr
    refine ⟨E, inferInstance, inferInstance, inferInstance, inferInstance, hN, ?_, ?_⟩
    · simpa only [NumberField.rootDiscr_def, Int.cast_abs, one_div, Nat.cast_ofNat] using hroot
    · rintro q ⟨n, rfl⟩
      exact exists_finset_maximalIdeals_of_finitePlaceSplitsCompletely
        E (primes n) (hsplit E hE n)

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)
Statement adapted from Formal Conjectures:
https://github.com/google-deepmind/formal-conjectures/blob/8323e878b83fcd7f4a448256069352a265460d75/FormalConjectures/ErdosProblems/90.lean#L193
Original statement: Copyright 2025 The Formal Conjectures Authors; Apache 2.0.

References

Will Sawin. An explicit lower bound for the unit distance problem. 2026. The arithmetic tower ingredients are related to Lemmas 11–12; the library does not formalize the whole unit-distance argument.
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.