Schnorr closure under weighted monomial substitutions

This strengthens Closure.separationClosure by allowing every source variable to carry an arbitrary natural coefficient. Positive weights merely rescale monomials; a zero weight deletes every source monomial using that variable. The enlarged closure is therefore stable under substitution of all natural constants, including zero.

The closure is still finite because a weighted monomial substitution can only identify or delete source monomials. This file proves the finite bound, its comparison with ordinary Schnorr closure, and the zero-cost product and constant laws. The addition law is developed separately because it is the only step that can create a new support branch.

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.transform {SourceVar : Type u} (weight : SourceVar → ℕ) (basis : SourceVar → ℕ →₀ ℕ) (polynomial : MvPolynomial SourceVar ℕ) : MvPolynomial ℕ ℕ

Apply a natural-weighted monomial substitution into countably many target variables.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Achievable {SourceVar : Type u} (polynomial : MvPolynomial SourceVar ℕ) (score : ℕ) : Prop

A score witnessed after a weighted monomial substitution.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.separationNumber_transform_le_card_sub_one {SourceVar : Type u} (weight : SourceVar → ℕ) (basis : SourceVar → ℕ →₀ ℕ) (polynomial : MvPolynomial SourceVar ℕ) : separationNumber (transform weight basis polynomial).support ≤ polynomial.support.card - 1

Every weighted substitution score is bounded by the original support cardinality minus one.

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.separationClosure {SourceVar : Type u} (polynomial : MvPolynomial SourceVar ℕ) : ℕ

Schnorr's separation measure closed under arbitrary natural-weighted monomial substitutions.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.separationNumber_transform_le_closure {SourceVar : Type u} (weight : SourceVar → ℕ) (basis : SourceVar → ℕ →₀ ℕ) (polynomial : MvPolynomial SourceVar ℕ) : separationNumber (transform weight basis polynomial).support ≤ separationClosure polynomial

Every particular weighted substitution lower-bounds the weighted closure.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.separationClosure_le_card_sub_one {SourceVar : Type u} (polynomial : MvPolynomial SourceVar ℕ) : separationClosure polynomial ≤ polynomial.support.card - 1

Weighted closure retains the finite support-cardinality bound.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.achievable_separationClosure_of_pos {SourceVar : Type u} {polynomial : MvPolynomial SourceVar ℕ} (positive : 0 < separationClosure polynomial) : Achievable polynomial (separationClosure polynomial)

A positive weighted-closure score has an actual substitution witness.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.transform_support_eq_of_support_eq {SourceVar : Type u} (weight : SourceVar → ℕ) (basis : SourceVar → ℕ →₀ ℕ) {left right : MvPolynomial SourceVar ℕ} (supportEqual : left.support = right.support) : (transform weight basis left).support = (transform weight basis right).support

Weighted transformed support depends only on source support.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.separationClosure_eq_of_support_eq {SourceVar : Type u} {left right : MvPolynomial SourceVar ℕ} (supportEqual : left.support = right.support) : separationClosure left = separationClosure right

Weighted Schnorr closure is coefficient-insensitive: polynomials with the same support have exactly the same value.

@[simp]

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.separationClosure_X {variableCount : ℕ} (coordinate : Fin variableCount) : separationClosure (MvPolynomial.X coordinate) = 0

A single variable has zero weighted closure, even though it may be deleted by a zero weight.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.transform_one_eq {SourceVar : Type u} (basis : SourceVar → ℕ →₀ ℕ) (polynomial : MvPolynomial SourceVar ℕ) : transform (fun (x : SourceVar) => 1) basis polynomial = Closure.transform basis polynomial

Unit weights recover the ordinary coefficient-one monomial transform.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.ordinary_separationClosure_le {SourceVar : Type u} (polynomial : MvPolynomial SourceVar ℕ) : Closure.separationClosure polynomial ≤ separationClosure polynomial

Weighted closure dominates Schnorr's ordinary monomial-substitution closure.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.separationNumber_le_closure {variableCount : ℕ} (polynomial : MvPolynomial (Fin variableCount) ℕ) : separationNumber polynomial.support ≤ separationClosure polynomial

In particular, displayed support separation lower-bounds weighted closure on finite circuit-variable sets.

def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.productWeight {variableCount : ℕ} (weight : Fin variableCount → ℕ) (left right : Fin variableCount) : Fin (variableCount + 1) → ℕ

Weight lift for reverse substitution of the newest variable by a product.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.productWeight weight left right i = Fin.lastCases (weight left * weight right) weight i

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.transform_product_eq {variableCount : ℕ} (weight : Fin variableCount → ℕ) (basis : Fin variableCount → ℕ →₀ ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) (left right : Fin variableCount) : transform weight basis ((MvPolynomial.bind₁ fun (i : Fin (variableCount + 1)) => Fin.lastCases (MvPolynomial.X left * MvPolynomial.X right) MvPolynomial.X i) polynomial) = transform (productWeight weight left right) (productLift basis left right) polynomial

Weighted monomial substitution commutes exactly with reverse product substitution.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.product_substitution_le {variableCount : ℕ} (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) (left right : Fin variableCount) : separationClosure ((MvPolynomial.bind₁ fun (i : Fin (variableCount + 1)) => Fin.lastCases (MvPolynomial.X left * MvPolynomial.X right) MvPolynomial.X i) polynomial) ≤ separationClosure polynomial

Product reverse substitution cannot increase weighted Schnorr closure.

def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.constantWeight {variableCount : ℕ} (weight : Fin variableCount → ℕ) (scalar : ℕ) : Fin (variableCount + 1) → ℕ

Weight lift for reverse substitution of the newest variable by an arbitrary natural scalar.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.constantWeight weight scalar i = Fin.lastCases scalar weight i

def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.constantBasis {variableCount : ℕ} (basis : Fin variableCount → ℕ →₀ ℕ) : Fin (variableCount + 1) → ℕ →₀ ℕ

Exponent lift for a scalar, whose monomial exponent is zero.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.constantBasis basis i = Fin.lastCases 0 basis i

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.transform_constant_eq {variableCount : ℕ} (weight : Fin variableCount → ℕ) (basis : Fin variableCount → ℕ →₀ ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) (scalar : ℕ) : transform weight basis ((MvPolynomial.bind₁ fun (i : Fin (variableCount + 1)) => Fin.lastCases (MvPolynomial.C scalar) MvPolynomial.X i) polynomial) = transform (constantWeight weight scalar) (constantBasis basis) polynomial

Weighted monomial substitution commutes exactly with substitution of any natural scalar, including zero.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.constant_substitution_le {variableCount : ℕ} (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) (scalar : ℕ) : separationClosure ((MvPolynomial.bind₁ fun (i : Fin (variableCount + 1)) => Fin.lastCases (MvPolynomial.C scalar) MvPolynomial.X i) polynomial) ≤ separationClosure polynomial

Reverse substitution of every natural scalar, zero included, cannot increase weighted Schnorr closure.