Documentation

Complexitylib.Algebraic.LowerBound.Fusion.Arithmetic.Progress.Separated.Clique.Exact

Clique-polynomial bounds over exact-support semirings #

The coefficient-one clique polynomial and its addition lower bounds are uniform over every nontrivial zero-sum-free commutative semiring without zero divisors. This single family specializes to natural and nonnegative-rational coefficients and remains compatible with arbitrary named constants, including zero.

source
noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.Exact.polynomial (R : Type u) [CommSemiring R] (vertexCount cliqueSize : ℕ) :
MvPolynomial (Fin (vertexCount * vertexCount)) R

Coefficient-one clique polynomial over a selected commutative semiring.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.Exact.polynomial_support (R : Type u) [CommSemiring R] [Nontrivial R] [ExactSupport.ZeroSumFree R] (vertexCount cliqueSize : ℕ) :
    (polynomial R vertexCount cliqueSize).support = cliqueSupport vertexCount cliqueSize
    source
    theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.Exact.card_polynomial_support (R : Type u) [CommSemiring R] [Nontrivial R] [ExactSupport.ZeroSumFree R] (vertexCount cliqueSize : ℕ) :
    (polynomial R vertexCount cliqueSize).support.card = vertexCount.choose cliqueSize
    source
    theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.Exact.circuit_addition_lowerBound_of_support_eq {R : Type u_2} [CommSemiring R] [Nontrivial R] [NoZeroDivisors R] [ExactSupport.ZeroSumFree R] {K : Type u_1} {vertexCount cliqueSize : ℕ} (constant : K → R) (target : MvPolynomial (Fin (vertexCount * vertexCount)) R) (supportEqual : target.support = cliqueSupport vertexCount cliqueSize) (circuit : Circuit (Arithmetic.signature K) (vertexCount * vertexCount) 1) (constructs : { inputCount := vertexCount * vertexCount, inputs := MvPolynomial.X, target := target }.Constructs circuit (General.polynomialInterpretation constant (Fin (vertexCount * vertexCount)))) :
    vertexCount.choose cliqueSize - 1 ≤ circuit.cost Arithmetic.additionCost

    Every polynomial with clique support needs one fewer addition than its number of monomials over any exact-support coefficient semiring.

    source
    theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.Exact.circuit_addition_lowerBound {R : Type u_2} [CommSemiring R] [Nontrivial R] [NoZeroDivisors R] [ExactSupport.ZeroSumFree R] {K : Type u_1} {vertexCount cliqueSize : ℕ} (constant : K → R) (circuit : Circuit (Arithmetic.signature K) (vertexCount * vertexCount) 1) (constructs : { inputCount := vertexCount * vertexCount, inputs := MvPolynomial.X, target := polynomial R vertexCount cliqueSize }.Constructs circuit (General.polynomialInterpretation constant (Fin (vertexCount * vertexCount)))) :
    vertexCount.choose cliqueSize - 1 ≤ circuit.cost Arithmetic.additionCost

    Addition lower bound for the exact-semiring clique polynomial.

    source
    theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.Exact.central_circuit_addition_lowerBound {R : Type u_2} [CommSemiring R] [Nontrivial R] [NoZeroDivisors R] [ExactSupport.ZeroSumFree R] {K : Type u_1} {halfVertices : ℕ} (constant : K → R) (circuit : Circuit (Arithmetic.signature K) (2 * halfVertices * (2 * halfVertices)) 1) (constructs : { inputCount := 2 * halfVertices * (2 * halfVertices), inputs := MvPolynomial.X, target := polynomial R (2 * halfVertices) halfVertices }.Constructs circuit (General.polynomialInterpretation constant (Fin (2 * halfVertices * (2 * halfVertices))))) :
    halfVertices.centralBinom - 1 ≤ circuit.cost Arithmetic.additionCost

    Central-binomial addition lower bound over every exact-support semiring.

    source
    theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.Exact.central_circuit_exponential_lowerBound {R : Type u_2} [CommSemiring R] [Nontrivial R] [NoZeroDivisors R] [ExactSupport.ZeroSumFree R] {K : Type u_1} {halfVertices : ℕ} (constant : K → R) (halfVerticesBig : 4 ≤ halfVertices) (circuit : Circuit (Arithmetic.signature K) (2 * halfVertices * (2 * halfVertices)) 1) (constructs : { inputCount := 2 * halfVertices * (2 * halfVertices), inputs := MvPolynomial.X, target := polynomial R (2 * halfVertices) halfVertices }.Constructs circuit (General.polynomialInterpretation constant (Fin (2 * halfVertices * (2 * halfVertices))))) :
    4 ^ halfVertices < halfVertices * (circuit.cost Arithmetic.additionCost + 1)

    Explicit exponential middle-layer lower bound over every exact-support semiring.