-- A checked local normal form for every nonconstant monic complex polynomial.
-- 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.LocalPolynomial
import SequentialContinuity
import Algebra.Field.Powers
import Algebra.Polynomial.HornerVanishing

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

theorem complexPolynomial.horner_value (x : Set) (cs : List(ℂ))
  requires member : x ∈ ℂ
  shows complexPolynomial(cs)(x) = hornerAt{ℂ}(complexAdd, complexMul, complexOne, x, cs)
proof
  rw complexPolynomial.value
  unfold hornerAt
  rfl

-- No nonroot hypothesis is needed: the normal form also describes roots.
-- n+1 is the first nonconstant exponent; the degree equation bounds it.
theorem complexPolynomial.local_normal_form (c a : Set) (cs : List(ℂ))
  requires coefficient : c ∈ ℂ
  requires center : a ∈ ℂ
  shows ∃ n ∈ ℕ, ∃ ds, List(ℂ, ds) ∧ complexPolynomial(ds)(ℂ[0]) ≠ ℂ[0] ∧
    length{ℂ}(cs) = Grace.Core.Nat.Rec.add(n, length{ℂ}(ds)) ∧
    ComplexContinuous(complexPolynomial(ds)) ∧
    (∀ h ∈ ℂ, complexPolynomial(c :: cs)(ℂ[a + h]) = ℂ[complexPolynomial(c :: cs)(a) + h ^ succ(n) * complexPolynomial(ds)(h)])
proof
  have field := complexes.is_field
  have ring := IsField.comm_ring with field
  have ordinary := IsCommRing.ring with ring
  have monoid := IsRing.multiplicative with ordinary
  have zeroIn : ℂ[0] ∈ ℂ by typecheck
  have unitNonzero : ℂ[1] ≠ ℂ[0]
    have distinct := Nontrivial.distinct with complexes.nontrivial
    intro same
    apply distinct
    symm
    exact same
  have list : List(ℂ, c :: cs) by typecheck
  have data := hornerTranslate.data at ℂ, complexAdd, complexZero, complexNeg, complexMul, complexOne, complexOne, a, c :: cs with *
  have shape := List.cases at ℂ, hornerTranslate{ℂ}(complexAdd, complexMul, complexOne, complexOne, a, c :: cs) with *
  cases shape with empty | nonempty
  . have degree := data.right
    rw [empty, length.nil, length.cons] at degree
    have impossible := Naturals.disjoint.zero.succ at length{ℂ}(cs)
    exfalso
    exact impossible with degree
  . obtain ⟨d, dIn, tail, tailList, translatedShape⟩ := nonempty
    have degree := data.right
    rw [translatedShape, length.cons, length.cons] at degree
    have tailDegree := Naturals.injective.succ with degree
    obtain ⟨n, nIn, ds, dsList, headNonzero, factorDegree, factor⟩ := hornerAt.first_nonzero at ℂ, complexAdd, complexZero, complexNeg, complexMul, complexOne, complexOne, tail with *
    have nNat := nat.omega.backward at n with *
    have constant := hornerTranslate.constant at ℂ, complexAdd, complexZero, complexNeg, complexMul, complexOne, complexOne, a, c :: cs with *
    rw [translatedShape, listHeadOr] at constant
    have headValue := hornerAt.at_zero at ℂ, complexAdd, complexZero, complexNeg, complexMul, complexOne, complexOne, a, ds with *
    have qNonzero : complexPolynomial(ds)(ℂ[0]) ≠ ℂ[0] by rwa [complexPolynomial.horner_value, headValue]
    have degreeBound : length{ℂ}(cs) = Grace.Core.Nat.Rec.add(n, length{ℂ}(ds)) by rwa ← tailDegree
    have continuous := complexPolynomial.continuous at ds with *
    refine ⟨n, nIn, ds, dsList, qNonzero, degreeBound, continuous, ?_⟩
    intros h hIn
    have sum := IsRing.add_closed with ordinary, center, hIn
    have power := monoidPow.closed at ℂ, complexMul, complexOne, h, n with *
    have qValue := hornerAt.closed at ℂ, complexAdd, complexZero, complexNeg, complexMul, complexOne, complexOne, h, ds with *
    have translated := hornerTranslate.value at ℂ, complexAdd, complexZero, complexNeg, complexMul, complexOne, complexOne, a, h, c :: cs with *
    rw [translatedShape, hornerAt.cons] at translated
    have tailFactor := factor with h, hIn
    rw tailFactor at translated
    rw [complexPolynomial.horner_value, ← translated, complexPolynomial.horner_value, complexPolynomial.horner_value, ← constant, monoidPow.succ]
    ring

-- A continuous nonzero value stays nonzero in a sufficiently small disk.
theorem ComplexContinuousAt.eventually_nonzero (f a : Set)
  requires continuous : ComplexContinuousAt(f, a)
  requires nonzero : f(a) ≠ ℂ[0]
  shows ∃ d ∈ ℝ, realZero < d ∧
    (∀ x ∈ ℂ, complexNormSquared(ℂ[x - a]) < d → f(x) ≠ ℂ[0])
proof
  unfold ComplexContinuousAt at continuous
  have image := FunctionBetween.apply_closed at f, ℂ, ℂ, a with *
  have positive := complexNormSquared.positive with *
  obtain ⟨d, dReal, dPositive, control⟩ := continuous.right.right with complexNormSquared(f(a)), positive
  refine ⟨d, dReal, dPositive, ?_⟩
  intros x xIn near vanishes
  have small := control with x, xIn, near
  rw vanishes at small
  have ring := complexes.comm_ring
  have ordinary := IsCommRing.ring with ring
  have difference : ℂ[0 - f(a)] = ℂ[-f(a)] by ring
  rw [difference, complexNormSquared.neg] at small
  have irrefl := realLess.irreflexive_on
  exact irrefl with complexNormSquared(f(a)), small

-- Every root of a nonconstant monic polynomial is isolated.
theorem complexPolynomial.isolated_root (c a : Set) (cs : List(ℂ))
  requires coefficient : c ∈ ℂ
  requires center : a ∈ ℂ
  requires root : complexPolynomial(c :: cs)(a) = ℂ[0]
  shows ∃ d ∈ ℝ, realZero < d ∧
    (∀ h ∈ ℂ, h ≠ ℂ[0] → complexNormSquared(h) < d → complexPolynomial(c :: cs)(ℂ[a + h]) ≠ ℂ[0])
proof
  obtain ⟨n, nIn, ds, dsList, nonzero, degree, continuous, expansion⟩ := complexPolynomial.local_normal_form at c, a, cs with *
  have zeroIn := complexZero.member
  have atZero := continuous.right with ℂ[0], zeroIn
  obtain ⟨d, dReal, dPositive, nonvanishing⟩ := ComplexContinuousAt.eventually_nonzero at complexPolynomial(ds), ℂ[0] with *
  refine ⟨d, dReal, dPositive, ?_⟩
  intros h hIn hNonzero near
  have field := complexes.is_field
  have ring := IsField.comm_ring with field
  have ordinary := IsCommRing.ring with ring
  have monoid := IsRing.multiplicative with ordinary
  have difference : ℂ[h - 0] = h by ring
  have nearZero : complexNormSquared(ℂ[h - 0]) < d by rwa difference
  have qNonzero := nonvanishing with h, hIn, nearZero
  have nNat := nat.omega.backward at n with *
  have powerNonzero := IsField.power_nonzero at ℂ, complexAdd, complexZero, complexNeg, complexMul, complexOne, h, succ(n) with *
  have power := monoidPow.closed at ℂ, complexMul, complexOne, h, succ(n) with *
  have function := continuous.left
  have qValue := FunctionBetween.apply_closed at complexPolynomial(ds), ℂ, ℂ, h with *
  have value := expansion with h, hIn
  rw root at value
  have simplify : ℂ[0 + h ^ succ(n) * complexPolynomial(ds)(h)] = ℂ[h ^ succ(n) * complexPolynomial(ds)(h)] by ring
  rw simplify at value
  rw value
  intro vanishes
  have noZero := IsField.no_zero_divisors with field
  have alternatives := noZero with h ^ succ(n), complexPolynomial(ds)(h), qValue, vanishes
  cases alternatives with first | second
  . exact powerNonzero with first
  . exact qNonzero with second

end Complexes