LemmaStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-02

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Bounded roots give finitely many monic integer polynomials

Statement

For every integer $n \geq 1$ and every real $R \geq 1$ , the set of monic polynomials in $Z [X]$ of degree at most $n$ whose complex roots, counted with multiplicity, all have modulus at most $R$ is finite.

Facts & Assumptions

Given: An integer $n \geq 1$ and a real $R \geq 1$ .

[F1]

If $α_{1}, \dots, α_{m} \in C$ and $f (X) = \prod_{j = 1}^{m} (X - α_{j}) = X^{m} + c_{m - 1} X^{m - 1} + \dots + c_{0}$ , then expanding the product and comparing coefficients gives $c_{m - k} = (- 1)^{k} \sum_{∣ S ∣ = k} \prod_{j \in S} α_{j}$ for $1 \leq k \leq m$ , the sum being over the $k$ -element subsets $S \subseteq {1, \dots, m}$ . In particular $∣ c_{m - k} ∣ \leq (\binom{m}{k}) R^{k}$ whenever every $∣ α_{j} ∣ \leq R$ .

Proof

1.1F1given

Fix $m$ with $1 \leq m \leq n$ and let $f (X) = X^{m} + c_{m - 1} X^{m - 1} + \dots + c_{0} \in Z [X]$ be monic of degree $m$ with roots $α_{1}, \dots, α_{m} \in C$ , counted with multiplicity; by [F1] each coefficient is an integer satisfying $∣ c_{m - k} ∣ \leq (\binom{m}{k}) R^{k}$ when $∣ α_{j} ∣ \leq R$ for all $j$ .

1.2given

The degree-zero case contributes only the constant polynomial $1$ , which has no roots, so the root condition holds for it vacuously.

2.1step 1.1algebra

Thus every $c_{m - k}$ lies in the intersection $Z \cap [- (\binom{m}{k}) R^{k}, (\binom{m}{k}) R^{k}]$ , an integer interval whose endpoints depend only on $m$ , $k$ and $R$ , and such an interval contains at most $2 (\binom{m}{k}) R^{k} + 1$ integers, a finite number because $R \geq 1$ .

3.1step 2.1algebra

For each fixed $m$ the coefficient vector $(c_{0}, \dots, c_{m - 1})$ therefore ranges over a product of $m$ finite sets, which is finite, and the monic degree- $m$ polynomials inject into that product by their coefficient vector, so there are finitely many of them.

4.1step 3.1step 1.2algebra∎

The set in the statement is the union over the finitely many degrees $0 \leq m \leq n$ of the corresponding pieces, and a finite union of finite sets is finite, so the statement holds.

Used by

Finitely many roots of unity in a number field Lemma
The logarithmic unit image is discrete Lemma
Hermite-Minkowski finiteness Theorem
Kronecker root-of-unity criterion Theorem

Dependency tree · 0 levels

Nothing. This result depends on no other item in the library.

Sources

J. S. Milne, Algebraic Number Theory v3.08 (standard reference, not scraped)
William A. Stein, Algebraic Number Theory: A Computational Approach (standard reference, not scraped)