Evaluating Winding Numbers and Counting Complex Roots through Cauchy Indices in Isabelle/HOL

TL;DR

This paper formalizes the computation of winding numbers and root counting of complex polynomials using Cauchy indices within Isabelle/HOL, enabling automated reasoning about complex roots in specified domains.

Contribution

It introduces a formalization and a tactic in Isabelle/HOL for approximating winding numbers via Cauchy indices and counting roots using the argument principle and remainder sequences.

Findings

Successfully formalized winding number approximation in Isabelle/HOL

Developed a tactic for evaluating winding numbers through Cauchy indices

Enabled effective counting of polynomial roots in specific domains

Abstract

In complex analysis, the winding number measures the number of times a path (counter-clockwise) winds around a point, while the Cauchy index can approximate how the path winds. We formalise this approximation in the Isabelle theorem prover, and provide a tactic to evaluate winding numbers through Cauchy indices. By further combining this approximation with the argument principle, we are able to make use of remainder sequences to effectively count the number of complex roots of a polynomial within some domains, such as a rectangular box and a half-plane.