Weighted Schnorr closure over nonnegative-rational coefficients

Weighted Schnorr closure is support-only, so a polynomial over ℚ≥0 receives the closure value of the natural coefficient-one polynomial with the same support. The exact-support interface proves that reverse addition, multiplication, and constant substitution have the same support over ℚ≥0 as over Nat, with a nonzero rational scalar represented by weight one and zero represented by weight zero.

This yields an unconditional addition lower bound for monotone arithmetic circuits over nonnegative-rational polynomials with arbitrary named nonnegative-rational constants.

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.NNRat.canonical {Variable : Type u_1} (polynomial : MvPolynomial Variable ℚ≥0) : MvPolynomial Variable ℕ

Natural coefficient-one representative of a nonnegative-rational polynomial's support.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.NNRat.canonical polynomial = Algebraic.Fusion.Arithmetic.Progress.Separated.Polynomial.ofSupport polynomial.support

@[simp]

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.NNRat.canonical_support {Variable : Type u_1} (polynomial : MvPolynomial Variable ℚ≥0) : (canonical polynomial).support = polynomial.support

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.NNRat.value {Variable : Type u_1} (polynomial : MvPolynomial Variable ℚ≥0) : ℕ

Weighted Schnorr value of a nonnegative-rational polynomial.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.NNRat.value_eq_of_support_eq {Variable : Type u_1} {left right : MvPolynomial Variable ℚ≥0} (supportEqual : left.support = right.support) : value left = value right

The value depends only on monomial support.

@[simp]

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

A single variable has zero nonnegative-rational weighted closure.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.NNRat.add_substitution_support_eq {variableCount : ℕ} (left right : Fin variableCount) (source : Fin (variableCount + 1)) : (Fin.lastCases (MvPolynomial.X left + MvPolynomial.X right) MvPolynomial.X source).support = (Fin.lastCases (MvPolynomial.X left + MvPolynomial.X right) MvPolynomial.X source).support

Reverse-addition variable images have the same support over ℚ≥0 and Nat.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.NNRat.mul_substitution_support_eq {variableCount : ℕ} (left right : Fin variableCount) (source : Fin (variableCount + 1)) : (Fin.lastCases (MvPolynomial.X left * MvPolynomial.X right) MvPolynomial.X source).support = (Fin.lastCases (MvPolynomial.X left * MvPolynomial.X right) MvPolynomial.X source).support

Reverse-product variable images have the same support over ℚ≥0 and Nat.

def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.NNRat.scalarWeight (scalar : ℚ≥0) : ℕ

Natural zero-or-one weight representing whether a nonnegative rational scalar has support.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.NNRat.scalarWeight scalar = if scalar = 0 then 0 else 1

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.NNRat.constant_substitution_support_eq {variableCount : ℕ} (scalar : ℚ≥0) (source : Fin (variableCount + 1)) : (Fin.lastCases (MvPolynomial.C scalar) MvPolynomial.X source).support = (Fin.lastCases (MvPolynomial.C (scalarWeight scalar)) MvPolynomial.X source).support

A rational scalar and its zero-or-one natural representative have the same constant-polynomial support.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.NNRat.add_substitution_le {variableCount : ℕ} (polynomial : MvPolynomial (Fin (variableCount + 1)) ℚ≥0) (left right : Fin variableCount) : value ((MvPolynomial.bind₁ fun (i : Fin (variableCount + 1)) => Fin.lastCases (MvPolynomial.X left + MvPolynomial.X right) MvPolynomial.X i) polynomial) ≤ value polynomial + 1

Reverse addition grows the nonnegative-rational weighted value by at most one.

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

Reverse multiplication cannot increase the nonnegative-rational weighted value.

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

Substitution of any nonnegative-rational scalar, zero included, cannot increase the weighted value.

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.NNRat.measure {K : Type u_1} (constant : K → ℚ≥0) : General.Measure constant Arithmetic.additionCost

Weighted Schnorr closure as an addition-cost progress measure over nonnegative-rational coefficients.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.NNRat.separationNumber_le_value {variableCount : ℕ} (polynomial : MvPolynomial (Fin variableCount) ℚ≥0) : separationNumber polynomial.support ≤ value polynomial

Ordinary support separation is bounded by the nonnegative-rational weighted value.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.NNRat.circuit_addition_lowerBound {K : Type u_1} {n : ℕ} (constant : K → ℚ≥0) (target : MvPolynomial (Fin n) ℚ≥0) (circuit : Circuit (Arithmetic.signature K) n 1) (constructs : { inputCount := n, inputs := MvPolynomial.X, target := target }.Constructs circuit (General.polynomialInterpretation constant (Fin n))) : value target ≤ circuit.cost Arithmetic.additionCost

Weighted Schnorr closure lower-bounds additions in monotone nonnegative-rational arithmetic circuits with arbitrary named constants.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.NNRat.circuit_addition_lowerBound_of_separationNumber {K : Type u_1} {n : ℕ} (constant : K → ℚ≥0) (target : MvPolynomial (Fin n) ℚ≥0) (circuit : Circuit (Arithmetic.signature K) n 1) (constructs : { inputCount := n, inputs := MvPolynomial.X, target := target }.Constructs circuit (General.polynomialInterpretation constant (Fin n))) : separationNumber target.support ≤ circuit.cost Arithmetic.additionCost

Ordinary support separation remains an addition lower bound over nonnegative-rational coefficients.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.NNRat.circuit_addition_lowerBound_of_isSeparated {K : Type u_1} {n : ℕ} (constant : K → ℚ≥0) (target : MvPolynomial (Fin n) ℚ≥0) (targetSeparated : IsSeparated target.support target.support) (circuit : Circuit (Arithmetic.signature K) n 1) (constructs : { inputCount := n, inputs := MvPolynomial.X, target := target }.Constructs circuit (General.polynomialInterpretation constant (Fin n))) : target.support.card - 1 ≤ circuit.cost Arithmetic.additionCost

Full-support Schnorr theorem over nonnegative-rational coefficients.