-- Roots in ℂ: for n ≥ 1 and c ∈ ℂ the solutions of zⁿ = c are the roots
-- of the polynomial zⁿ − c in Horner form, so finitely many
-- 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.Geometry.Absorption.Roots
import Complex.Field
import Complex.PowerArithmetic
import Algebra.Polynomial.HornerRoots

-- A run of k zero coefficients, and the roots of zᵏ⁺¹ − c as the root
-- set of the Horner form with the lower coefficients −c, 0, …, 0.
def complexZeros (k : Nat) → Set
  | zero => []
  | succ(j) => complexZero :: complexZeros(j)

def complexPowerRoots (c : Set, k : Nat) : Set :=
  hornerRoots{complexCarrier}(complexAdd, complexZero, complexMul, complexOne,
    complexNeg(c) :: complexZeros(k))

def complexUnityRoots (k : Nat) : Set := complexPowerRoots(complexOne, k)

theorem complexZeros.zero
  shows complexZeros(0) = []
proof
  simp [complexZeros]

theorem complexZeros.succ (j : Nat)
  shows complexZeros(succ(j)) = complexZero :: complexZeros(j)
proof
  simp [complexZeros]

theorem complexZeros.list (k : Nat)
  shows List(complexCarrier, complexZeros(k))
proof
  induction k
  | zero =>
    rw complexZeros.zero
    typecheck
  | succ(j) using ih =>
    have zeroIn := complexZero.member
    rw complexZeros.succ
    typecheck

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

-- The Horner value of a run of zero coefficients under the leading
-- coefficient 1 is the power zᵏ.
theorem hornerAt.zeros (z : Set) (k : Nat)
  requires member : z ∈ complexCarrier
  shows hornerAt{complexCarrier}(complexAdd, complexMul, complexOne, z,
      complexZeros(k)) =
    monoidPow(complexMul, complexOne, z, k)
proof
  induction k
  | zero =>
    rw [complexZeros.zero, hornerAt.nil, monoidPow.zero]
    rfl
  | succ(j) using ih =>
    have ring := complexes.comm_ring
    have ordinary := IsCommRing.ring with ring
    have monoid := IsRing.multiplicative with ordinary
    have zeroIn := complexZero.member
    have tail := complexZeros.list at j
    have power := monoidPow.closed at complexCarrier, complexMul, complexOne, z, j
      with monoid, member
    have product := IsRing.mul_closed with ordinary, member, power
    rw [complexZeros.succ, hornerAt.cons, ih, monoidPow.succ]
    ring

theorem complexPowerRoots.graph (c : Set, k : Nat)
  shows complexPowerRoots(c, k) =
    hornerRoots{complexCarrier}(complexAdd, complexZero, complexMul, complexOne,
      complexNeg(c) :: complexZeros(k))
proof
  simp [complexPowerRoots]

theorem complexUnityRoots.graph (k : Nat)
  shows complexUnityRoots(k) = complexPowerRoots(complexOne, k)
proof
  simp [complexUnityRoots]

theorem complexPowerRoots.contains (z c : Set) (k : Nat)
  requires member : z ∈ complexCarrier
  requires target : c ∈ complexCarrier
  requires power : monoidPow(complexMul, complexOne, z, succ(k)) = c
  shows z ∈ complexPowerRoots(c, k)
proof
  have ring := complexes.comm_ring
  have ordinary := IsCommRing.ring with ring
  have oneIn := complexOne.member
  have negIn := IsRing.neg_closed with ordinary, target
  have zeroIn := complexZero.member
  have tail := complexZeros.list at k
  have value := hornerAt.zeros with member
  rw monoidPow.succ at power
  have vanishes : hornerAt{complexCarrier}(complexAdd, complexMul, complexOne, z,
      complexNeg(c) :: complexZeros(k)) = complexZero
    rw [hornerAt.cons, value, power]
    ring
  rw complexPowerRoots.graph
  exact hornerRoots.membership.backward with ⟨member, vanishes⟩

theorem complexPowerRoots.finite (c : Set, k : Nat)
  requires target : c ∈ complexCarrier
  shows Finite(complexPowerRoots(c, k))
proof
  have field := complexes.is_field
  have ring := complexes.comm_ring
  have ordinary := IsCommRing.ring with ring
  have oneIn := complexOne.member
  have negIn := IsRing.neg_closed with ordinary, target
  have zeroIn := complexZero.member
  have tail := complexZeros.list at k
  have distinct := Nontrivial.distinct with complexes.nontrivial
  have nonzero : complexOne ≠ complexZero
    intro same
    symm at same
    exact distinct with same
  rw complexPowerRoots.graph
  exact hornerRoots.finite with field, oneIn, nonzero

theorem complexUnityRoots.contains (z : Set) (k : Nat)
  requires member : z ∈ complexCarrier
  requires power : monoidPow(complexMul, complexOne, z, succ(k)) = complexOne
  shows z ∈ complexUnityRoots(k)
proof
  have oneIn := complexOne.member
  rw complexUnityRoots.graph
  exact complexPowerRoots.contains with member, oneIn, power

theorem complexUnityRoots.finite (k : Nat)
  shows Finite(complexUnityRoots(k))
proof
  have oneIn := complexOne.member
  rw complexUnityRoots.graph
  exact complexPowerRoots.finite with oneIn

end Complexes