PolynomialReconstruction

Sparse polynomial reconstruction and evaluation from extracted coefficients

Open in Workbench View on GitHub

1-- Sparse polynomial reconstruction and evaluation from extracted coefficients.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 PolynomialReconstruction8import Grace.Cumulus.Algebra.Polynomial.HornerReconstruction910section Polynomials11variable (I A add z neg mul one p j : Set)12notation ring R := (A, add, z, neg, mul, one)13notation ring P := R[I]14hypothesis ring : IsCommRing(R)15hypothesis polynomial : p ∈ P16hypothesis index : j ∈ I1718theorem representation19  shows ∃ cs, List(P, cs) ∧ coefficientsOmitVariable(I, A, z, j, cs) ∧ polynomialFromCoefficients(I, R, j, cs) = p20proof21  exact polynomials.exists_coefficient_horner with *2223theorem reconstruction (cs : List(P))24  requires coefficients : ∀ n, Nat(n) → listCoefficient{P}(P[0], cs, n) = polynomialVariableCoefficient(I, R, p, j, n)25  shows polynomialFromCoefficients(I, R, j, cs) = p26proof27  exact polynomialFromCoefficients.reconstruct with *2829theorem nonzero_representation30  requires nonzero : p ≠ P[0]31  shows ∃ cs, List(P, cs) ∧ coefficientsOmitVariable(I, A, z, j, cs) ∧ polynomialFromCoefficients(I, R, j, cs) = p ∧ (∃ n ∈ ℕ, listCoefficient{P}(P[0], cs, n) ≠ P[0])32proof33  exact polynomials.exists_nonzero_coefficient_horner with *3435theorem evaluation (v : Set) (cs : List(P))36  requires assignment : v : I → R37  requires coefficients : ∀ n, Nat(n) → listCoefficient{P}(P[0], cs, n) = polynomialVariableCoefficient(I, R, p, j, n)38  shows polynomialAt(I, R, v)(p) = hornerAt{A}(add, mul, z, v(j), listMap{P}(polynomialAt(I, R, v), cs))39proof40  exact polynomialAt.reconstruction with *4142end Polynomials43