1810.04314

Shilpi Goel and Matt Kaufmann (Eds.): ACL2 Theorem Prover and its Applications (ACL2-2018) EPTCS 280, 2018, pp. 98-110, doi:10.4204/EPTCS.280.8 c R. Gamboa & J. Cowles This work is licensed under the Creative Commons Attribution License. The Fundamental Theorem of Algebra in ACL2 Ruben Gamboa & John Cowles University of Wyoming Laramie, Wyoming { ruben,cowles } @uwyo.edu We report on a verification of the Fundamental Theorem of Algebra in ACL2(r). The proof con- sists of four parts. First, continuity for both complex-valued and real-valued functions of complex numbers is defined, and it is shown that continuous functions from the complex to the real numbers achieve a minimum value over a closed square region. An important case of continuous real-valued, complex functions results from taking the traditional complex norm of a continuous complex func- tion. We think of these continuous functions as having only one (complex) argument, but in ACL2(r) they appear as functions of two arguments. The extra argument is a "context", which is uninterpreted. For example, it could be other arguments that are held fixed, as in an exponential function which has a base and an exponent, either of which could be held fixed. Second, it is shown that complex poly- nomials are continuous, so the norm of a complex polynomial is a continuous real-valued function and it achieves its minimum over an arbitrary square region centered at the origin. This part of the proof benefits from the introduction of the "context" argument, and it illustrates an innovation that simplifies the proofs of classical properties with unbound parameters. Third, we derive lower and upper bounds on the norm of non-constant polynomials for inputs that are sufficiently far away from the origin. This means that a sufficiently large square can be found to guarantee that it contains the global minimum of the norm of the polynomial. Fourth, it is shown that if a given number is not a root of a non-constant polynomial, then it cannot be the global minimum. Finally, these results are combined to show that the global minimum must be a root of the polynomial. This result is part of a larger effort in the formalization of complex polynomials in ACL2(r). 1 Introduction In this paper, we describe a verification of the Fundamental Theorem of Algebra (FTA) in ACL2(r). That is, we prove that if p is a non-constant, complex 1 polynomial with complex coefficients, then there is some complex number z such that p ( z ) = 0. The proof follows the outline of the first proof in [3], and it is a formal version of d'Alembert's proof of 1746 [1], which is illustrated (literally) in [11]. Figure 1 provides an outline of the proof, which comprises three main strands. First (step 1 in Figure 1), we show that continuous functions from the complex plane to the reals always achieve a minimum value in a closed, bounded, rectangular region. The consequence to the FTA is that if p is a complex polynomial, then the function mapping z ∈ C to || p ( z ) || , where || · || denotes the traditional complex norm, achieves a minimum value in a square region centered at the origin (steps 2, 3, and 5). Second (step 4), we show that the norm of polynomials is dominated by the term of highest power. In particular, if p ( z ) = a n z n + a n - 1 z n - 1 + ··· + a 0 , then 1 2 || a n |||| z || n < || p ( z ) || < 3 2 || a n |||| z || n for sufficiently large z . These two facts can be combined to show that the global minimum of a polynomial (norm) must be enclosed in a possibly large region around the origin, so the polynomial must achieve this global minimum. The third strand (step 6), known as d'Alembert's Lemma, states that if p is a complex 1 By "complex" we mean the traditional mathematical view that the complex numbers are an extension of the real numbers, not the ACL2 view that complex numbers are necessarily not real.

R. Gamboa & J. Cowles 99 Figure 1: Proof Outline polynomial and z is such that p ( z ) 6 = 0, then there is some z 0 such that || p ( z 0 ) || < || p ( z ) || . This implies that the global minimum guaranteed by the previous lemmas must be a root of the polynomial (step 7). To our knowledge, this is the first proof of the Fundamental Theorem of Algebra in the Boyer- Moore family of theorem provers, but it has been proved earlier in other theorem provers, e.g., Mizar [9], HOL [8], and Coq [7]. 2 Continuity and the Extreme Value Theorem 2.1 Continuous Functions We begin the proof of the FTA with a proof of the Extreme Value Theorem for complex functions. The first step is to define the notion of continuity for complex functions, and this follows the pattern used before for real functions [6]. In particular, we say that f is continuous if for any standard number z , f ( z ) is close to f ( z * ) for any z * that is close to z . To be precise, two complex numbers are "close" if both the real and imaginary parts of their difference are infinitesimal. This also implies that the distance between the two points is infinitesimal. We also introduced in ACL2(r) the notion of a continuous function from the complex to the real numbers, and we proved that if both f : C → C and g : C → R are continuous, then so is g ◦ f : C → R . Moreover, we proved that the function given by the traditional complex norm, || a + bi || = √ a 2 + b 2 , is continuous. So for any continuous function f : C → C , the function from C to R given by h ( z ) = || f ( z ) || is continuous. An important difference from the development in [6] is that continuous functions in this paper have two arguments in ACL2, even though we think of them as functions of only one variable. This is similar to the way the function x n and a x are introduced in elementary calculus. Those functions are thought of as functions of the single variable x , and the derivatives are given as nx n - 1 and a x ln a , even though both

100 Fund. Thm. of Algebra functions are simply slices of the bivariate function x y . In ACL2(r), we introduce the continuous function ccfn using encapsulate as (ccfn context z) , where the argument z is the one that is allowed to vary, whereas context is the argument that is held fixed. The non-standard definition of continuity that we use here requires that close points be mapped to close values, but only for standard z . Similarly, we require that close points are mapped to close values only when both z and context are standard. The context argument plays an important role, which can be illustrated by the continuity of poly- nomials. Consider, for example, a proof that the function x n is continuous. This would appear to be easy to prove by induction as follows: 1. x 0 is a constant function, so it is definitely continuous. 2. x n = x n - 1 · x , and x n - 1 is continuous from the induction hypothesis, and so is the product of con- tinuous functions. However, this does not work. The formal definition of continuity uses the non-classical notions of close : standard ( x ) ∧ close ( x , x 0 ) → close ( x n , x n 0 ) . But ACL2(r) restricts induction on non-classical functions to standard values of the arguments. In this particular case, we could prove that x n is continuous, but only for standard values of n , as was done in [10]. Setting that aside for now, we can imagine what would happen if we could establish (somehow) that complex polynomials are continuous. The next step in the proof would be to show that since p ( z ) is continuous in the complex plane, then || p ( z ) || is continuous from C to R , and this could be done by functionally instantiating the previous result about norms of continuous functions. Once more, however, we run into a major complication. The problem is that we want to say this about all polynomials, not just about a specific polynomial p . For example, we could use this approach to show that the norm of the following polynomial is continuous: (defun p(z) (+ 1 (* #c(0 1) z) (* 3 z z))) But that would lead to a proof that the polynomial p has a root, not that all polynomials have roots. To reason about all polynomials, we use a data structure that can represent any polynomial and an evaluator function that can compute the value of a given polynomial at a given point. For example, the polynomial above is represented with the list (1 #c(0 1) 3) , and the function eval-polynomial is defined so that (eval-polynomial '(1 #c(0 1) 3) z) = (p z) . But we cannot use functional instantiation to show that the norm of eval-polynomial is continuous, because the formal statement of continuity uses the non-classical notion of close . ACL2(r) restricts functional instantiation so that pseudo-lambda expressions cannot be used in place of functions when the theorem to be proved uses non-classical functions. It should be noted that both of these restrictions are necessary! For example, x n is "obviously" continuous, but what happens when n is large? Suppose that x = 1 + ε , where ε is small, so that 1 and 1 + ε are close. From the binomial theorem, ( 1 + ε ) n = 1 + n ε + ··· . The thing is that if n is large, n ε is not necessarily small. For instance, if n = 1 / ε , then n ε = 1, and ( 1 + ε ) n > 2, so it is not close to 1 n = 1. Yes, x n is continuous, but the non-standard definition of continuity only applies when x and n are standard. Similarly, the restriction for pseudo-lambda expressions is crucial. Consider, for example, the theo- rem that f ( x ) is standard when x is standard. This is true, but we could not use it to show that x + y is standard when x is standard by functionally instantiating λ x . x + y for f . The proposed theorem is just not true when, for example, x = 0 and y = ε .