Sturm's Theorem

Sturm's Theorem uses a sequence of polynomials built from a given univariate polynomial and its derivative by a variant of Euclid's algorithm, called the Sturm sequence, to express the number of distinct real roots of the polynomial in an interval as the number of sign changes of the Sturm sequence's values at the interval's endpoints. Applied to the entire real line, it gives the total count of the polynomial's distinct real roots, and by subdividing intervals it isolates each root into an arbitrarily small interval, yielding the oldest real-root isolation algorithm. Named after Jacques Charles Francois Sturm, who discovered it in 1829, the theorem remains fundamental to the theoretical study of decidability and quantifier elimination for the real numbers, even though other methods, such as Descartes' Rule of Signs, are more efficient for ordinary computation.