PolynomialHornerBridge
Sparse polynomial evaluation, finite variable dependence, and localization in ZF
1-- Sparse polynomial evaluation, finite variable dependence, and localization in ZF.2-- Part of the Grace17 examples.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module PolynomialHornerBridge8import Grace.Cumulus.Algebra.Polynomial.HornerLocalization9import Grace.Cumulus.Algebra.Polynomial.Variables1011section Sparse12variable (I A add z neg mul one p v w : Set)13notation ring R := (A, add, z, neg, mul, one)14notation ring P := R[I]15hypothesis ring : IsCommRing(R)16hypothesis polynomial : p ∈ P1718theorem finitely_many_variables19 shows Finite(polynomialVariablesUsed(I, R, p))20proof21 exact polynomialVariablesUsed.finite with *2223theorem evaluation_depends_on_used_variables24 requires first : v : I → R25 requires second : w : I → R26 requires agreement : ∀ i ∈ polynomialVariablesUsed(I, R, p), v(i) = w(i)27 shows polynomialAt(I, R, v)(p) = polynomialAt(I, R, w)(p)28proof29 exact polynomialAt.agree_on_variables with *3031end Sparse3233section Horner34variable (I A add z neg mul one j leading : Set)35notation ring R := (A, add, z, neg, mul, one)36notation ring P := R[I]37hypothesis field : IsField(R)38hypothesis initial : leading ∈ R39hypothesis nonzero : leading ≠ R[0]40hypothesis infinite : ¬Finite(R)41hypothesis index : j ∈ I4243theorem nonvanishing (cs : List(A))44 shows ∃ v, FunctionBetween(v, I, R) ∧ polynomialAt(I, R, v)(polynomialFromHorner(I, R, j, leading, cs)) ≠ R[0]45proof46 exact polynomialFromHorner.nonvanishing with *4748end Horner4950section Localizations51variable (I A add z neg mul one B plus o minus times unit g j leading T : Set)52notation ring R := (A, add, z, neg, mul, one)53notation ring P := R[I]54notation ring S := (B, plus, o, minus, times, unit)55notation ring L := S ↾ T56hypothesis coefficients : IsField(R)57hypothesis infinite : ¬Finite(R)58hypothesis initial : leading ∈ R59hypothesis nonzero : leading ≠ R[0]60hypothesis index : j ∈ I61hypothesis target : IsCommRing(S)62hypothesis embedding : IsRingHom(g, P, S)63hypothesis injective : InjectiveBetween(g, P, S)6465theorem not_a_field (cs : List(A))66 requires carrier : T = localizationWithin(S, functionImage(g, P, S), functionImage(g, denominatorPowers(P, polynomialFromHorner(I, R, j, leading, cs)), S))67 shows ¬IsField(L)68proof69 exact polynomialLocalization.not_field_from_horner with *7071end Localizations72