An explicit count of number fields of bounded discriminant

Mathlib's NumberField.finite_of_discr_bdd is the qualitative summit of geometry of numbers: inside a fixed extension A / ℚ, the number fields K with |discr K| ≤ N form a finite set. Its proof bounds the degree of such a K (rank_le_rankOfDiscrBdd), bounds the conjugates of a primitive integral generator (minkowskiBound_lt_boundOfDiscBdd, the convex-body input), and so exhibits each K as ℚ⟮x⟯ for x a root of an integer polynomial of bounded degree and coefficient height; finiteness follows because there are finitely many such polynomials. The proof extracts the finiteness of that generating set but discards the count.

This file is the effective Hermite--Minkowski count (the Layer-2 summit of the effective-bounds roadmap): an explicit upper bound on the number of such fields. We re-run the generating-set step of Mathlib's argument to expose the explicit polynomial bounds, then feed them to the elementary field-counting lemma assembled in TauCeti.IntermediateField (built on the bounded-polynomial root count of TauCeti.Algebra.Polynomial). The result is

#{K : |discr K| ≤ N} ≤ (2 * C + 1) ^ (D + 1) * D,

with D = rankOfDiscrBdd N Mathlib's explicit degree bound and C = coeffBoundOfDiscrBdd N an explicit coefficient bound derived from Mathlib's Minkowski bound boundOfDiscBdd N.

Main results

• coeffBoundOfDiscrBdd: an explicit height bound for the integer minimal polynomials of primitive generators of number fields of discriminant ≤ N, uniform over real and complex generators.
• NumberField.exists_mem_rootSet_eq_adjoin_of_abs_discr_le: each such field is generated by a root of an integer polynomial of degree ≤ rankOfDiscrBdd N and height ≤ coeffBoundOfDiscrBdd N.
• NumberField.ncard_setOf_finiteDimensional_abs_discr_le_le: the explicit count.

The remainder of the file is the consumer-facing API layer over that count, packaging the exact constants and recording the monotonicities that later effective estimates need:

• hermiteCountBound and hermiteCountBound_mono: the polynomial-count expression (2C+1)^(D+1)·D as a function of the degree and coefficient-height bounds, monotone in both.
• ncard_setOf_finiteDimensional_abs_discr_le_le_of_bounds: the count using any larger degree and coefficient-height bounds for the same threshold.
• ncard_setOf_finiteDimensional_abs_discr_le_le_of_threshold_le / ..._of_threshold_bounds: counting the fields with |d_K| ≤ N using the constants attached to any larger threshold M, optionally coarsened further.
• ncard_setOf_finiteDimensional_natAbs_discr_le_le_*: the same family restated for the natural-number discriminant inequality (discr K).natAbs ≤ N that later estimates carry.

Provenance

The generating-set construction (the case split on a real or complex infinite place, the use of exists_primitive_element_lt_of_isReal / exists_primitive_element_lt_of_isComplex and Embeddings.coeff_bdd_of_norm_le, and the final IntermediateField.lift identification) follows the proofs of NumberField.hermiteTheorem.finite_of_discr_bdd_of_isReal and ..._of_isComplex in Mathlib's Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean; here those proofs are recast to return the explicit generating set rather than only its finiteness. No formal code is vendored verbatim.

noncomputable def NumberField.coeffBoundOfDiscrBdd (N : ℕ) : ℕ

An explicit height bound for the integer minimal polynomial of a primitive generator of a number field of discriminant ≤ N. It is ⌈M ^ D * (D.choose (D / 2))⌉₊ where D = rankOfDiscrBdd N is Mathlib's degree bound and M = max √(1 + boundOfDiscBdd N ^ 2) 1 dominates the per-conjugate bound of both the real and complex primitive elements of finite_of_discr_bdd.

theorem NumberField.exists_mem_rootSet_eq_adjoin_of_abs_discr_le (A : Type u_1) [Field A] [CharZero A] [DecidableEq A] {N : ℕ} (K : IntermediateField ℚ A) (hK₀ : FiniteDimensional ℚ ↥K) (hK : |discr ↥K| ≤ ↑N) : ∃ x ∈ ⋃ (f : Polynomial ℤ), ⋃ (_ : f.natDegree ≤ hermiteTheorem.rankOfDiscrBdd N ∧ ∀ (i : ℕ), |f.coeff i| ≤ ↑(coeffBoundOfDiscrBdd N)), ↑(Polynomial.map (algebraMap ℤ A) f).roots.toFinset, K = ℚ⟮x⟯

Effective Hermite--Minkowski, generating step. Each number field K (a finite extension of ℚ inside A) with |discr K| ≤ N is generated over ℚ by a root in A of an integer polynomial of degree at most rankOfDiscrBdd N and all coefficients of absolute value at most coeffBoundOfDiscrBdd N. This is NumberField.hermiteTheorem.finite_of_discr_bdd recast to expose its explicit generating set.

theorem NumberField.ncard_setOf_finiteDimensional_abs_discr_le_le (A : Type u_1) [Field A] [CharZero A] (N : ℕ) : {K : { F : IntermediateField ℚ A // FiniteDimensional ℚ ↥F } | |discr ↥↑K| ≤ ↑N}.ncard ≤ (2 * coeffBoundOfDiscrBdd N + 1) ^ (hermiteTheorem.rankOfDiscrBdd N + 1) * hermiteTheorem.rankOfDiscrBdd N

Effective Hermite--Minkowski. Inside a fixed extension A / ℚ, the number of number fields K (finite extensions of ℚ) with |discr K| ≤ N is at most (2 * coeffBoundOfDiscrBdd N + 1) ^ (rankOfDiscrBdd N + 1) * rankOfDiscrBdd N, an explicit function of N alone. This upgrades Mathlib's NumberField.finite_of_discr_bdd from finiteness to an explicit count.

def NumberField.hermiteCountBound (D C : ℕ) : ℕ

The elementary polynomial count appearing in effective Hermite--Minkowski: if every field is generated by a root of an integer polynomial of degree at most D and coefficient height at most C, then the number of possible generated fields is bounded by (2 * C + 1) ^ (D + 1) * D.

@[simp]

theorem NumberField.hermiteCountBound_def (D C : ℕ) : hermiteCountBound D C = (2 * C + 1) ^ (D + 1) * D

theorem NumberField.hermiteCountBound_zero_left (C : ℕ) : hermiteCountBound 0 C = 0

theorem NumberField.hermiteCountBound_zero_right (D : ℕ) : hermiteCountBound D 0 = D

theorem NumberField.hermiteCountBound_mono {D₁ D₂ C₁ C₂ : ℕ} (hD : D₁ ≤ D₂) (hC : C₁ ≤ C₂) : hermiteCountBound D₁ C₁ ≤ hermiteCountBound D₂ C₂

The Hermite-count expression is monotone in the degree bound and the coefficient-height bound.

theorem NumberField.ncard_setOf_finiteDimensional_abs_discr_le_le_hermiteCountBound (A : Type u_1) [Field A] [CharZero A] (N : ℕ) : {K : { F : IntermediateField ℚ A // FiniteDimensional ℚ ↥F } | |discr ↥↑K| ≤ ↑N}.ncard ≤ hermiteCountBound (hermiteTheorem.rankOfDiscrBdd N) (coeffBoundOfDiscrBdd N)

The effective Hermite--Minkowski count with the exact constants packaged as hermiteCountBound.

theorem NumberField.ncard_setOf_finiteDimensional_abs_discr_le_le_of_bounds (A : Type u_1) [Field A] [CharZero A] (N D C : ℕ) (hD : hermiteTheorem.rankOfDiscrBdd N ≤ D) (hC : coeffBoundOfDiscrBdd N ≤ C) : {K : { F : IntermediateField ℚ A // FiniteDimensional ℚ ↥F } | |discr ↥↑K| ≤ ↑N}.ncard ≤ hermiteCountBound D C

Monotone effective Hermite--Minkowski. If D and C are any explicit bounds above Mathlib's degree bound rankOfDiscrBdd N and the coefficient bound coeffBoundOfDiscrBdd N, then the number of finite-dimensional subfields of an ambient extension A / ℚ with discriminant at most N is bounded by (2 * C + 1) ^ (D + 1) * D.

This is the usable form for later explicit estimates, where D and C are often replaced by simpler closed-form upper bounds.

theorem NumberField.ncard_setOf_finiteDimensional_abs_discr_le_le_of_threshold_le (A : Type u_1) [Field A] [CharZero A] {N M : ℕ} (hNM : N ≤ M) : {K : { F : IntermediateField ℚ A // FiniteDimensional ℚ ↥F } | |discr ↥↑K| ≤ ↑N}.ncard ≤ hermiteCountBound (hermiteTheorem.rankOfDiscrBdd M) (coeffBoundOfDiscrBdd M)

Threshold-monotone effective Hermite--Minkowski. If N ≤ M, then the number of finite-dimensional subfields of an ambient extension A / ℚ with absolute discriminant at most N is bounded by the explicit Hermite-count expression attached to the larger threshold M.

theorem NumberField.ncard_setOf_finiteDimensional_abs_discr_le_le_of_threshold_bounds (A : Type u_1) [Field A] [CharZero A] {N M D C : ℕ} (hNM : N ≤ M) (hD : hermiteTheorem.rankOfDiscrBdd M ≤ D) (hC : coeffBoundOfDiscrBdd M ≤ C) : {K : { F : IntermediateField ℚ A // FiniteDimensional ℚ ↥F } | |discr ↥↑K| ≤ ↑N}.ncard ≤ hermiteCountBound D C

Threshold-monotone effective Hermite--Minkowski with coarser constants. If N ≤ M, and D and C bound the degree and coefficient-height constants attached to M, then the number of finite-dimensional subfields of an ambient extension A / ℚ with absolute discriminant at most N is at most hermiteCountBound D C.

theorem NumberField.ncard_setOf_finiteDimensional_natAbs_discr_le_le_of_threshold_le (A : Type u_1) [Field A] [CharZero A] {N M : ℕ} (hNM : N ≤ M) : {K : { F : IntermediateField ℚ A // FiniteDimensional ℚ ↥F } | (discr ↥↑K).natAbs ≤ N}.ncard ≤ hermiteCountBound (hermiteTheorem.rankOfDiscrBdd M) (coeffBoundOfDiscrBdd M)

Threshold-monotone effective Hermite--Minkowski, natural-discriminant form. If N ≤ M, then the number of finite-dimensional subfields of an ambient extension A / ℚ whose discriminant has natural absolute value at most N is bounded by the explicit Hermite-count expression attached to the larger threshold M.

theorem NumberField.ncard_setOf_finiteDimensional_natAbs_discr_le_le_hermiteCountBound (A : Type u_1) [Field A] [CharZero A] (N : ℕ) : {K : { F : IntermediateField ℚ A // FiniteDimensional ℚ ↥F } | (discr ↥↑K).natAbs ≤ N}.ncard ≤ hermiteCountBound (hermiteTheorem.rankOfDiscrBdd N) (coeffBoundOfDiscrBdd N)

Effective Hermite--Minkowski, natural-discriminant form. Inside a fixed extension A / ℚ, the number of finite-dimensional subfields whose discriminant has natural absolute value at most N is bounded by the explicit Hermite-count expression attached to N.

theorem NumberField.ncard_setOf_finiteDimensional_natAbs_discr_le_le_of_threshold_bounds (A : Type u_1) [Field A] [CharZero A] {N M D C : ℕ} (hNM : N ≤ M) (hD : hermiteTheorem.rankOfDiscrBdd M ≤ D) (hC : coeffBoundOfDiscrBdd M ≤ C) : {K : { F : IntermediateField ℚ A // FiniteDimensional ℚ ↥F } | (discr ↥↑K).natAbs ≤ N}.ncard ≤ hermiteCountBound D C

Threshold-monotone effective Hermite--Minkowski with coarser constants, natural-discriminant form. If N ≤ M, and D and C bound the degree and coefficient-height constants attached to M, then the number of finite-dimensional subfields of an ambient extension A / ℚ whose discriminant has natural absolute value at most N is at most hermiteCountBound D C.

theorem NumberField.ncard_setOf_finiteDimensional_natAbs_discr_le_le_of_bounds (A : Type u_1) [Field A] [CharZero A] (N D C : ℕ) (hD : hermiteTheorem.rankOfDiscrBdd N ≤ D) (hC : coeffBoundOfDiscrBdd N ≤ C) : {K : { F : IntermediateField ℚ A // FiniteDimensional ℚ ↥F } | (discr ↥↑K).natAbs ≤ N}.ncard ≤ hermiteCountBound D C

Monotone effective Hermite--Minkowski, natural-discriminant form. If D and C bound the degree and coefficient-height constants attached to N, then the number of finite-dimensional subfields of an ambient extension A / ℚ whose discriminant has natural absolute value at most N is at most hermiteCountBound D C.