Grace/Cumulus/Complex/FTAReduction.g17
Imports
PolynomialStationarity · ExtremeValue
Declarations
- complexPolynomial.minimum_power_pairing theorem derivation
- complexPolynomial.root_of_power_directions theorem derivation
Source
1-- The analytic FTA argument reduced to an explicit algebraic power-direction lemma.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 Passmore67module Grace.Cumulus.Complex.FTAReduction8import PolynomialStationarity9import ExtremeValue1011section Complexes12notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)1314theorem complexPolynomial.minimum_power_pairing (c a : Set) (cs : List(ℂ))15 requires coefficient : c ∈ ℂ16 requires center : a ∈ ℂ17 requires minimum : ∀ z ∈ ℂ, complexNormSquared(complexPolynomial(c :: cs)(a)) ≤ complexNormSquared(complexPolynomial(c :: cs)(z))18 shows ∃ n ∈ ℕ, ∃ ds, List(ℂ, ds) ∧ complexPolynomial(ds)(ℂ[0]) ≠ ℂ[0] ∧19 length{ℂ}(cs) = Grace.Core.Nat.Rec.add(n, length{ℂ}(ds)) ∧20 (∀ u ∈ ℂ, realZero ≤ Euclidean.dot(complexPolynomial(c :: cs)(a), ℂ[u ^ succ(n) * complexPolynomial(ds)(ℂ[0])]))21proof22 have steps := dyadicRadii.converges_zero23 have positive : ∀ j ∈ ℕ, realZero < dyadicRadii(j)24 intros j jIn25 have jNat := nat.omega.backward at j with *26 rw dyadicRadii.value27 exact dyadicRadius.positive with *28 exact complexPolynomial.minimum_leading_term with *2930-- The descent property is a hypothesis of this theorem; the library assumes31-- no axiom for it.32theorem complexPolynomial.root_of_power_directions (cs : List(ℂ))33 requires nonconstant : cs ≠ []34 requires directions : ∀ n ∈ ℕ, ∀ z ∈ ℂ, ∀ w ∈ ℂ, z ≠ ℂ[0] → w ≠ ℂ[0] →35 ∃ u ∈ ℂ, Euclidean.dot(z, ℂ[u ^ succ(n) * w]) < realZero36 shows ∃ a ∈ ℂ, monicValue(ℂ, identity(ℂ), ℂ, a, cs) = ℂ[0]37proof38 have cases := List.cases with *39 cases cases with empty | cons40 . exfalso41 exact nonconstant with empty42 . obtain ⟨c, cIn, tail, tailList, shape⟩ := cons43 have list : List(ℂ, c :: tail) by typecheck44 obtain ⟨a, aIn, least⟩ := complexPolynomial.global_minimum at c, tail with *45 have function := complexPolynomial.function at c :: tail with *46 have valueIn := FunctionBetween.apply_closed at complexPolynomial(c :: tail), ℂ, ℂ, a with *47 have root : complexPolynomial(c :: tail)(a) = ℂ[0]48 by_contra nonzero49 obtain ⟨n, nIn, ds, dsList, residualNonzero, degree, pairing⟩ := complexPolynomial.minimum_power_pairing at c, a, tail with *50 have residualFunction := complexPolynomial.function at ds with *51 have zeroIn := complexZero.member52 have residualIn := FunctionBetween.apply_closed at complexPolynomial(ds), ℂ, ℂ, ℂ[0] with *53 have nNat := nat.omega.backward at n with *54 obtain ⟨u, uIn, negative⟩ := directions with n, nIn, complexPolynomial(c :: tail)(a), valueIn, complexPolynomial(ds)(ℂ[0]), residualIn, nonzero, residualNonzero55 have nonnegative := pairing with u, uIn56 have ring := complexes.comm_ring57 have ordinary := IsCommRing.ring with ring58 have monoid := IsRing.multiplicative with ordinary59 have power := monoidPow.closed at ℂ, complexMul, complexOne, u, succ(n) with *60 have product := IsRing.mul_closed with ordinary, power, residualIn61 have firstPoint := complex.point with valueIn62 have secondPoint := complex.point with product63 have impossible := realLe.transitive_less at realZero, Euclidean.dot(complexPolynomial(c :: tail)(a), ℂ[u ^ succ(n) * complexPolynomial(ds)(ℂ[0])]), realZero with *64 have irrefl := realLess.irreflexive_on65 exact irrefl with realZero, impossible66 refine ⟨a, aIn, ?_⟩67 rwa [complexPolynomial.value, ← shape] at root6869end Complexes70