Archimedean degree bound beyond the cubic case

Fix the polynomial ring $\mathbb{Q}[X]$ over the rationals.

The statement asserts the following. Let $m \in \mathbb{Q}[X]$ be a polynomial that is irreducible in $\mathbb{Q}[X]$ (in the ring-theoretic sense: $m$ is neither a unit nor zero, and whenever $m = ab$ one of $a, b$ is a unit). Let $\alpha_1 \in \mathbb{R}$ be a real number satisfying $m(\alpha_1) = 0$, where $m$ is evaluated at $\alpha_1$ via the canonical embedding $\mathbb{Q} \hookrightarrow \mathbb{R}$ applied to its coefficients. Let $\alpha_2 \in \mathbb{C}$ be a complex number satisfying $m(\alpha_2) = 0$, evaluated via $\mathbb{Q} \hookrightarrow \mathbb{C}$. Write $\operatorname{Re}\alpha_2$ and $\operatorname{Im}\alpha_2$ for the real and imaginary parts of $\alpha_2$. Assume the sign condition

i.e. the product of the two real numbers $\operatorname{Re}\alpha_2 - \alpha_1$ and $\operatorname{Im}\alpha_2$ is strictly positive. Let $\alpha \in \mathbb{C}$ be a further complex number with $m(\alpha) = 0$; note that $\alpha$ is a third, independent variable, tied to $\alpha_1$ and $\alpha_2$ only by being a root of the same $m$, and nothing forces $\alpha$ to differ from, or agree with, either of them. Let $f \in \mathbb{Q}[X]$ be a polynomial which is split over $\mathbb{Q}$ in the following expanded sense (this is the bundle's own predicate, unfolded):

• $\deg f > 0$, where $\deg$ is the natural-number degree (so in particular $f \ne 0$ and $f$ is not a nonzero constant); and
• there exist a rational number $a \ne 0$ and a finite multiset $R$ of rational numbers such that

the product being taken over $R$ with multiplicity. (Since $\deg f > 0$, the multiset $R$ is necessarily nonempty and $|R| = \deg f$; roots may repeat.)

Finally, let $c \in \mathbb{Q}$ be a rational number such that evaluating $f$ at the complex number $\alpha$ gives exactly the image of $c$ in $\mathbb{C}$:

Under all of these hypotheses, the conclusion asserted is the inequality

a comparison of real numbers, where $\deg f$ is the natural-number degree of $f$ cast into $\mathbb{R}$, $\pi$ is the usual circle constant, and $\arctan$ is the principal inverse tangent, taking values in $(-\pi/2, \pi/2)$. The inequality is non-strict ($\le$), and it is stated in the direction "the ratio is at most the degree".

On degeneracy, satisfiability, and junk values.

The hypotheses are jointly satisfiable, so the statement is not vacuous. The sign hypothesis $0 < (\operatorname{Re}\alpha_2 - \alpha_1)\operatorname{Im}\alpha_2$ forces both factors to be nonzero and of the same sign; in particular $\operatorname{Im}\alpha_2 \ne 0$, so $\alpha_2$ is genuinely non-real, and $\operatorname{Re}\alpha_2 \ne \alpha_1$. Consequently $m$ has a real root $\alpha_1$ and a non-real root $\alpha_2$; together with irreducibility over $\mathbb{Q}$ this forces $\deg m \ge 3$ (an irreducible rational polynomial of degree $1$ has only a real root, and one of degree $2$ has either two real roots or two non-real ones, never one of each). So $m$ cannot be linear or quadratic, and the hypothesis block is consistent — for instance any irreducible rational cubic with one real and two complex roots, with $\alpha_2$ chosen as whichever of the conjugate pair makes the product positive, satisfies the first four hypotheses.

Because $\operatorname{Im}\alpha_2 \ne 0$ is forced, the quotient $(\operatorname{Re}\alpha_2 - \alpha_1)/\operatorname{Im}\alpha_2$ is an honest division and no division-by-zero junk value arises there; moreover that quotient is strictly positive (the two factors having equal sign), so $\arctan$ of it lies strictly in $(0, \pi/2)$ and is in particular nonzero. Hence the outer division $\pi / \arctan(\cdot)$ is also an honest division: the denominator cannot be $0$, and the left-hand side is a well-defined real number strictly greater than $\pi/(\pi/2) = 2$. Note that the sign hypothesis constrains only $\alpha_1$ and $\alpha_2$ and does not involve $\alpha$ or $f$.

There is, however, no hypothesis relating $\alpha$ to $\alpha_1$ or $\alpha_2$ beyond all three being roots of $m$, and no hypothesis asserting that $\alpha_1$, $\alpha_2$, $\alpha$ are distinct, that $\alpha_2$ and $\alpha_1$ are "adjacent" in any sense, or that $f$ is nonconstant on any set other than as recorded by $\deg f > 0$. Likewise, $\alpha_1$ is a real number required to be a root, and $\alpha_2$, $\alpha$ are complex numbers required to be roots; no hypothesis says $m$ is monic, primitive, or of any particular degree beyond what irreducibility plus the two root conditions force. The condition $f(\alpha) = c$ says only that $f$ takes a rational value at the specific root $\alpha$; it is not required to take rational values at the other roots, and $c$ is not required to be nonzero.

Finally, $\deg f$ appears on the right as a natural number coerced to $\mathbb{R}$; the split hypothesis guarantees $\deg f \ge 1$, so the right-hand side is at least $1$, but the conclusion asserts the specific numerical bound above, not merely positivity.