Documentation

Complexitylib.Algebraic.LowerBound.Fusion.Arithmetic.Progress.Separated.Closure.PositiveConstants

Schnorr closure with positive named constants #

Positive scalar constants change coefficients but do not delete support. After an arbitrary monomial substitution, replacing the newest variable by a positive scalar is a positive weighted monomial substitution: the newest variable has exponent image zero and scalar weight, while every prior variable keeps its monomial image and unit weight.

The weighted-substitution support theorem therefore proves that constant reverse substitution cannot increase Schnorr's closure. Combined with the existing addition and product laws, this gives the classical coefficient-insensitive addition lower bound for monotone arithmetic circuits with arbitrary positive natural constants.

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

Weights realizing substitution of the newest variable by scalar and leaving all previous monomial substitutions coefficient-one.

Equations
Instances For
    source
    theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.PositiveConstants.constantWeight_pos {variableCount scalar : ℕ} (positive : 0 < scalar) (source : Fin (variableCount + 1)) :
    0 < constantWeight scalar source

    Every weight in constantWeight is positive when the scalar is.

    source
    theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.PositiveConstants.transform_reverse_constant_eq_weighted {variableCount : ℕ} (basis : Fin variableCount → ℕ →₀ ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) (scalar : ℕ) :
    transform basis ((MvPolynomial.bind₁ fun (i : Fin (variableCount + 1)) => Fin.lastCases (MvPolynomial.C scalar) MvPolynomial.X i) polynomial) = WeightedMonomialSubstitution.transform (constantWeight scalar) (Addition.endpointBasis basis 0) polynomial

    Applying an arbitrary target monomial substitution after reverse substitution of a scalar is exactly a weighted monomial substitution of the original polynomial.

    source
    theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.PositiveConstants.support_transform_reverse_constant {variableCount : ℕ} (basis : Fin variableCount → ℕ →₀ ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) (scalar : ℕ) (positive : 0 < scalar) :
    (transform basis ((MvPolynomial.bind₁ fun (i : Fin (variableCount + 1)) => Fin.lastCases (MvPolynomial.C scalar) MvPolynomial.X i) polynomial)).support = (transform (Addition.endpointBasis basis 0) polynomial).support

    A positive scalar reverse substitution has the same transformed support as sending the eliminated variable to the coefficient-one constant monomial.

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

    Reverse substitution of a positive scalar cannot increase Schnorr's substitution-closed separation number.

    source
    noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.PositiveConstants.measure {K : Type u_1} (constant : K → ℕ) (positive : ∀ (scalar : K), 0 < constant scalar) :
    General.Measure constant Arithmetic.additionCost

    Schnorr closure as an addition-cost progress measure for a chosen positive natural interpretation of named constants.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.PositiveConstants.circuit_addition_lowerBound {K : Type u_1} {n : ℕ} (constant : K → ℕ) (positive : ∀ (scalar : K), 0 < constant scalar) (target : MvPolynomial (Fin n) ℕ) (circuit : Circuit (Arithmetic.signature K) n 1) (constructs : { inputCount := n, inputs := MvPolynomial.X, target := target }.Constructs circuit (General.polynomialInterpretation constant (Fin n))) :
      separationClosure target ≤ circuit.cost Arithmetic.additionCost

      Coefficient-insensitive Schnorr closure lower-bounds additions in every monotone arithmetic circuit whose named constants are positive naturals.

      source
      theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.PositiveConstants.circuit_addition_lowerBound_of_separationNumber {K : Type u_1} {n : ℕ} (constant : K → ℕ) (positive : ∀ (scalar : K), 0 < constant scalar) (target : MvPolynomial (Fin n) ℕ) (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 in the presence of positive named constants.

      source
      theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.PositiveConstants.circuit_addition_lowerBound_of_isSeparated {K : Type u_1} {n : ℕ} (constant : K → ℕ) (positive : ∀ (scalar : K), 0 < constant scalar) (target : MvPolynomial (Fin n) ℕ) (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

      Schnorr's full-support form with arbitrary positive natural constants.