A Martinet-type bounded-discriminant corollary

Mathematical statement

There exists a real number $C>0$ such that for every natural number $N$ there are an integer $d\ge N$ and a totally real number field $K$ with $$[K:\mathbb Q]=d,\qquad|\operatorname{disc}(K)|\le C^d.$$

Thus one constant controls the discriminants exponentially in the degree, while the degrees are unbounded. Equivalently, the root discriminants of the chosen fields are uniformly bounded. The field may depend on $N$, but $C$ does not.

Lean code

`ClassFieldTower.Sawin.exists_totallyReal_discr_le`

Published library source ↗Same source in NYLL ↗

theorem exists_totallyReal_discr_le :
    ∃ C : ℝ, 0 < C ∧ ∀ N : ℕ, ∃ d : ℕ, N ≤ d ∧
      ∃ (K : Type) (_ : Field K) (_ : NumberField K)
        (_ : NumberField.IsTotallyReal K),
        Module.finrank ℚ K = d ∧
          |(NumberField.discr K : ℝ)| ≤ C ^ d := by
  obtain ⟨rdBound, Q, _hQ, _hprimes, hfields⟩ :=
    sawin_totally_real_tower
  have hC : (0 : ℝ) < max 1 rdBound :=
    lt_of_lt_of_le zero_lt_one (le_max_left 1 rdBound)
  refine ⟨max 1 rdBound, hC, ?_⟩
  intro N
  obtain ⟨K, fieldK, _charZeroK, numberFieldK, totallyRealK,
    hN, hroot, _hsplit⟩ := hfields N
  have hdegree : (0 : ℝ) < (Module.finrank ℚ K : ℝ) :=
    Nat.cast_pos.mpr
      (Module.finrank_pos : 0 < Module.finrank ℚ K)
  have hrootC :
      |(NumberField.discr K : ℝ)| ^
          (Module.finrank ℚ K : ℝ)⁻¹ ≤ max 1 rdBound := by
    simpa only [one_div] using
      hroot.trans (le_max_right (1 : ℝ) rdBound)
  have hdiscr :
      |(NumberField.discr K : ℝ)| ≤
        (max 1 rdBound) ^ (Module.finrank ℚ K : ℝ) :=
    (Real.rpow_inv_le_iff_of_pos
      (abs_nonneg (NumberField.discr K : ℝ)) hC.le hdegree).mp hrootC
  refine ⟨Module.finrank ℚ K, hN, K, fieldK,
    numberFieldK, totallyRealK, rfl, ?_⟩
  simpa only [Real.rpow_natCast] using hdiscr

In-scope Lean context

namespace ClassFieldTower.Sawin

Full declaration and proof

/-- Totally real number fields of arbitrarily large degree satisfy a
uniform exponential bound on their absolute discriminants. -/
theorem exists_totallyReal_discr_le :
    ∃ C : ℝ, 0 < C ∧ ∀ N : ℕ, ∃ d : ℕ, N ≤ d ∧
      ∃ (K : Type) (_ : Field K) (_ : NumberField K)
        (_ : NumberField.IsTotallyReal K),
        Module.finrank ℚ K = d ∧
          |(NumberField.discr K : ℝ)| ≤ C ^ d := by
  obtain ⟨rdBound, Q, _hQ, _hprimes, hfields⟩ :=
    sawin_totally_real_tower
  have hC : (0 : ℝ) < max 1 rdBound :=
    lt_of_lt_of_le zero_lt_one (le_max_left 1 rdBound)
  refine ⟨max 1 rdBound, hC, ?_⟩
  intro N
  obtain ⟨K, fieldK, _charZeroK, numberFieldK, totallyRealK,
    hN, hroot, _hsplit⟩ := hfields N
  have hdegree : (0 : ℝ) < (Module.finrank ℚ K : ℝ) :=
    Nat.cast_pos.mpr
      (Module.finrank_pos : 0 < Module.finrank ℚ K)
  have hrootC :
      |(NumberField.discr K : ℝ)| ^
          (Module.finrank ℚ K : ℝ)⁻¹ ≤ max 1 rdBound := by
    simpa only [one_div] using
      hroot.trans (le_max_right (1 : ℝ) rdBound)
  have hdiscr :
      |(NumberField.discr K : ℝ)| ≤
        (max 1 rdBound) ^ (Module.finrank ℚ K : ℝ) :=
    (Real.rpow_inv_le_iff_of_pos
      (abs_nonneg (NumberField.discr K : ℝ)) hC.le hdegree).mp hrootC
  refine ⟨Module.finrank ℚ K, hN, K, fieldK,
    numberFieldK, totallyRealK, rfl, ?_⟩
  simpa only [Real.rpow_natCast] using hdiscr

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 Lean Eval:
https://github.com/leanprover/lean-eval/blob/6b4b87b672f5301f24983a12fda65dac608453ce/generated/martinet_totally_real_towers/Challenge.lean
Lean Eval repository: Copyright 2026 Lean FRO, LLC; Apache 2.0.

References

Jacques Martinet. Tours de corps de classes et estimations de discriminants. Inventiones mathematicae, 44, 65–73, 1978.