PolynomialAssignments
Arbitrary variable assignments and certificates excluding common zeros
1-- Arbitrary variable assignments and certificates excluding common zeros.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 PolynomialAssignments8import Grace.Cumulus.Algebra.Polynomial.Assignment910section Evaluation11variable (I A add zero neg mul one v e : Set)12hypothesis coefficients : IsCommRing(A, add, zero, neg, mul, one)13hypothesis assignment : v : I → A14hypothesis evaluation : e = polynomialAt(I, A, add, zero, neg, mul, one, v)15notation ring R := (A, add, zero, neg, mul, one)16notation ring P := R[I]1718theorem evaluate_variable (j : Set)19 requires hj : j ∈ I20 shows e(polynomialVariable(I, A, zero, one, j)) = v(j)21proof22 rw evaluation23 exact polynomialAt.variable at I, A, add, zero, neg, mul, one, v, j with *2425theorem evaluate_product (p q : Set)26 requires hp : p ∈ P27 requires hq : q ∈ P28 shows e(P[p * q]) = R[e(p) * e(q)]29proof30 have hom := polynomialAt.hom at I, A, add, zero, neg, mul, one, v with *31 rw evaluation32 exact IsRingHom.mul with hom, hp, hq3334theorem evaluate_constant (a : Set)35 requires ha : a ∈ R36 shows e(polynomialConstant(I, A, zero, a)) = a37proof38 rw evaluation39 exact polynomialAt.constant at I, A, add, zero, neg, mul, one, v, a with *4041end Evaluation4243section Certificates44variable (I A add zero neg mul one : Set)45hypothesis coefficients : IsCommRing(A, add, zero, neg, mul, one)46hypothesis nontrivial : Nontrivial(A, zero, one)47notation ring R := (A, add, zero, neg, mul, one)48notation ring P := R[I]4950-- This applies to every polynomial p, hence in particular to p = X_j.51-- The certificate 1*p + 1*(1-p) = 1 is discharged by ring automation.52theorem incompatible_equations (p : Set)53 requires hp : p ∈ P54 shows ¬(∃ v, PolynomialCommonZero(I, A, add, zero, neg, mul, one, {p, P[1 - p]}, v))55proof56 have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *57 have ordinary := IsCommRing.ring with source58 have multiplicative := IsRing.multiplicative with ordinary59 have unit := IsMonoid.unit_in_carrier with multiplicative60 have negative := IsRing.neg_closed with ordinary, hp61 have complement := IsRing.add_closed with ordinary, unit, negative62 have generators : {p, P[1 - p]} ⊆ P by settle with Subset, pair.membership63 have first : p ∈ {p, P[1 - p]} by settle with pair.membership64 have second : P[1 - p] ∈ {p, P[1 - p]} by settle with pair.membership65 have identity : P[1 * p + 1 * (1 - p)] = P[1] by ring66 exact polynomialIdeal.no_common_zero_of_combination at I, A, add, zero, neg, mul, one, {p, P[1 - p]}, p, P[1 - p], P[1], P[1] with *6768end Certificates69