Coefficient semirings with exact polynomial support

Polynomial support is functorial for semirings in which a sum is zero only when both summands are zero and nonzero factors have nonzero product. This module packages the missing zero-sum condition, proves exact support laws for addition, multiplication, and substitution, and supplies cross-coefficient congruence: substitutions over two such semirings have the same support when their source and variable-image supports agree.

Both Nat and the nonnegative rationals satisfy these assumptions. The cross-coefficient theorem is the bridge used to transport natural-coefficient Schnorr combinatorics to nonnegative-rational arithmetic circuits.

class Algebraic.Fusion.Arithmetic.ExactSupport.ZeroSumFree (R : Type u) [Add R] [Zero R] : Prop

A zero-sum-free additive structure: no two nonzero elements cancel.

• add_eq_zero_iff (left right : R) : left + right = 0 ↔ left = 0 ∧ right = 0

instance Algebraic.Fusion.Arithmetic.ExactSupport.instZeroSumFreeNat : ZeroSumFree ℕ

instance Algebraic.Fusion.Arithmetic.ExactSupport.instZeroSumFreeNNRat : ZeroSumFree ℚ≥0

theorem Algebraic.Fusion.Arithmetic.ExactSupport.finset_sum_eq_zero_iff {R : Type u_1} {Index : Type u_2} [AddCommMonoid R] [ZeroSumFree R] (indices : Finset Index) (value : Index → R) : ∑ index ∈ indices, value index = 0 ↔ ∀ index ∈ indices, value index = 0

A finite sum in a zero-sum-free commutative monoid vanishes exactly when every summand vanishes.

theorem Algebraic.Fusion.Arithmetic.ExactSupport.polynomial_support_add {R : Type u_2} [CommSemiring R] [ZeroSumFree R] {Variable : Type u_1} [DecidableEq Variable] (left right : MvPolynomial Variable R) : (left + right).support = left.support ∪ right.support

Exact support of addition over a zero-sum-free coefficient semiring.

theorem Algebraic.Fusion.Arithmetic.ExactSupport.polynomial_support_mul {R : Type u_2} [CommSemiring R] [NoZeroDivisors R] [ZeroSumFree R] {Variable : Type u_1} [DecidableEq Variable] (left right : MvPolynomial Variable R) : (left * right).support = left.support + right.support

Exact support of multiplication over a zero-sum-free semiring without zero divisors.

theorem Algebraic.Fusion.Arithmetic.ExactSupport.support_finset_sum {R : Type u_3} [CommSemiring R] [ZeroSumFree R] {Variable : Type u_1} {Index : Type u_2} [DecidableEq Variable] (indices : Finset Index) (polynomial : Index → MvPolynomial Variable R) : (∑ index ∈ indices, polynomial index).support = indices.biUnion fun (index : Index) => (polynomial index).support

Exact support of a finite polynomial sum.

theorem Algebraic.Fusion.Arithmetic.ExactSupport.support_C_mul_of_ne_zero {R : Type u_2} [CommSemiring R] [NoZeroDivisors R] [ZeroSumFree R] {Variable : Type u_1} [DecidableEq Variable] (coefficient : R) (nonzero : coefficient ≠ 0) (polynomial : MvPolynomial Variable R) : (MvPolynomial.C coefficient * polynomial).support = polynomial.support

Multiplication by a nonzero scalar does not change support.

noncomputable def Algebraic.Fusion.Arithmetic.ExactSupport.monomialExpansion {R : Type u_1} [CommSemiring R] {SourceVar : Type u_2} {TargetVar : Type u_3} (substitution : SourceVar → MvPolynomial TargetVar R) (exponent : SourceVar →₀ ℕ) : MvPolynomial TargetVar R

Expansion of one coefficient-one source monomial under substitution.

Equations

• Algebraic.Fusion.Arithmetic.ExactSupport.monomialExpansion substitution exponent = (MvPolynomial.bind₁ substitution) ((MvPolynomial.monomial exponent) 1)

theorem Algebraic.Fusion.Arithmetic.ExactSupport.support_bind₁_monomial_coeff {R : Type u_3} [CommSemiring R] [NoZeroDivisors R] [ZeroSumFree R] {TargetVar : Type u_1} {SourceVar : Type u_2} [DecidableEq TargetVar] (substitution : SourceVar → MvPolynomial TargetVar R) (polynomial : MvPolynomial SourceVar R) (exponent : SourceVar →₀ ℕ) (present : exponent ∈ polynomial.support) : ((MvPolynomial.bind₁ substitution) ((MvPolynomial.monomial exponent) (polynomial.coeff exponent))).support = (monomialExpansion substitution exponent).support

A supported source coefficient has the same substituted support as its coefficient-one monomial.

theorem Algebraic.Fusion.Arithmetic.ExactSupport.support_bind₁ {R : Type u_3} [CommSemiring R] [NoZeroDivisors R] [ZeroSumFree R] {TargetVar : Type u_1} {SourceVar : Type u_2} [DecidableEq TargetVar] (substitution : SourceVar → MvPolynomial TargetVar R) (polynomial : MvPolynomial SourceVar R) : ((MvPolynomial.bind₁ substitution) polynomial).support = polynomial.support.biUnion fun (exponent : SourceVar →₀ ℕ) => (monomialExpansion substitution exponent).support

Exact support decomposition of a polynomial substitution.

theorem Algebraic.Fusion.Arithmetic.ExactSupport.support_pow_congr {R : Type u_2} {S : Type u_3} [CommSemiring R] [Nontrivial R] [NoZeroDivisors R] [ZeroSumFree R] [CommSemiring S] [Nontrivial S] [NoZeroDivisors S] [ZeroSumFree S] {TargetVar : Type u_1} [DecidableEq TargetVar] (left : MvPolynomial TargetVar R) (right : MvPolynomial TargetVar S) (supportEqual : left.support = right.support) (power : ℕ) : (left ^ power).support = (right ^ power).support

Powers over two exact-support semirings have equal support whenever their bases do.

theorem Algebraic.Fusion.Arithmetic.ExactSupport.support_finset_prod_congr {R : Type u_3} {S : Type u_4} [CommSemiring R] [Nontrivial R] [NoZeroDivisors R] [ZeroSumFree R] [CommSemiring S] [Nontrivial S] [NoZeroDivisors S] [ZeroSumFree S] {TargetVar : Type u_1} {Index : Type u_2} [DecidableEq TargetVar] (indices : Finset Index) (left : Index → MvPolynomial TargetVar R) (right : Index → MvPolynomial TargetVar S) (supportEqual : ∀ index ∈ indices, (left index).support = (right index).support) : (∏ index ∈ indices, left index).support = (∏ index ∈ indices, right index).support

Finite products over two exact-support semirings preserve pointwise support equality.

theorem Algebraic.Fusion.Arithmetic.ExactSupport.support_monomialExpansion_congr {R : Type u_3} {S : Type u_4} [CommSemiring R] [Nontrivial R] [NoZeroDivisors R] [ZeroSumFree R] [CommSemiring S] [Nontrivial S] [NoZeroDivisors S] [ZeroSumFree S] {TargetVar : Type u_1} {SourceVar : Type u_2} [DecidableEq TargetVar] (left : SourceVar → MvPolynomial TargetVar R) (right : SourceVar → MvPolynomial TargetVar S) (supportEqual : ∀ (source : SourceVar), (left source).support = (right source).support) (exponent : SourceVar →₀ ℕ) : (monomialExpansion left exponent).support = (monomialExpansion right exponent).support

Cross-coefficient support congruence for one monomial expansion.

theorem Algebraic.Fusion.Arithmetic.ExactSupport.support_bind₁_congr {R : Type u_3} {S : Type u_4} [CommSemiring R] [Nontrivial R] [NoZeroDivisors R] [ZeroSumFree R] [CommSemiring S] [Nontrivial S] [NoZeroDivisors S] [ZeroSumFree S] {TargetVar : Type u_1} {SourceVar : Type u_2} [DecidableEq TargetVar] (leftSubstitution : SourceVar → MvPolynomial TargetVar R) (rightSubstitution : SourceVar → MvPolynomial TargetVar S) (substitutionSupportEqual : ∀ (source : SourceVar), (leftSubstitution source).support = (rightSubstitution source).support) (leftPolynomial : MvPolynomial SourceVar R) (rightPolynomial : MvPolynomial SourceVar S) (polynomialSupportEqual : leftPolynomial.support = rightPolynomial.support) : ((MvPolynomial.bind₁ leftSubstitution) leftPolynomial).support = ((MvPolynomial.bind₁ rightSubstitution) rightPolynomial).support

Substitution support is independent of the exact-support coefficient semiring when source support and every variable-image support agree.