-- Horner representations evaluated through arbitrary coefficient extensions (ZF).
-- 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.Algebra.Polynomial.HornerExtension
import HornerDegree
import Characteristic

section Extensions
variable (I A add zero neg mul one B plus z minus times unit f v j : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring S := (B, plus, z, minus, times, unit)
notation ring P := R[I]
hypothesis source : IsCommRing(R)
hypothesis target : IsCommRing(S)
hypothesis hom : IsRingHom(f, R, S)
hypothesis assignment : v : I → S
hypothesis index : j ∈ I

theorem polynomialAtOver.from_horner (leading : Set) (cs : List(A))
  requires initial : leading ∈ R
  shows polynomialAtOver(I, R, S, f, v)(polynomialFromHorner(I, R, j, leading, cs)) =
    monicValue{A}(f, plus, times, f(leading), v(j), cs)
proof
  induction cs
  | List.nil =>
    rw [polynomialFromHorner.nil, monicValue]
    exact polynomialAtOver.constant with *
  | List.cons(c, tail) using ih =>
    have coefficient : c ∈ R by assumption
    have previous := ih
    have zeroIn : R[0] ∈ R by typecheck
    have oneIn : R[1] ∈ R by typecheck
    have polynomialRing := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *
    have ordinary := IsCommRing.ring with polynomialRing
    have constant := polynomialConstant.member at I, A, zero, c with *
    have variable := polynomialVariable.member at I, A, zero, one, j with *
    have rest := polynomialFromHorner.member at I, A, add, zero, neg, mul, one, j, leading, tail with *
    have product := IsRing.mul_closed with ordinary, variable, rest
    have evaluation := polynomialAtOver.hom with *
    have sumValue := IsRingHom.add with evaluation, constant, product
    have productValue := IsRingHom.mul with evaluation, variable, rest
    have constantValue := polynomialAtOver.constant with coefficient
    have variableValue := polynomialAtOver.variable at I, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, v, j with *
    have expression := polynomialFromHorner.cons at I, A, add, zero, neg, mul, one, j, leading, c, tail with *
    have evaluated := hornerValue.cons at A, f, plus, times, f(leading), v(j), c, tail with *
    cc

theorem polynomialAtOver.from_monic_horner (cs : List(A))
  shows polynomialAtOver(I, R, S, f, v)(polynomialFromHorner(I, R, j, R[1], cs)) =
    monicValue(R, f, S, v(j), cs)
proof
  have initial : R[1] ∈ R by typecheck
  have mappedOne := IsRingHom.one with hom
  have evaluated := polynomialAtOver.from_horner with *
  cc

-- This consumes a proved monic representation; it does not assume one exists.
theorem characteristicPolynomial.horner_annihilates (n : Nat) (M N w k : Set) (cs : List(A))
  requires matrixM : RingMatrix(n, R, M)
  requires matrixN : RingMatrix(n, S, N)
  requires entries : ∀ a ∈ n, ∀ b ∈ n, N[a, b] = f(M[a, b])
  requires eigenvector : LeftEigenvector(n, S, N, v(j), w)
  requires coordinate : k ∈ n
  requires representation : characteristicPolynomial(n, I, R, M, j) = polynomialFromHorner(I, R, j, R[1], cs)
  shows S[monicValue(R, f, S, v(j), cs) * w(k)] = S[0]
proof
  have evaluated := polynomialAtOver.from_monic_horner with *
  have annihilated := characteristicPolynomial.annihilates with *
  cc

end Extensions