-- The fundamental theorem of algebra for every nonconstant 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.FundamentalTheoremGeneral
import FundamentalTheorem
import Algebra.Polynomial.HornerNormalization

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

-- A product with a unit's partner vanishes only at zero.
theorem complex.zero_of_inverse_mul (b c v : Set)
  requires bIn : b ∈ ℂ
  requires cIn : c ∈ ℂ
  requires vIn : v ∈ ℂ
  requires cancels : ℂ[b * c] = ℂ[1]
  requires product : ℂ[b * v] = ℂ[0]
  shows v = ℂ[0]
proof
  linear_combination c * product - v * cancels

-- Scaling the leading coefficient and every lower coefficient by b scales
-- the value of the polynomial by b.
theorem complexPolynomial.leading_scale (b c x : Set) (cs : List(ℂ))
  requires bIn : b ∈ ℂ
  requires cIn : c ∈ ℂ
  requires xIn : x ∈ ℂ
  shows hornerAt{ℂ}(complexAdd, complexMul, ℂ[b * c], x, ringScale{ℂ}(complexMul, b, cs)) =
    ℂ[b * hornerAt{ℂ}(complexAdd, complexMul, c, x, cs)]
proof
  have ring := complexes.comm_ring
  have hom := IsRingHom.identity with ring
  have scaled := hornerValue.scale at complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne,
    complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne,
    identity(complexCarrier), x, b, c, cs with *
  have bValue := identity.apply with bIn
  rw bValue at scaled
  unfold hornerAt
  cc

-- Scaling preserves nonemptiness of the coefficient list.
theorem complexPolynomial.scaled_nonempty (b : Set) (cs : List(ℂ))
  requires bIn : b ∈ ℂ
  requires nonconstant : cs ≠ []
  shows ringScale{ℂ}(complexMul, b, cs) ≠ []
proof
  have cases := List.cases with *
  cases cases with empty | cons
  . exfalso
    exact nonconstant with empty
  . obtain ⟨d, dIn, tail, tailList, shape⟩ := cons
    have productIn : ℂ[b * d] ∈ ℂ by typecheck
    have scaleClosed : ∀ u ∈ ℂ, ℂ[b * u] ∈ ℂ
      intros u uIn
      typecheck
    have scaledTail := ringScale.closed at complexCarrier, complexMul, b, tail with scaleClosed
    rw [shape, ringScale]
    intro equal
    symm at equal
    exact List.inductive.disjoint.nil.cons at ℂ[b * d],
      ringScale{ℂ}(complexMul, b, tail) with equal

-- The fundamental theorem of algebra with an arbitrary nonzero leading
-- coefficient c: cs lists the lower coefficients in ascending order, so the
-- polynomial is c X^n + cs(n-1) X^(n-1) + ... + cs(0) with n = length(cs) ≥ 1.
theorem complexes.fundamental_theorem_of_algebra_general (c : Set) (cs : List(ℂ))
  requires leading : c ∈ ℂ
  requires nonzero : c ≠ ℂ[0]
  requires nonconstant : cs ≠ []
  shows ∃ a ∈ ℂ, hornerAt{ℂ}(complexAdd, complexMul, c, a, cs) = ℂ[0]
proof
  have field := complexes.is_field
  have ring := complexes.comm_ring
  obtain ⟨b, inverse⟩ := IsField.inverse_exists with field, leading, nonzero
  have bIn := inverse.right.left
  have cancels := inverse.right.right.left
  have scaleClosed : ∀ u ∈ ℂ, ℂ[b * u] ∈ ℂ
    intros u uIn
    typecheck
  have scaledList := ringScale.closed with *
  have scaledNonempty := complexPolynomial.scaled_nonempty with bIn, nonconstant
  obtain ⟨a, aIn, root⟩ := complexes.fundamental_theorem_of_algebra at
    ringScale{ℂ}(complexMul, b, cs) with *
  have monicRoot : hornerAt{ℂ}(complexAdd, complexMul, ℂ[1], a, ringScale{ℂ}(complexMul, b, cs)) = ℂ[0]
    unfold hornerAt
    cc
  have scaled := complexPolynomial.leading_scale at b, c, a, cs with *
  rw [cancels, monicRoot] at scaled
  have valueIn := hornerAt.closed at
    complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne, c, a, cs with *
  symm at scaled
  refine ⟨a, aIn, ?_⟩
  exact complex.zero_of_inverse_mul with bIn, leading, valueIn, cancels, scaled

end Complexes

-- The same theorem for a single ascending coefficient list cs representing
-- cs(0) + cs(1) X + ... : a nonzero coefficient of X^(n+1) makes the
-- polynomial nonconstant, whatever zeros follow it.
theorem complexes.fundamental_theorem_of_algebra_coefficients (cs : List(complexCarrier)) (n : Nat)
  requires nonconstant : listCoefficient{complexCarrier}(complexZero, cs, n + 1) ≠ complexZero
  shows ∃ a ∈ complexCarrier,
    hornerAt{complexCarrier}(complexAdd, complexMul, complexZero, a, cs) = complexZero
proof
  have ring := complexes.comm_ring
  have successor := add.right_one at n
  rw successor at nonconstant
  have cases := List.cases with *
  cases cases with empty | cons
  . exfalso
    rw [empty, listCoefficient.nil] at nonconstant
    apply nonconstant
    rfl
  . obtain ⟨d, dIn, tail, tailList, shape⟩ := cons
    rw [shape, listCoefficient.succ] at nonconstant
    have tailNonzero : ∃ m, Nat(m) ∧ listCoefficient{complexCarrier}(complexZero, tail, m) ≠ complexZero
      refine ⟨n, assumption, nonconstant⟩
    obtain ⟨leading, leadingIn, nonzero, lower, lowerList, equal⟩ := hornerAt.normalize at
      complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne, tail with *
    have consNonempty : d :: lower ≠ []
      intro same
      symm at same
      exact List.inductive.disjoint.nil.cons at d, lower with same
    obtain ⟨a, aIn, root⟩ := complexes.fundamental_theorem_of_algebra_general at
      leading, d :: lower with *
    have value := equal with a, aIn
    refine ⟨a, aIn, ?_⟩
    rw [shape, hornerAt.cons, value]
    rw hornerAt.cons at root
    exact root