Root and sign certificates for parameter-dependent polynomials

Let $p$ be a real polynomial in two formal indeterminates $X,T$, understood as a finite coefficient family. For real $x,a$, define $p(x,a)$ as the image of $p$ under the evaluation homomorphism ${\mathrm{ev}}_{x,a}:\mathbb{R}[X,T]\to \mathbb{R}$ that fixes real constants and sends $X$ to $x$ and $T$ to $a$. Let $A=[a_{-},a_{+}]$ and $I=[u,v]$ be nonempty closed bounded real intervals, with $u<v$.

A sign certificate for $p$ on $I\times A$ is a proof of a stated sign inequality for every $(x,a)\in I\times A$, or a proof of an enclosure $p(x,a)\in [L,U]$ for every such pair. An enclosure proves $p>0$ if $L>0$, and proves $p<0$ if $U<0$; non-strict endpoint inequalities give the corresponding non-strict signs.

A root certificate on $I$ over $A$ consists of proofs that, for every $a\in A$, the function $x\mapsto p(x,a)$ is continuous on $I$, its endpoint values have strictly opposite signs, and it is strictly monotone on $I$. Strict monotonicity means either $p(x,a)<p(y,a)$ for every $u\le x<y\le v$, or $p(x,a)>p(y,a)$ for every such pair; the direction may depend on $a$. To certify uniqueness on a larger specified real set $I\subseteq D\subseteq \mathbb{R}$, the certificate also contains a proof that $p(x,a)\mathrm{\ne }0$ for every $x\in D\setminus I$ and every $a\in A$.

For a cubic $b_3{x}^3+b_2{x}^2+b_{1}x+b_0$ with $b_3\mathrm{\ne }0$, its discriminant is $\mathrm{\Delta }=b_2^2{b}_1^2-4b_3{b}_1^3-4b_2^3{b}_0-27b_3^2{b}_0^2+18b_3{b}_2{b}_1{b}_0$. A discriminant-based certificate must state the applicable root-count theorem and verify its hypotheses separately in the cases $\mathrm{\Delta }<0$, $\mathrm{\Delta }=0$, and $\mathrm{\Delta }>0$ that occur in the parameter range, including parameter endpoints. This definition itself asserts no root count from the discriminant.

The polynomial ring R[xᵢ:i∈ I] as finitely supported coefficient families on monomials

Universal property of a polynomial ring on an arbitrary family of indeterminates

Intervals of ℝ: the nine order-convex forms, nondegeneracy, and length

Continuity of f : A → ℝ at a point of A and on A: the ε-δ condition, its agreement with lim_x → c f(x) = f(c) at a limit point, and continuity at an isolated point

The evaluation homomorphism exists uniquely by Universal property of a polynomial ring on an arbitrary family of indeterminates, applied with both coefficient and target ring equal to $\mathbb{R}$, the coefficient homomorphism the identity, and the two assigned values $x,a$. The closed intervals are those of Intervals of ℝ: the nine order-convex forms, nondegeneracy, and length, and continuity on $I$ means continuity at every point of $I$ as in Continuity of f : A → ℝ at a point of A and on A: the ε-δ condition, its agreement with lim_x → c f(x) = f(c) at a limit point, and continuity at an isolated point.

For each fixed $a\in A$, the continuity and opposite-sign conditions give a zero in $[u,v]$ by Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on [a,b] takes every value between f(a) and f(b). Strict monotonicity gives at most one zero there: two distinct zeros would have strictly ordered values. The additional exclusion gives uniqueness throughout $D$. A derivative-sign proof of strict monotonicity may use On an interval I, for f continuous on I and differentiable at every interior point: f' ≥ 0 throughout gives f nondecreasing, f' > 0 gives f increasing, f' ≤ 0 and f' < 0 give the two decreasing forms; conversely a nondecreasing f has f' ≥ 0 and a nonincreasing f has f' ≤ 0 wherever it is differentiable, and no strict converse is claimed only after checking continuity on the interval, differentiability at its interior points, and a strictly positive or strictly negative derivative throughout those points.

A finite outward-rounded interval calculation may establish an enclosure only under the domain and finite-result conditions of Finite real interval operations enclose their exact values; an inconclusive enclosure does not establish a sign. Multiplication of an inequality by a denominator requires a proof of its sign on the relevant domain: a positive denominator preserves the inequality, a negative one reverses it, by Sign rules for products and monotonicity of multiplication; equality is preserved by either multiplication, so the same rules apply to non-strict inequalities. Division requires the denominator to be nonzero. These certificates are proof obligations for the particular polynomial and parameter range; they do not themselves establish a sign or root count for any article polynomial.