ComplexPolynomialExtremeValue

Minimum attainment; axiom audit records the existing Global Choice route

Open in Workbench View on GitHub

1-- Minimum attainment; axiom audit records the existing Global Choice route.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 ComplexPolynomialExtremeValueExample9import Grace.Cumulus.Complex.ExtremeValue10theorem disk_minimum (cs : List(complexCarrier)) (radius : Real)11  requires nonnegative : realZero ≤ radius12  shows ComplexDiskMinimum(complexPolynomial(cs), radius)13proof14  exact complexPolynomial.disk_minimum with *1516theorem global_minimum (c : Set) (cs : List(complexCarrier))17  requires coefficient : c ∈ complexCarrier18  shows ∃ a ∈ complexCarrier, ∀ z ∈ complexCarrier,19    complexNormSquared(complexPolynomial(c :: cs)(a)) ≤ complexNormSquared(complexPolynomial(c :: cs)(z))20proof21  exact complexPolynomial.global_minimum with *2223-- Local descent remains a hypothesis here.24section Complexes25notation ring C := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)2627theorem root_if_descent (c : Set) (cs : List(C))28  requires coefficient : c ∈ C29  requires descent : ∀ a ∈ C, complexPolynomial(c :: cs)(a) ≠ C[0] → ∃ z ∈ C, complexNormSquared(complexPolynomial(c :: cs)(z)) < complexNormSquared(complexPolynomial(c :: cs)(a))30  shows ∃ a ∈ C, monicValue(C, identity(C), C, a, c :: cs) = C[0]31proof32  exact complexPolynomial.root_of_descent with *3334end Complexes35