ComplexDescent
1module ComplexDescentExample2-- 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.Descent89section Complexes10notation ring C := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)11notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)1213theorem power (t : Real) (z : Set) (n : Nat)14 requires member : z ∈ C15 shows monoidPow(C, complexScale(t, z), n) = complexScale(realPow(t, n), monoidPow(C, z, n))16proof17 exact complexScale.power at t, z, n with *1819theorem directional_descent (z w : Set) (t : Real)20 requires first : z ∈ C21 requires second : w ∈ C22 requires direction : Euclidean.dot(z, w) < realZero23 requires positive : realZero < t24 requires small : t < scaledRadius(R[-Euclidean.dot(z, w)], limitScale(complexNormSquared(w)))25 shows complexNormSquared(C[z + complexScale(t, w)]) < complexNormSquared(z)26proof27 exact complexNormSquared.directional_descent at z, w, t with *2829theorem descent_radius (z w : Set)30 requires first : z ∈ C31 requires second : w ∈ C32 requires direction : Euclidean.dot(z, w) < realZero33 shows ∃ d ∈ ℝ, realZero < d ∧34 (∀ t ∈ ℝ, realZero < t → t < d → complexNormSquared(C[z + complexScale(t, w)]) < complexNormSquared(z))35proof36 exact complexNormSquared.descent_radius at z, w with *3738theorem ray_normal_form (c a : Set) (cs : List(C))39 requires coefficient : c ∈ C40 requires center : a ∈ C41 shows ∃ n ∈ ℕ, ∃ ds, List(C, ds) ∧ complexPolynomial(ds)(C[0]) ≠ C[0] ∧42 length{C}(cs) = Grace.Core.Nat.Rec.add(n, length{C}(ds)) ∧43 ComplexContinuous(complexPolynomial(ds)) ∧44 (∀ u ∈ C, ∀ t ∈ ℝ, complexPolynomial(c :: cs)(C[a + complexScale(t, u)]) = C[complexPolynomial(c :: cs)(a) + complexScale(realPow(t, succ(n)), C[monoidPow(C, u, succ(n)) * complexPolynomial(ds)(complexScale(t, u))])])45proof46 exact complexPolynomial.ray_normal_form at c, a, cs with *4748end Complexes49