Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL
 72 Downloads
Abstract
In complex analysis, the winding number measures the number of times a path (counterclockwise) 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 halfplane.
Keywords
Interactive theorem proving Isabelle/HOL Computer algebra Cauchy index Winding number Root counting The Routh–Hurwitz stability criterion1 Introduction
However, when formally evaluating the winding number in proof assistants such as Isabelle/HOL and HOL Light, unexpected difficulties arise, as pointed out by Harrison [8] and Li et al. [14]. To address this problem, we formalise a theory of the Cauchy index on the complex plane, thereby approximating how the path winds. When the path is a cycle and comprises line segments and parts of circles, we can now evaluate the winding number by calculating Cauchy indices along those subpaths.
In addition, by further combining our previous formalisation of the argument principle [14] (which associates the winding number with the number of complex roots), we build effective procedures to count the complex roots of a polynomial within some domains, such as a rectangle box and a halfplane.

a novel tactic to enable users to evaluate the winding number through Cauchy indices,

and novel verified procedures to count complex roots of a polynomial.
Formulations in this paper, such as the definition of the Cauchy index and statements of some key lemmas, mainly follow Rahman and Schmeisser’s book [19, Chapter 11] and Eisermann’s paper [6]. Nevertheless, we were still obliged to devise some proofs on our own, as discussed later.
This paper continues as follows: we start with a motivating example (Sect. 2) to explain the difficulty of formal evaluation of the winding number in Isabelle/HOL. We then present an intuitive description of the link between the winding number and the Cauchy indices (Sect. 3), which is then developed formally (Sect. 4). Next, we present verified procedures that count the number of complex roots in a domain (Sect. 5), along with some limitations (Sect. 6) and make some general remarks on the formalisation (Sect. 7). Finally, we discuss related work (Sect. 8) and present conclusions (Sect. 9).
2 A Motivating Example
Example 1
Lemma 1
where Open image in new window encodes the winding number of \(\gamma _1\) around z: \(n(\gamma _1,z)\), and Open image in new window encodes the homotopic proposition between two paths. Putting (8) and (9) together yields \(n(L_r+C_r,i) = 1\), which concludes the whole proof.
Example 2
Lemma 2

Open image in new window assumes that \(\gamma \) is piecewise continuously differentiable on [0, 1],

Open image in new window asserts that z is not on the path \(\gamma \),

the assumption Open image in new window asserts that the ray starting at \(z \in {\mathbb {C}}\) and through \(w \in {\mathbb {C}}\) (\(\{z + a (wz) \mid a>0 \}\)) does not intersect with \(\gamma \)—for all \(a>0\), \(z + a (wz)\) does not lie on \(\gamma \).
As can be observed in Examples 1 and 2, our proofs of \(n(L_r+C_r,i) = 1\) and \(n(L_r+C_r,i) = 0\) were ad hoc, and involved the manual construction of auxiliary paths or rays (e.g., \(C'_R\) and \(L'_R\)). Similar difficulties have also been mentioned by John Harrison when formalising the prime number theorem [8]. In the next section, we will introduce an idea to systematically evaluate winding numbers.
3 The Intuition
Definition 1
Definition 2
Definition 3
Proposition 1
A formal proof of Proposition 1 will be introduced in Sect. 4.1. Here, given the statement of the proposition, we can have alternative proofs for \(n(L_r+C_r,i) = 1\) and \(n(L_r+C_r,i) = 0\).
Example 3
Example 4
Compared to the previous proofs presented in Examples 1 and 2, the alternative proofs in Examples 3 and 4 are systematic and less demanding to devise once we have a formalisation of Proposition 1, which is what we will introduce in the next section.
4 Evaluating Winding Numbers
The previous section presented an informal intuition to systematically evaluate winding numbers; in this section, we will report the formal development of this intuition. We will first present a mechanised proof of Proposition 1 (Sect. 4.1), which includes mechanised definitions of jumps and Cauchy indices (i.e., Definition 1, 2 and 3) and several related properties of these objects. After that, we build a tactic in Isabelle/HOL that is used to mechanise proofs presented in Example 3 and 4 (Sect. 4.2). Finally, we discuss some subtleties we encountered during the formalisation (Sect. 4.3).
4.1 A Formal Proof of Proposition 1
respectively. Here, Open image in new window , Open image in new window , Open image in new window , and Open image in new window are all filters, where a filter is a predicate on predicates that satisfies certain properties. Filters are extensively used in the analysis library of Isabelle to encode varieties of logical quantification: for example, Open image in new window encodes the statement “for a variable that is sufficiently close to x from the left", and Open image in new window represents “for a sufficiently large variable". Furthermore, Open image in new window encoded the proposition
As can be expected, the finiteness of jumps over a path can be derived by the finiteness of segments:
Lemma 3
where Open image in new window asserts that \(\gamma \) is a continuous function on [0..1] (so that it is a path). Roughly speaking, Lemma 3 claims that a path will have a finite number of jumps if it can be divided into a finite number of segments.
By assuming such a finite number of segments we have welldefined Open image in new window , and can then derive some useful related properties:
Lemma 4
More importantly, we now have an induction rule for a path with a finite number of segments:
Lemma 5

Open image in new window is the base case that Open image in new window holds for a constant path;

Open image in new window is the inductive case when the last segment is right on the line \(\{x \mid {\text {Re}}(x) = {\text {Re}}(z) \}\): \(\forall t \in (s,1).\, {\text {Re}}(g(t)) = {\text {Re}}(z)\);

Open image in new window is the inductive case when the last segment does not cross the line \(\{x \mid {\text {Re}}(x) = {\text {Re}}(z) \}\): \(\forall t \in (s,1).\, {\text {Re}}(g(t)) \ne {\text {Re}}(z)\).
Before attacking Proposition 1, we can show an auxiliary lemma about \({\text {Re}}(n(\gamma ,z_0))\) and \({\text {Indp}}(\gamma ,z_0)\) when the end points of \(\gamma \) are on the line \(\{z \mid {\text {Re}}(z) = {\text {Re}}(z_0) \}\):
Lemma 6
Here, Lemma 6 is almost equivalent to Proposition 1 except for that more restrictions haven been placed on the end points of \(\gamma \).
Proof of Lemma 6
As there are a finite number of segments along \(\gamma \) (i.e., Open image in new window ), by inducting on these segments with Lemma 5 we end up with three cases. The base case is straightforward: given a constant path \(g : [0,1] \rightarrow {\mathbb {C}}\) and a complex point \(z \in {\mathbb {C}}\), we have \({\text {Re}}(n(g,z)) = 0\) and \({\text {Indp}}(g,z) = 0\), hence \(2 {\text {Re}}(n(g,z)) =  {\text {Indp}}(g,z)\).
Finally, we are ready to formally derive Proposition 1 in Isabelle/HOL:
Theorem 1
Proof
By assumption, we know that \(\gamma \) is a loop, and the point \(\gamma (0) = \gamma (1)\) can be away from the line \(\{z \mid {\text {Re}}(z) = {\text {Re}}(z_0) \}\) which makes Lemma 6 inapplicable. To resolve this problem, we look for a point \(\gamma (s)\) on \(\gamma \) such that \(0 \le s \le 1\) and \({\text {Re}}(\gamma (s)) = {\text {Re}}(z_0)\), and we can either fail or succeed.
4.2 A Tactic for Evaluating Winding Numbers
Lemma 7
to eliminate the path join operations ( Open image in new window ) until the predicate Open image in new window is only applied to a linear path or a part of a circular path, and either of these two cases can be directly discharged because these two kinds of paths are proved to be divisible into a finite number of segments by the imaginary axis:
Lemma 8
Lemma 9
Lemma 10
to convert the subgoal (30) to (23) and (25).
After building the tactic Open image in new window , we are now able to convert a goal like Eq. (22) to (23), (24) and (25). In most cases, discharging (23) and (24) is straightforward. To derive (25), we will need to formally evaluate each \({\text {Indp}}(\gamma _j,z_0)\) (\(1 \le j \le n\)) when \(\gamma _j\) is either a linear path or a part of a circular path.
When \(\gamma _j\) is a linear path, the following lemma grants us a way to evaluate \({\text {Indp}}(\gamma _j,z_0)\) through its righthand side:
Lemma 11
When \(\gamma _j\) is a part of a circular path, a similar lemma has been provided to facilitate the evaluation of \({\text {Indp}}(\gamma _j,z_0)\).
4.3 Subtleties
The first subtlety we have encountered during the formalisation of Proposition 1 is about the definitions of jumps and Cauchy indices, for which our first attempt followed the standard definitions in textbooks [2, 16, 19].
Definition 4
Definition 5

The function \(\lambda t.\, {\text {Re}}(\gamma (t)  z_0)\) cannot vanish at either end of the interval. That is, we need to additionally assume \({\text {Re}}(\gamma (0)  z_0) \ne 0\) as in Rahman and Schmeisser’s formulation [19, Lemma 11.1.1 and Theorem 11.1.3], and Proposition 1 will be inapplicable in the case of Fig. 6c where \({\text {Re}}(\gamma (0)) = {\text {Re}}(\gamma (1)) = {\text {Re}}(z_0)\).
 The function \(\lambda t.\, {{\text {Im}}(\gamma (t)  z_0)}/{{\text {Re}}(\gamma (t)  z_0)}\) has to be rational, which makes Proposition 1 inapplicable for cases like in Fig. 6d (if we follow Definition 5). To elaborate, it can be observed in Fig. 6d that \(n(\gamma ,z_0) = 1\), while we will only get a wrong answer by following Definition 5 and evaluating via Proposition 1:where \(f(t) = {{\text {Im}}(\gamma (t)  z_0)}/{{\text {Re}}(\gamma (t)  z_0)}\). In comparison, Definition 2 leads to the correct answer:$$\begin{aligned}  \frac{1}{2} \left( \sum _{x \in (0,1)} \mathrm {jump}(f,x) \right) =  \frac{\mathrm {jump}(f,t_2)}{2} =  \frac{1}{2}, \end{aligned}$$$$\begin{aligned} \begin{aligned} n(\gamma ,z_0)&=  \frac{1}{2} \left( \sum _{x \in [0,1)} \mathrm {jump}_+(f,x)  \sum _{x \in (0,1]} \mathrm {jump}_(f,x) \right) \\&=  \frac{1}{2} \left( \mathrm {jump}_+(f,t_2) + \mathrm {jump}_+(f,t_1)  \mathrm {jump}_(f,t_2)  \mathrm {jump}_(f,t_0) \right) \\&=  \frac{1}{2} \left( \frac{1}{2} + \frac{1}{2}  ( \frac{1}{2})  ( \frac{1}{2}) \right) \\&=  1. \end{aligned} \end{aligned}$$
5 Counting the Number of Complex Roots
The previous section described a way to evaluate winding numbers via Cauchy indices. In this section, we will further explore this idea and propose verified procedures to count the number of complex roots of a polynomial in some domain such as a rectangle and a halfplane.
5.1 Roots in a Rectangle

\(p'\) is the first derivative of p,
 the Tarski query \(\mathrm {TaQ}(q,p,a,b)\) defined as follows:$$\begin{aligned} \mathrm {TaQ}(q,p,a,b) = \sum _{x \in (a,b), p(x) = 0} \mathrm {sgn}(q(x)), \end{aligned}$$

\(\mathrm {SRemS}(p,q)\) is the signed remainder sequence started with p and q.
 Let \([p_1,p_2,\ldots ,p_n]\) be a sequence of polynomials, \(\mathrm {Var}([p_1,p_2,\ldots ,p_n];a,b)\) is the difference in the number of sign variations when evaluating \([p_1,p_2,\ldots ,p_n]\) at a and b:$$\begin{aligned}&\mathrm {Var}([p_1,p_2,\ldots ,p_n];a,b) \nonumber \\&= \mathrm {Var}([p_1(a),p_2(a),\ldots ,p_n(a)])  \mathrm {Var}([p_1(b),p_2(b),\ldots ,p_n(b)]). \end{aligned}$$(36)
While proceeding to the formal development, the first problem we encountered was that the Cauchy index in Eq. (37) actually follows the classic definition (i.e., Definition 5), and is different from the one in Eq. (34) (i.e., Definitions 2 and 3). Subtle differences between these two formulations have already been discussed in Sect. 4.3. Luckily, Eisermann [6] has also described an alternative sign variation operator so that our current definition of the Cauchy index (i.e., Definition 2) can be computationally evaluated:
Lemma 12
The next step is to make the definition Open image in new window executable. This is achieved by proving a code equation, where the lefthand side of the equation is the target definition and the righthand side is an executable expression. In the case of Open image in new window , the code equation is the following lemma:
Lemma 13
where Open image in new window is the polynomial composition operation and Open image in new window and Open image in new window , respectively, extract the real and imaginary parts of the complex polynomial Open image in new window .
Proof of Lemma 13
Lemma 14
Example 5
5.2 Roots in a Halfplane
Lemma 15
Next, for \(\lim _{r \rightarrow +\infty } {\text {Re}}(n(C_p(r), 0))\), we first derive a lemma about \(C_r\):
Lemma 16
that is, \(\lim _{r \rightarrow +\infty } {\text {Re}}(n(C_r, 0)) = 1/2\), following which and by induction we have
Lemma 17
Putting Eqs. (40) and (41) together yields the core lemma about Open image in new window in this section:
Lemma 18
Lemma 19

Open image in new window divides the polynomial Open image in new window by its leading coefficient so that the resulting polynomial Open image in new window is monic. This corresponds to the assumption Open image in new window in Lemma 18.

Open image in new window checks if Open image in new window has no root lying on the real axis, which is due to the second assumption in Lemma 18.
 Open image in new window evaluatesby following Eq. (37).$$\begin{aligned} {\text {Ind}}_{\infty }^{+\infty } \left( \lambda t.\, \frac{{\text {Im}}(p_I(t))}{{\text {Re}}(p_R(t))} \right) \end{aligned}$$
Lemma 20
And so we can naturally evaluate Open image in new window through Open image in new window :
Lemma 21
Example 6
Despite our naive implementation, both Open image in new window and Open image in new window are applicable for small or medium examples. For most polynomials with coefficient bitsize up to 10 and degree up to 30, our complex root counting procedures terminate within minutes.
6 Limitations and Future Work
There are, of course, several improvements that can be made on both the evaluation tactic of Sect. 4.2 and the root counting procedures of Sect. 5. As the tactic is intended to be applied to winding numbers with variables, full automation with this tactic is unlikely in most cases, but we can always aim for better automation and an enhanced interactive experience for users (e.g., presenting unsolved goals in a more userfriendly way).
 To generalise the definition of winding numbers. The current formulation of winding numbers in Isabelle/HOL follows the one in complex analysis:which becomes undefined when the point z is on the image of the path \(\gamma \). With more general formulations of winding numbers, such as the algebraic version by Eisermann [6], we may be able to derive a stronger version of the argument principle that allows zeros on the border.$$\begin{aligned} n(\gamma ,z) = \frac{1}{2 \pi i} \oint _\gamma \frac{d w}{w  z} \end{aligned}$$

To deploy a more sophisticated strategy to count the number of times that the path winds. Recall that the underlying idea in this paper is to reduce the evaluation of winding numbers to classifications of how paths cross some line. The Cauchy index merely provides one classification strategy, which we considered simple and elegant enough for formalisation. In contrast, Collins and Krandick [4] propose a much more sophisticated strategy for such classifications. Their strategy has, in fact, been widely implemented in modern systems, such as Mathematica and SymPy, to count the number of complex roots.
7 Potential Applications

Rahman and Schmeisser formulated the Cauchy index as in Definitions 4 and 5, and we used their formulation in our first attempt. However, after we realised the subtleties discussed in Sect. 4.3, we abandoned this formulation and switched to Eisermann’s (i.e., Definition 2). As a result, the root counting procedures presented in this paper are more general than the ones in their book, having fewer preconditions.

Eisermann formulated a winding number \(n(\gamma ,z_0)\) in a realalgebraical sense where \(\gamma \) is required to be a piecewise polynomial path (i.e., each piece from the path needs to be a polynomial). In comparison, \(n(\gamma ,z_0)\) in Isabelle/HOL follows the classic definition in complex analysis, and places fewer restrictions on the shape of \(\gamma \) (i.e., piecewise continuously differentiable is less restrictive than being a piecewise polynomial) but does not permit \(z_0\) to be on the image of \(\gamma \) (while Eisermann’s formulation does). Consequently, Eisermann’s root counting procedure works in more restrictive domains (i.e., he only described the rectangle case in his paper) but does not prevent roots on the border.

Our root counting procedure is based on remainder sequences, which are generally considered much slower than those built upon Descartes’ rule of signs.

Modern isolation procedures are routinely required to deliver isolation boxes whose sizes meet some userspecified limit, hence they usually keep refining the isolation boxes even after the roots have been successfully isolated. The bisection strategy still works in the root refinement stage, but dedicated numerical approaches such as Newton’s iteration are commonly implemented for efficiency reasons.

Modern isolation procedures sometimes prefer a bitstream model in which the coefficients of the polynomial are approximated as a bit stream. This approach is particularly beneficial when the coefficients have extremely large bitwidth or consist of algebraic numbers.

Modern implementations usually incorporate numerous lowlevel optimisations, such as hash tables, which are hard to implement as verified procedures in a theorem prover.
8 Related Work
Formalisations of the winding number (from an analytical perspective) are available in Coq [3], HOL Light [7] and Isabelle/HOL. To the best of our knowledge, our tactic of evaluating winding numbers through Cauchy indices is novel. As both HOL Light and Isabelle/HOL have a relatively comprehensive library of complex analysis (i.e., at least including Cauchy’s integral theorem), our evaluation tactic could be useful when deriving analytical proofs in these two proof assistants.
The ability to count the real roots of a polynomial only requires Sturm’s theorem, so this capability is widely available among major proof assistants including PVS [18], Coq [15], HOL Light [17] and Isabelle [5, 10, 13]. However, as far as we know, our procedures to count complex roots are novel, as they require a formalisation of the argument principle [14], which is only available in Isabelle at the time of writing.
9 Conclusion
We have further related Cauchy indices to the argument principle and developed novel verified procedures to count the complex roots of a polynomial within the areas of rectangles and halfplanes. Despite the limitations of not allowing roots on the border (which we will solve in future work), the ability to formally count complex roots is believed to lay the foundations for conducting stability analysis (e.g., the Routh–Hurwitz stability criterion) in the framework of the Isabelle theorem prover.
Footnotes
 1.
Applying an introduction rule will replace a goal by a set of subgoals derived from the premises of the rule, provided the goal can be unified with the conclusion of the rule.
Notes
Acknowledgements
We thank Dr. Angeliki KoutsoukouArgyraki and Anthony Bordg for commenting on the early version of this draft. The work was supported by the ERC Advanced Grant ALEXANDRIA (Project 742178), funded by the European Research Council.
References
 1.Arnold, V.I.: Ordinary Differential Equations. Springer, Berlin (1992)Google Scholar
 2.Basu, S., Pollack, R., Roy, M.F.: Algorithms in Real Algebraic Geometry. Springer, Berlin (2006)zbMATHGoogle Scholar
 3.Brunel, A.: Nonconstructive complex analysis in Coq. In: Danielsson, N.A., Nordström, B. (eds.) 18th International Workshop on Types for Proofs and Programs (TYPES 2011), pp. 1–15. Schloss DagstuhlLeibnizZentrum fuer Informatik, Dagstuhl, Germany (2013)Google Scholar
 4.Collins, G.E., Krandick, W.: An efficient algorithm for infallible polynomial complex root isolation. In: Proceedings of International Symposium on Symbolic and Algebraic Computation, ISSAC ’92, pp. 189–194. ACM (1992)Google Scholar
 5.Eberl, M.: A decision procedure for univariate real polynomials in Isabelle/HOL. In: Conference on Certified Programs and Proofs, pp. 75–83. ACM Press (2015)Google Scholar
 6.Eisermann, M.: The fundamental theorem of algebra made effective: an elementary realalgebraic proof via Sturm chains. Am. Math. Mon. 119(9), 715 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
 7.Harrison, J.: Formalizing basic complex analysis. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar and Rhetoric, vol. 10, no. 23, pp. 151–165. University of Białystok (2007). http://mizar.org/trybulec65/. Accessed 2 Apr 2019
 8.Harrison, J.: Formalizing an analytic proof of the prime number theorem (Dedicated to Mike Gordon on the occasion of his 60th birthday). J. Autom. Reason. 43, 243–261 (2009)CrossRefGoogle Scholar
 9.Hölzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle/HOL. In: Volume 7998, pp. 279–294 (2013). https://doi.org/10.1007/9783642396342_21
 10.Li, W.: The Sturm–Tarski theorem. In: Archive of Formal Proofs (2014). http://isaafp.org/entries/Sturm_Tarski.html. Accessed 2 Apr 2019
 11.Li, W.: Count the number of complex roots. In: Archive of Formal Proofs (2017). http://isaafp.org/entries/Count_Complex_Roots.html. Accessed 2 Apr 2019
 12.Li, W.: Evaluate winding numbers through cauchy indices. In: Archive of Formal Proofs (2017). http://isaafp.org/entries/Winding_Number_Eval.html. Accessed 2 Apr 2019
 13.Li, W., Passmore, G.O., Paulson, L.C.: Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL. J Autom Reason 62, 69–91 (2017). https://doi.org/10.1007/s1081701794246 MathSciNetCrossRefzbMATHGoogle Scholar
 14.Li, W., Paulson, L.C.: A formal proof of Cauchy’s residue theorem. In: Blanchette, J.C., Merz, S., (eds.) 7th International Conference on Interactive Theorem Proving, pp. 235–251. Springer (2016)Google Scholar
 15.Mahboubi, A., Cohen, C.: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Log. Methods Comput. Sci. 8(1), 1–40 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
 16.Marden, M.: Geometry of Polynomials, 2nd edn. American Mathematical Society, Providence (1949)CrossRefzbMATHGoogle Scholar
 17.McLaughlin, S., Harrison, J.: A proofproducing decision procedure for real arithmetic. In: Nieuwenhuis, R. (ed.) Automated Deduction – CADE20. CADE 2005. Lecture Notes in Computer Science, vol. 3632. Springer, Berlin (2005)Google Scholar
 18.Narkawicz, A., Muñoz, C.A., Dutle, A.: Formallyverified decision procedures for univariate polynomial computation based on Sturm’s and Tarski’s theorems. J. Autom. Reason. 54(4), 285–326 (2015)MathSciNetCrossRefzbMATHGoogle Scholar
 19.Rahman, Q.I., Schmeisser, G.: Analytic Theory of Polynomials (2002). Oxford University Press, Oxford (2016)Google Scholar
 20.Wilf, H.S.: A global bisection algorithm for computing the zeros of polynomials in the complex plane. J. ACM 25(3), 415–420 (1978)MathSciNetCrossRefzbMATHGoogle Scholar
 21.Yap, C.K., Sagraloff, M.: A simple but exact and efficient algorithm for complex root isolation. In: 36th International Symposium on Symbolic and Algebraic Computation, ISSAC ’11, pp. 353–360. ACM Press (2011)Google Scholar
Copyright information
Open AccessThis article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.