ComplexLocalPolynomial
1module ComplexLocalPolynomialExample2-- 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 Passmore67import Grace.Cumulus.Complex.LocalPolynomial89section Complexes10notation ring C := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)1112theorem local_normal_form (c a : Set) (cs : List(C))13 requires coefficient : c ∈ C14 requires center : a ∈ C15 shows ∃ n ∈ ℕ, ∃ ds, List(C, ds) ∧ complexPolynomial(ds)(C[0]) ≠ C[0] ∧16 length{C}(cs) = Grace.Core.Nat.Rec.add(n, length{C}(ds)) ∧17 ComplexContinuous(complexPolynomial(ds)) ∧18 (∀ h ∈ C, complexPolynomial(c :: cs)(C[a + h]) = C[complexPolynomial(c :: cs)(a) + monoidPow(C, h, succ(n)) * complexPolynomial(ds)(h)])19proof20 exact complexPolynomial.local_normal_form at c, a, cs with *2122theorem isolated_root (c a : Set) (cs : List(C))23 requires coefficient : c ∈ C24 requires center : a ∈ C25 requires root : complexPolynomial(c :: cs)(a) = C[0]26 shows ∃ d ∈ ℝ, realZero < d ∧27 (∀ h ∈ C, h ≠ C[0] → complexNormSquared(h) < d → complexPolynomial(c :: cs)(C[a + h]) ≠ C[0])28proof29 exact complexPolynomial.isolated_root at c, a, cs with *3031end Complexes32