Finite-height polynomial root avoidance (source code)

= Finite-height polynomial root avoidance

Suppose $P(\xi',z)$ has degree $m$ in $z$ and a nonzero constant leading coefficient $a$. Among the $m+1$ heights $h_\ell=3\ell$, at least one satisfies
$$
|P(\xi',s+ih_\ell)|\geq|a|\qquad\text{for all }s\in\mathbb R
$$
at each real $\xi'$. Factor into $m$ linear factors with multiplicity. Each root's imaginary part can be within distance less than one of at most one candidate height. The <pigeonhole principle> leaves a height whose distance from every root is at least one, proving the product bound. The height can be chosen measurably: the set where a candidate succeeds is the closed intersection of $|P(\xi',q+ih_\ell)|\geq|a|$ over rational $q$, and selecting the first successful candidate gives a <Borel set> partition. This avoids any need for continuous global root labels.