The Fundamental Theorem of Algebra made effective: an elementary real-algebraic proof via Sturm chains

TL;DR

This paper presents an elementary, constructive, real-algebraic proof of the Fundamental Theorem of Algebra using Sturm chains and winding numbers, leading to an effective root-finding algorithm.

Contribution

It provides the first elementary, algebraic proof of Cauchy's theorem for polynomials over real closed fields, connecting geometric notions with algebraic methods.

Findings

Proof uses only intermediate value theorem and polynomial arithmetic.

The approach is constructive and translates directly into an algebraic root-finding algorithm.

The proof is formalizable in the first-order language of real closed fields.

Abstract

Sturm's theorem (1829/35) provides an elegant algorithm to count and locate the real roots of any real polynomial. In his residue calculus (1831/37) Cauchy extended Sturm's method to count and locate the complex roots of any complex polynomial. For holomorphic functions Cauchy's index is based on contour integration, but in the special case of polynomials it can effectively be calculated via Sturm chains using euclidean division as in the real case. In this way we provide an algebraic proof of Cauchy's theorem for polynomials over any real closed field. As our main tool, we formalize Gauss' geometric notion of winding number (1799) in the real-algebraic setting, from which we derive a real-algebraic proof of the Fundamental Theorem of Algebra. The proof is elementary inasmuch as it uses only the intermediate value theorem and arithmetic of real polynomials. It can thus be formulated in the first-order language of real closed fields. Moreover, the proof is constructive and immediately translates to an algebraic root-finding algorithm.