The Fundamental Theorem of Algebra Made Effective: An Elementary Real-algebraic Proof via Sturm Chains
From MaRDI portal
Publication:4923948
Zeros of polynomials, rational functions, and other analytic functions of one complex variable (e.g., zeros of functions with bounded Dirichlet integral) (30C15) Real polynomials: location of zeros (26C10) Numerical computation of roots of polynomial equations (65H04) Algorithms with automatic result verification (65G20) Mappings and functions (educational aspects) (97I20)
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.
Recommendations
- scientific article; zbMATH DE number 1336414
- Beweis eines Hauptsatzes in der Theorie der Algebren.
- scientific article; zbMATH DE number 4204493
- The fundamental theorem of algebra: an elementary and direct proof
- A direct proof and a transcendental version of the fundamental theorem of algebra via Cauchy's theorem
- Fundamental theorem of algebra constructively
- A proof of the fundamental theorem of algebra using Hurwitz's theorem
- scientific article; zbMATH DE number 1817227
- scientific article; zbMATH DE number 2038169
Cited in
(15)- The fundamental theorem of algebra in ACL2
- Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL
- Theorem of three circles in Coq
- Degree of rational mappings, and the theorems of Sturm and Tarski
- Algebraic winding numbers
- Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
- A note on the fundamental theorem of algebra
- A new general formula for the Cauchy index on an interval with subresultants
- How to count the number of zeros that a polynomial has on the unit circle?
- A note on \(p\)-adic simplicial volumes
- Local Bézout theorem for Henselian rings
- An algebraic certificate for Budan's theorem
- Quantitative fundamental theorem of algebra
- Algebraic certificates for Budan's theorem
- Deux moments dans l'histoire du Théorème d'algèbre de Ch. F. Sturm
This page was built for publication: The Fundamental Theorem of Algebra Made Effective: An Elementary Real-algebraic Proof via Sturm Chains
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4923948)
