Counting the roots of all polynomials of bounded degree and bounded coefficients

For a ring hom m : R →+* S into a domain S and a finite set U of allowed coefficient values, the set of all roots in S of the polynomials of degree at most d with every coefficient in U,

⋃ (f) (_ : f.natDegree ≤ d ∧ ∀ i, f.coeff i ∈ U), (f.map m).roots.toFinset,

has cardinality at most #U ^ (d + 1) · d: there are at most #U ^ (d + 1) such polynomials (TauCeti.Polynomial.ncard_natDegree_le_coeff_mem_le), and each contributes at most d roots (a degree-≤ d polynomial has at most d roots in a domain).

This is precisely the explicit count of the generating set in Mathlib's proof of Hermite's finiteness theorem. There, NumberField.finite_of_discr_bdd shows the number fields of bounded discriminant inside a fixed extension are finite by realising each as ℚ(x) for x a root of an integer polynomial of explicitly bounded degree and coefficient height, then invoking the finiteness of this very union of root sets, Polynomial.bUnion_roots_finite. Mathlib exposes only that finiteness; the effective Hermite–Minkowski target of the effective-bounds roadmap needs the matching explicit cardinality, so that an injection of the fields into this generating set turns into an explicit count of the fields. This file supplies that cardinality, upgrading Polynomial.bUnion_roots_finite exactly as TauCeti.Polynomial.ncard_natDegree_le_coeff_mem_le upgrades the polynomial finiteness it is built on.

Main results

• TauCeti.Polynomial.ncard_biUnion_roots_natDegree_le_coeff_mem_le: at most #U ^ (d + 1) · d roots in S among all degree-≤ d polynomials with every coefficient in a finite set U.
• TauCeti.Polynomial.ncard_biUnion_roots_natDegree_le_abs_intCoeff_le: the integer specialisation, (2 · B + 1) ^ (d + 1) · d roots among all degree-≤ d integer polynomials with every coefficient bounded by B in absolute value. This is the form named by the Layer-2 ("effective Hermite–Minkowski") target.

theorem TauCeti.Polynomial.ncard_biUnion_roots_natDegree_le_coeff_mem_le {R : Type u_1} {S : Type u_2} [Semiring R] [CommRing S] [IsDomain S] [DecidableEq S] (m : R →+* S) (d : ℕ) (U : Finset R) : (⋃ (f : Polynomial R), ⋃ (_ : f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U), ↑(Polynomial.map m f).roots.toFinset).ncard ≤ U.card ^ (d + 1) * d

The roots in a domain S of all polynomials of degree at most d with every coefficient in a finite set U, mapped along a ring hom m : R →+* S, number at most #U ^ (d + 1) · d: there are at most #U ^ (d + 1) such polynomials, and each, having degree at most d, has at most d roots in S. This is the explicit cardinality of the set whose finiteness is Polynomial.bUnion_roots_finite.

theorem TauCeti.Polynomial.ncard_biUnion_roots_natDegree_le_abs_intCoeff_le {S : Type u_2} [CommRing S] [IsDomain S] [DecidableEq S] (m : ℤ →+* S) (d B : ℕ) : (⋃ (f : Polynomial ℤ), ⋃ (_ : f.natDegree ≤ d ∧ ∀ (i : ℕ), |f.coeff i| ≤ ↑B), ↑(Polynomial.map m f).roots.toFinset).ncard ≤ (2 * B + 1) ^ (d + 1) * d

The integer specialisation: the roots in a domain S of all integer polynomials of degree at most d with every coefficient bounded by B in absolute value number at most (2 · B + 1) ^ (d + 1) · d. Each of the 2 · B + 1 integers in [-B, B] is an allowed coefficient, and a degree-≤ d polynomial has at most d roots. This is the counting input named by the Layer-2 effective Hermite–Minkowski target.