Documentation

Complexitylib.Algebraic.LowerBound.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Exact

Weighted Schnorr closure over exact-support coefficient semirings #

For any zero-sum-free commutative semiring without zero divisors, polynomial support obeys the same addition, multiplication, and substitution rules as it does over Nat. We therefore assign a polynomial the weighted Schnorr value of the natural coefficient-one polynomial with the same support and transport all local enrichment laws across the cross-coefficient support theorem.

This gives one reusable addition lower-bound theorem for arbitrary named constants over every exact-support coefficient semiring. Nat and ℚ≥0 are canonical instances.

source
noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Exact.canonical {R : Type u_1} [CommSemiring R] {Variable : Type u_2} (polynomial : MvPolynomial Variable R) :
MvPolynomial Variable ℕ

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

Equations
Instances For
    source
    @[simp]
    theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Exact.canonical_support {R : Type u_2} [CommSemiring R] {Variable : Type u_1} (polynomial : MvPolynomial Variable R) :
    (canonical polynomial).support = polynomial.support
    source
    noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Exact.value {R : Type u_1} [CommSemiring R] {Variable : Type u_2} (polynomial : MvPolynomial Variable R) :
    ℕ

    Weighted Schnorr value transported through monomial support.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Exact.value_eq_of_support_eq {R : Type u_2} [CommSemiring R] {Variable : Type u_1} {left right : MvPolynomial Variable R} (supportEqual : left.support = right.support) :
      value left = value right

      The transported value depends only on support.

      source
      @[simp]
      theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Exact.value_X {R : Type u_1} [CommSemiring R] [Nontrivial R] {variableCount : ℕ} (coordinate : Fin variableCount) :
      value (MvPolynomial.X coordinate) = 0

      A single variable has zero transported value.

      source
      theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Exact.add_substitution_support_eq {R : Type u_1} [CommSemiring R] [Nontrivial R] [ExactSupport.ZeroSumFree R] {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 R and Nat.

      source
      theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Exact.mul_substitution_support_eq {R : Type u_1} [CommSemiring R] [Nontrivial R] [NoZeroDivisors R] [ExactSupport.ZeroSumFree R] {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 R and Nat.

      source
      noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Exact.scalarWeight {R : Type u_1} [CommSemiring R] (scalar : R) :
      ℕ

      Natural zero-or-one weight recording whether a scalar is nonzero.

      Equations
      Instances For
        source
        theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Exact.constant_substitution_support_eq {R : Type u_1} [CommSemiring R] [Nontrivial R] {variableCount : ℕ} (scalar : R) (source : Fin (variableCount + 1)) :
        (Fin.lastCases (MvPolynomial.C scalar) MvPolynomial.X source).support = (Fin.lastCases (MvPolynomial.C (scalarWeight scalar)) MvPolynomial.X source).support

        A scalar and its zero-or-one natural representative have equal constant support.

        source
        theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Exact.add_substitution_le {R : Type u_1} [CommSemiring R] [Nontrivial R] [NoZeroDivisors R] [ExactSupport.ZeroSumFree R] {variableCount : ℕ} (polynomial : MvPolynomial (Fin (variableCount + 1)) R) (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 transported weighted value by at most one.

        source
        theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Exact.mul_substitution_le {R : Type u_1} [CommSemiring R] [Nontrivial R] [NoZeroDivisors R] [ExactSupport.ZeroSumFree R] {variableCount : ℕ} (polynomial : MvPolynomial (Fin (variableCount + 1)) R) (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 transported weighted value.

        source
        theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Exact.constant_substitution_le {R : Type u_1} [CommSemiring R] [Nontrivial R] [NoZeroDivisors R] [ExactSupport.ZeroSumFree R] {variableCount : ℕ} (polynomial : MvPolynomial (Fin (variableCount + 1)) R) (scalar : R) :
        value ((MvPolynomial.bind₁ fun (i : Fin (variableCount + 1)) => Fin.lastCases (MvPolynomial.C scalar) MvPolynomial.X i) polynomial) ≤ value polynomial

        Substitution of any scalar, zero included, cannot increase the transported weighted value.

        source
        noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Exact.measure {R : Type u_1} [CommSemiring R] [Nontrivial R] [NoZeroDivisors R] [ExactSupport.ZeroSumFree R] {K : Type u_2} (constant : K → R) :
        General.Measure constant Arithmetic.additionCost

        Weighted Schnorr closure as an addition-cost progress measure over an exact-support coefficient semiring.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Exact.separationNumber_le_value {R : Type u_1} [CommSemiring R] {variableCount : ℕ} (polynomial : MvPolynomial (Fin variableCount) R) :
          separationNumber polynomial.support ≤ value polynomial

          Ordinary support separation is bounded by the transported value.

          source
          theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Exact.circuit_addition_lowerBound {R : Type u_2} [CommSemiring R] [Nontrivial R] [NoZeroDivisors R] [ExactSupport.ZeroSumFree R] {K : Type u_1} {n : ℕ} (constant : K → R) (target : MvPolynomial (Fin n) R) (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 over every exact-support coefficient semiring.

          source
          theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Exact.circuit_addition_lowerBound_of_separationNumber {R : Type u_2} [CommSemiring R] [Nontrivial R] [NoZeroDivisors R] [ExactSupport.ZeroSumFree R] {K : Type u_1} {n : ℕ} (constant : K → R) (target : MvPolynomial (Fin n) R) (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 is an addition lower bound over every exact-support coefficient semiring.

          source
          theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Exact.circuit_addition_lowerBound_of_isSeparated {R : Type u_2} [CommSemiring R] [Nontrivial R] [NoZeroDivisors R] [ExactSupport.ZeroSumFree R] {K : Type u_1} {n : ℕ} (constant : K → R) (target : MvPolynomial (Fin n) R) (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 every exact-support coefficient semiring.