ComplexPolynomialMinimum

Concrete complex estimates and the explicit minimum-modulus reduction

Open in Workbench View on GitHub

1-- Concrete complex estimates and the explicit minimum-modulus reduction.2-- Copyright (c) 2026 Grant Passmore.3-- Released under the Apache License 2.0. See LICENSE in the repository root.4-- Authors: Grant Passmore56module ComplexPolynomialMinimumExample7import Grace.Cumulus.Complex.PolynomialMinimum89section Complexes10notation ring C := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)11notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)1213theorem product (z w : Set)14  requires first : z ∈ C15  requires second : w ∈ C16  shows complexNormSquared(C[z * w]) = R[complexNormSquared(z) * complexNormSquared(w)]17proof18  exact complexNormSquared.mul with *1920theorem decrease (z w : Set)21  requires first : z ∈ C22  requires second : w ∈ C23  requires direction : R[2 * Euclidean.dot(z, w) + complexNormSquared(w)] < R[0]24  shows complexNormSquared(C[z + w]) < complexNormSquared(z)25proof26  exact complexNormSquared.strict_descent with *2728-- Neither analytic premise below is yet proved for all nonconstant polynomials.29theorem root (cs : List(complexCarrier))30  requires minimum : ∃ a ∈ C, ∀ z ∈ C, complexNormSquared(complexPolynomial(cs)(a)) ≤ complexNormSquared(complexPolynomial(cs)(z))31  requires descent : ∀ a ∈ C, complexPolynomial(cs)(a) ≠ C[0] → ∃ z ∈ C, complexNormSquared(complexPolynomial(cs)(z)) < complexNormSquared(complexPolynomial(cs)(a))32  shows ∃ a ∈ C, monicValue(C, identity(C), C, a, cs) = C[0]33proof34  exact complexPolynomial.root_of_minimum_and_descent with *3536end Complexes37section Translation38variable (A add zero neg mul one leading a x : Set)39notation ring R := (A, add, zero, neg, mul, one)40hypothesis ring : IsCommRing(R)41hypothesis initial : leading ∈ R42hypothesis center : a ∈ R43hypothesis element : x ∈ R4445theorem translated_value (cs : List(A))46  shows hornerAt{A}(add, mul, leading, x, hornerTranslate{A}(add, mul, one, leading, a, cs)) = hornerAt{A}(add, mul, leading, R[a + x], cs)47proof48  exact hornerTranslate.value with *4950theorem translated_constant (cs : List(A))51  shows listHeadOr{A}(leading, hornerTranslate{A}(add, mul, one, leading, a, cs)) = hornerAt{A}(add, mul, leading, a, cs)52proof53  exact hornerTranslate.constant with *5455end Translation56