-- The analytic FTA argument reduced to an explicit algebraic power-direction lemma.
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Complex.FTAReduction
import PolynomialStationarity
import ExtremeValue

section Complexes
notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)

theorem complexPolynomial.minimum_power_pairing (c a : Set) (cs : List(ℂ))
  requires coefficient : c ∈ ℂ
  requires center : a ∈ ℂ
  requires minimum : ∀ z ∈ ℂ, complexNormSquared(complexPolynomial(c :: cs)(a)) ≤ complexNormSquared(complexPolynomial(c :: cs)(z))
  shows ∃ n ∈ ℕ, ∃ ds, List(ℂ, ds) ∧ complexPolynomial(ds)(ℂ[0]) ≠ ℂ[0] ∧
    length{ℂ}(cs) = Grace.Core.Nat.Rec.add(n, length{ℂ}(ds)) ∧
    (∀ u ∈ ℂ, realZero ≤ Euclidean.dot(complexPolynomial(c :: cs)(a), ℂ[u ^ succ(n) * complexPolynomial(ds)(ℂ[0])]))
proof
  have steps := dyadicRadii.converges_zero
  have positive : ∀ j ∈ ℕ, realZero < dyadicRadii(j)
    intros j jIn
    have jNat := nat.omega.backward at j with *
    rw dyadicRadii.value
    exact dyadicRadius.positive with *
  exact complexPolynomial.minimum_leading_term with *

-- The descent property is a hypothesis of this theorem; the library assumes
-- no axiom for it.
theorem complexPolynomial.root_of_power_directions (cs : List(ℂ))
  requires nonconstant : cs ≠ []
  requires directions : ∀ n ∈ ℕ, ∀ z ∈ ℂ, ∀ w ∈ ℂ, z ≠ ℂ[0] → w ≠ ℂ[0] →
    ∃ u ∈ ℂ, Euclidean.dot(z, ℂ[u ^ succ(n) * w]) < realZero
  shows ∃ a ∈ ℂ, monicValue(ℂ, identity(ℂ), ℂ, a, cs) = ℂ[0]
proof
  have cases := List.cases with *
  cases cases with empty | cons
  . exfalso
    exact nonconstant with empty
  . obtain ⟨c, cIn, tail, tailList, shape⟩ := cons
    have list : List(ℂ, c :: tail) by typecheck
    obtain ⟨a, aIn, least⟩ := complexPolynomial.global_minimum at c, tail with *
    have function := complexPolynomial.function at c :: tail with *
    have valueIn := FunctionBetween.apply_closed at complexPolynomial(c :: tail), ℂ, ℂ, a with *
    have root : complexPolynomial(c :: tail)(a) = ℂ[0]
      by_contra nonzero
      obtain ⟨n, nIn, ds, dsList, residualNonzero, degree, pairing⟩ := complexPolynomial.minimum_power_pairing at c, a, tail with *
      have residualFunction := complexPolynomial.function at ds with *
      have zeroIn := complexZero.member
      have residualIn := FunctionBetween.apply_closed at complexPolynomial(ds), ℂ, ℂ, ℂ[0] with *
      have nNat := nat.omega.backward at n with *
      obtain ⟨u, uIn, negative⟩ := directions with n, nIn, complexPolynomial(c :: tail)(a), valueIn, complexPolynomial(ds)(ℂ[0]), residualIn, nonzero, residualNonzero
      have nonnegative := pairing with u, uIn
      have ring := complexes.comm_ring
      have ordinary := IsCommRing.ring with ring
      have monoid := IsRing.multiplicative with ordinary
      have power := monoidPow.closed at ℂ, complexMul, complexOne, u, succ(n) with *
      have product := IsRing.mul_closed with ordinary, power, residualIn
      have firstPoint := complex.point with valueIn
      have secondPoint := complex.point with product
      have impossible := realLe.transitive_less at realZero, Euclidean.dot(complexPolynomial(c :: tail)(a), ℂ[u ^ succ(n) * complexPolynomial(ds)(ℂ[0])]), realZero with *
      have irrefl := realLess.irreflexive_on
      exact irrefl with realZero, impossible
    refine ⟨a, aIn, ?_⟩
    rwa [complexPolynomial.value, ← shape] at root

end Complexes