Grace/Cumulus/Algebra/Polynomial/HornerExtension.g17

Open in Workbench Download source

Imports

HornerDegree · Characteristic

Declarations

Source

1-- Horner representations evaluated through arbitrary coefficient extensions (ZF).2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.Polynomial.HornerExtension8import HornerDegree9import Characteristic1011section Extensions12variable (I A add zero neg mul one B plus z minus times unit f v j : Set)13notation ring R := (A, add, zero, neg, mul, one)14notation ring S := (B, plus, z, minus, times, unit)15notation ring P := R[I]16hypothesis source : IsCommRing(R)17hypothesis target : IsCommRing(S)18hypothesis hom : IsRingHom(f, R, S)19hypothesis assignment : v : I → S20hypothesis index : j ∈ I2122theorem polynomialAtOver.from_horner (leading : Set) (cs : List(A))23  requires initial : leading ∈ R24  shows polynomialAtOver(I, R, S, f, v)(polynomialFromHorner(I, R, j, leading, cs)) =25    monicValue{A}(f, plus, times, f(leading), v(j), cs)26proof27  induction cs28  | List.nil =>29    rw [polynomialFromHorner.nil, monicValue]30    exact polynomialAtOver.constant with *31  | List.cons(c, tail) using ih =>32    have coefficient : c ∈ R by assumption33    have previous := ih34    have zeroIn : R[0] ∈ R by typecheck35    have oneIn : R[1] ∈ R by typecheck36    have polynomialRing := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *37    have ordinary := IsCommRing.ring with polynomialRing38    have constant := polynomialConstant.member at I, A, zero, c with *39    have variable := polynomialVariable.member at I, A, zero, one, j with *40    have rest := polynomialFromHorner.member at I, A, add, zero, neg, mul, one, j, leading, tail with *41    have product := IsRing.mul_closed with ordinary, variable, rest42    have evaluation := polynomialAtOver.hom with *43    have sumValue := IsRingHom.add with evaluation, constant, product44    have productValue := IsRingHom.mul with evaluation, variable, rest45    have constantValue := polynomialAtOver.constant with coefficient46    have variableValue := polynomialAtOver.variable at I, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, v, j with *47    have expression := polynomialFromHorner.cons at I, A, add, zero, neg, mul, one, j, leading, c, tail with *48    have evaluated := hornerValue.cons at A, f, plus, times, f(leading), v(j), c, tail with *49    cc5051theorem polynomialAtOver.from_monic_horner (cs : List(A))52  shows polynomialAtOver(I, R, S, f, v)(polynomialFromHorner(I, R, j, R[1], cs)) =53    monicValue(R, f, S, v(j), cs)54proof55  have initial : R[1] ∈ R by typecheck56  have mappedOne := IsRingHom.one with hom57  have evaluated := polynomialAtOver.from_horner with *58  cc5960-- This consumes a proved monic representation; it does not assume one exists.61theorem characteristicPolynomial.horner_annihilates (n : Nat) (M N w k : Set) (cs : List(A))62  requires matrixM : RingMatrix(n, R, M)63  requires matrixN : RingMatrix(n, S, N)64  requires entries : ∀ a ∈ n, ∀ b ∈ n, N[a, b] = f(M[a, b])65  requires eigenvector : LeftEigenvector(n, S, N, v(j), w)66  requires coordinate : k ∈ n67  requires representation : characteristicPolynomial(n, I, R, M, j) = polynomialFromHorner(I, R, j, R[1], cs)68  shows S[monicValue(R, f, S, v(j), cs) * w(k)] = S[0]69proof70  have evaluated := polynomialAtOver.from_monic_horner with *71  have annihilated := characteristicPolynomial.annihilates with *72  cc7374end Extensions75