PolynomialVariableCoefficients

An arbitrary sparse polynomial, viewed coefficientwise in one chosen variable

Open in Workbench View on GitHub

1-- An arbitrary sparse polynomial, viewed coefficientwise in one chosen variable.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 PolynomialVariableCoefficients8import Grace.Cumulus.Algebra.Polynomial.VariableExpansion910section Coefficients11variable (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 ∈ P1617theorem ring_constants18  shows R[0] ∈ R ∧ R[1] ∈ R19proof20  constructor21  . typecheck22  . typecheck2324theorem coefficient_is_polynomial (n : Nat)25  shows polynomialVariableCoefficient(I, R, p, j, n) ∈ P26proof27  have zeroIn : R[0] ∈ R by typecheck28  exact polynomialVariableCoefficient.member with *2930theorem coefficient_uses_fewer_variables (n : Nat)31  shows polynomialVariablesUsed(I, R, polynomialVariableCoefficient(I, R, p, j, n)) ⊆ polynomialVariablesUsed(I, R, p) ∖ {j}32proof33  have zeroIn : R[0] ∈ R by typecheck34  exact polynomialVariableCoefficient.variables with *3536theorem coefficients_determine_polynomial (q : Set)37  requires other : q ∈ P38  requires index : j ∈ I39  requires coefficients : ∀ n ∈ ℕ, polynomialVariableCoefficient(I, R, p, j, n) = polynomialVariableCoefficient(I, R, q, j, n)40  shows p = q41proof42  have zeroIn : R[0] ∈ R by typecheck43  exact polynomialVariableCoefficient.ext with *4445theorem nonzero_coefficient46  requires index : j ∈ I47  requires nonzero : p ≠ P[0]48  shows ∃ n ∈ ℕ, polynomialVariableCoefficient(I, R, p, j, n) ≠ P[0]49proof50  have zeroIn : R[0] ∈ R by typecheck51  exact polynomialVariableCoefficient.exists_nonzero with *5253theorem finitely_many_coefficients54  requires index : j ∈ I55  shows CoefficientMap(polynomialCoefficientFamily(I, R, p, j), ℕ, P, P[0])56proof57  have zeroIn : R[0] ∈ R by typecheck58  exact polynomialCoefficientFamily.map with *5960theorem coefficient_evaluation_ignores_chosen_variable (v w : Set, n : Nat)61  requires first : v : I → R62  requires second : w : I → R63  requires agreement : ∀ i ∈ I, i ≠ j → v(i) = w(i)64  shows polynomialAt(I, R, v)(polynomialVariableCoefficient(I, R, p, j, n)) = polynomialAt(I, R, w)(polynomialVariableCoefficient(I, R, p, j, n))65proof66  exact polynomialVariableCoefficient.agree_away with *6768end Coefficients69