math.NT — Number Theory

Every algebraic number is a critical value of an integer polynomial

Contributed by RJ Acuna

We arrived at an independent proof of Petrov's theorem. For every irreducible $f \in \mathbb{Z}[x]$ of positive degree there are $g \in \mathbb{Z}[x]$ and an irreducible $F \in \mathbb{Z}[x]$ of positive degree with $F \mid g'$ and $F^{2} \mid f \circ g$. Equivalently, every algebraic number is a critical value of an integer polynomial, so the set of critical values of $\mathbb{Z}[x]$ is exactly $\overline{\mathbb{Q}}$. The construction is explicit. We classify $g \in \mathbb{Z}[x]$ with critical value $\alpha$, and find a lower bound for $\deg g$. The proof was assisted by AI, and has been formalized in Lean.