Counting polynomials of bounded degree and bounded coefficients

For a (semi)ring R and a finite set U of allowed coefficient values, the polynomials of degree at most d all of whose coefficients lie in U form a set of cardinality at most #U ^ (d + 1): a polynomial of degree ≤ d is determined by its d + 1 coefficients coeff 0, …, coeff d, each of which ranges over U.

Mathlib uses the finiteness of this set inline, as the engine of its bUnion_roots_finite (the set of roots of all polynomials of bounded degree with coefficients in a finite set is finite), where the same injection f ↦ (f.coeff i)ᵢ appears, but exposes neither that finiteness nor the explicit cardinality bound; this file supplies both.

The integer specialisation counts the polynomials of degree ≤ d whose coefficients are bounded in absolute value by B: there are at most (2 * B + 1) ^ (d + 1) of them. This is the elementary counting input named by the Layer-2 ("effective Hermite–Minkowski") target of the effective-bounds roadmap: Mathlib's NumberField.finite_of_discr_bdd already bounds the degree and coefficient height of a generating polynomial of a number field of bounded discriminant (natDegree_le_rankOfDiscrBdd, boundOfDiscBdd), so an explicit count of number fields of bounded discriminant needs an explicit count of the polynomials of bounded degree and height.

The cardinality bound counts a number but does not by itself record finiteness (Set.ncard is 0 on an infinite set), so each count is paired with the matching finiteness statement: these are what turn an injection of some family into one of these boxes into an explicit count of the family, the counting step the Layer-2 effective Hermite–Minkowski target needs. Mathlib proves this finiteness only inline, inside Polynomial.bUnion_roots_finite, rather than exposing it.

Main results

• TauCeti.Polynomial.ncard_natDegree_le_coeff_mem_le: at most #U ^ (d + 1) polynomials of degree ≤ d with every coefficient in a finite set U.
• TauCeti.Polynomial.finite_setOf_natDegree_le_coeff_mem: that family is finite.
• TauCeti.Polynomial.ncard_natDegree_le_abs_intCoeff_le: at most (2 * B + 1) ^ (d + 1) integer polynomials of degree ≤ d with every coefficient bounded by B in absolute value.
• TauCeti.Polynomial.finite_setOf_natDegree_le_abs_intCoeff_le: that family is finite.

theorem TauCeti.Polynomial.ncard_natDegree_le_coeff_mem_le {R : Type u_1} [Semiring R] (d : ℕ) (U : Finset R) : {f : Polynomial R | f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U}.ncard ≤ U.card ^ (d + 1)

The polynomials of degree at most d whose coefficients all lie in a finite set U number at most #U ^ (d + 1): such a polynomial is determined by the d + 1 coefficients coeff 0, …, coeff d, each ranging over U, so the coefficient map injects the set into the (d + 1)-fold product Fin (d + 1) → U.

theorem TauCeti.Polynomial.finite_setOf_natDegree_le_coeff_mem {R : Type u_1} [Semiring R] (d : ℕ) {U : Set R} (hU : U.Finite) : {f : Polynomial R | f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U}.Finite

The polynomials of degree at most d whose coefficients all lie in a finite set U form a finite set: the same coefficient map that gives the count above injects them into the finite product Fin (d + 1) → U. Finiteness needs no computable finset data, so U is an arbitrary finite Set. (Mathlib proves this only inline, inside Polynomial.bUnion_roots_finite.)

theorem TauCeti.Polynomial.ncard_natDegree_le_abs_intCoeff_le (d B : ℕ) : {f : Polynomial ℤ | f.natDegree ≤ d ∧ ∀ (i : ℕ), |f.coeff i| ≤ ↑B}.ncard ≤ (2 * B + 1) ^ (d + 1)

The integer polynomials of degree at most d all of whose coefficients are bounded by B in absolute value number at most (2 * B + 1) ^ (d + 1): each of the d + 1 coefficients coeff 0, …, coeff d ranges over the 2 * B + 1 integers in [-B, B].

theorem TauCeti.Polynomial.finite_setOf_natDegree_le_abs_intCoeff_le (d B : ℕ) : {f : Polynomial ℤ | f.natDegree ≤ d ∧ ∀ (i : ℕ), |f.coeff i| ≤ ↑B}.Finite

The integer polynomials of degree at most d all of whose coefficients are bounded by B in absolute value form a finite set: their coefficients range over the finite interval [-B, B].