ComplexPolynomialGrowth

Growth and the compact-disk reduction for arbitrary-degree monic polynomials

Open in Workbench View on GitHub

1-- Growth and the compact-disk reduction for arbitrary-degree monic polynomials.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67-- Copyright (c) 2026 Grant Passmore. Apache License 2.0.8module ComplexPolynomialGrowthExample9import Grace.Cumulus.Complex.PolynomialGrowth1011section Growth12notation ring C := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)13notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)1415theorem escape (c : Set) (target : Real) (cs : List(complexCarrier))16  requires coefficient : c ∈ C17  shows ∃ radius ∈ ℝ, realZero ≤ radius ∧ (∀ z ∈ C, radius ≤ complexNormSquared(z) → target < complexNormSquared(complexPolynomial(c :: cs)(z)))18proof19  exact complexPolynomial.grows_at_infinity with *2021theorem lower_step (c z w : Set) (target : Real)22  requires coefficient : c ∈ C23  requires first : z ∈ C24  requires second : w ∈ C25  requires unitBound : R[1] ≤ complexNormSquared(w)26  requires large : R[2 * (target + complexNormSquared(c))] ≤ complexNormSquared(z)27  shows target ≤ complexNormSquared(C[c + z * w])28proof29  exact complexNormSquared.horner_step_lower_bound with *3031-- Disk minimization is a hypothesis here.32theorem minimum (c : Set) (cs : List(complexCarrier))33  requires coefficient : c ∈ C34  requires diskMinima : ∀ radius ∈ ℝ, realZero ≤ radius → ComplexDiskMinimum(complexPolynomial(c :: cs), radius)35  shows ∃ a ∈ C, ∀ z ∈ C, complexNormSquared(complexPolynomial(c :: cs)(a)) ≤ complexNormSquared(complexPolynomial(c :: cs)(z))36proof37  exact complexPolynomial.minimum_of_disk_minima with *3839theorem root (c : Set) (cs : List(complexCarrier))40  requires coefficient : c ∈ C41  requires diskMinima : ∀ radius ∈ ℝ, realZero ≤ radius → ComplexDiskMinimum(complexPolynomial(c :: cs), radius)42  requires descent : ∀ a ∈ C, complexPolynomial(c :: cs)(a) ≠ C[0] → ∃ z ∈ C, complexNormSquared(complexPolynomial(c :: cs)(z)) < complexNormSquared(complexPolynomial(c :: cs)(a))43  shows ∃ a ∈ C, monicValue(C, identity(C), C, a, c :: cs) = C[0]44proof45  exact complexPolynomial.root_of_disk_minima_and_descent with *4647end Growth48