Real-root intervals certify the sign of a real polynomial

Repeated use of [F1] and [F2] factors $H$ over $\mathbb{C}$ into linear factors with multiplicity. For a root $\zeta$ of multiplicity $m$, write $H=(x-\zeta {)}^{m}G$ with $G(\zeta )\mathrm{\ne }0$. Conjugating coefficients gives $H=(x-\bar{\zeta }{)}^m\bar{G}$ and $\bar{G}(\bar{\zeta })=\overline{G(\zeta )}\mathrm{\ne }0$, so the conjugate has exactly the same multiplicity. Thus, consistently with [F3], nonreal factors pair as $(x-(a+ib))(x-(a-ib))=(x-a{)}^2+b^2$, which is strictly positive for real $x$ when $b\mathrm{\ne }0$. The remaining factors are real linear factors $x-r$ for the real roots $r$.

On an open interval containing no real root, each real factor $x-r$ is either strictly positive throughout or strictly negative throughout by [F5]; every paired nonreal factor is positive throughout, and the real leading coefficient has fixed sign. Thus $H$ has one constant sign on that interval.

Each root value is zero, and the endpoints are checked separately. Step 2.1 shows each exact sample determines the sign on its entire root-free component, so the finite checks imply $H\ge 0$ on all of $[-1,1]$. If $H\ge 0$ everywhere, every sample and endpoint check plainly passes.