A uniform root-discriminant bound of 255255

Mathematical statement

Let $L/\mathbb Q$ be a finite Galois number field whose Galois group is a $2$-group. Assume it is unramified at finite places outside $S=\{3,5,7,11,13,17\}$. Then $$|\operatorname{disc}(L)|\le255255^{[L:\mathbb Q]},\qquad255255=3\cdot5\cdot7\cdot11\cdot13\cdot17.$$

Consequently its root discriminant satisfies $|\operatorname{disc}(L)|^{1/[L:\mathbb Q]}\le255255$. Total reality is not an assumption of this discriminant theorem; it is supplied separately when the theorem is applied to the chosen tower.

Lean code

`ClassFieldTower.Sawin.discr_natAbs_le_of_sawin_ramification`

Published library source ↗Same source in NYLL ↗

theorem discr_natAbs_le_of_sawin_ramification
    (L : Type*) [Field L] [NumberField L] [IsGalois ℚ L]
    (hP : IsPGroup 2 Gal(L/ℚ))
    (hOutside : IsUnramifiedAtFinitePlacesOutside ℚ L sawinRationalPrimeSupport) :
    (NumberField.discr L).natAbs ≤ 255255 ^ Module.finrank ℚ L

In-scope Lean context

open scoped NumberField

open NumberField

noncomputable section

namespace ClassFieldTower.Sawin

Full declaration and proof

/-- The initial tower's arithmetic conditions give a discriminant bound
with one constant for all finite Galois number fields satisfying them. -/
theorem discr_natAbs_le_of_sawin_ramification
    (L : Type*) [Field L] [NumberField L] [IsGalois ℚ L]
    (hP : IsPGroup 2 Gal(L/ℚ))
    (hOutside : IsUnramifiedAtFinitePlacesOutside ℚ L sawinRationalPrimeSupport) :
    (NumberField.discr L).natAbs ≤ 255255 ^ Module.finrank ℚ L := by
  have : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
  obtain ⟨a, ha⟩ := hP.exists_card_eq
  rw [IsGalois.card_aut_eq_finrank] at ha
  apply AlgebraicNumberTheory.Discriminant.natAbs_discr_le_pow_of_coprime_support
    L 255255 (by decide)
  · rw [ha]
    exact Nat.Coprime.pow_right a (by decide : Nat.Coprime 255255 2)
  · intro q hq
    have hmem := (rationalPrime_mem_sawinRationalPrimeSupport_iff q).mp
      ((isUnramifiedAtFinitePlacesOutside_rat_iff_discr L sawinRationalPrimeSupport).mp
        hOutside q hq)
    have hProd : ∏ p ∈ sawinRationalPrimes, p = 255255 := by decide
    rw [← hProd]
    exact Finset.dvd_prod_of_mem (fun p : ℕ ↦ p) hmem

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

Farshid Hajir, Christian Maire, and Ravi Ramakrishna. Cutting towers of number fields. 2019. Cited as the arXiv preprint; develops cutting methods with refined Golod–Shafarevich estimates.
Jacques Martinet. Tours de corps de classes et estimations de discriminants. Inventiones mathematicae, 44, 65–73, 1978.