Clique-polynomial lower bounds over nonnegative rationals

The coefficient-one clique polynomial can be formed over ℚ≥0 with exactly the same separated support as its natural-coefficient counterpart. The support-only nonnegative-rational Schnorr measure therefore gives the full central-binomial and explicit exponential addition lower bounds for circuits with arbitrary named nonnegative-rational constants, including zero.

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.NNRat.polynomial (vertexCount cliqueSize : ℕ) : MvPolynomial (Fin (vertexCount * vertexCount)) ℚ≥0

Coefficient-one clique polynomial over nonnegative rationals.

Equations

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

@[simp]

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.NNRat.polynomial_support (vertexCount cliqueSize : ℕ) : (polynomial vertexCount cliqueSize).support = cliqueSupport vertexCount cliqueSize

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.NNRat.card_polynomial_support (vertexCount cliqueSize : ℕ) : (polynomial vertexCount cliqueSize).support.card = vertexCount.choose cliqueSize

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.NNRat.circuit_addition_lowerBound_of_support_eq {K : Type u_1} {vertexCount cliqueSize : ℕ} (constant : K → ℚ≥0) (target : MvPolynomial (Fin (vertexCount * vertexCount)) ℚ≥0) (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 nonnegative-rational polynomial with clique support needs one fewer addition than its number of monomials.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.NNRat.circuit_addition_lowerBound {K : Type u_1} {vertexCount cliqueSize : ℕ} (constant : K → ℚ≥0) (circuit : Circuit (Arithmetic.signature K) (vertexCount * vertexCount) 1) (constructs : { inputCount := vertexCount * vertexCount, inputs := MvPolynomial.X, target := polynomial vertexCount cliqueSize }.Constructs circuit (General.polynomialInterpretation constant (Fin (vertexCount * vertexCount)))) : vertexCount.choose cliqueSize - 1 ≤ circuit.cost Arithmetic.additionCost

Addition lower bound for the nonnegative-rational clique polynomial.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.NNRat.central_circuit_addition_lowerBound {K : Type u_1} {halfVertices : ℕ} (constant : K → ℚ≥0) (circuit : Circuit (Arithmetic.signature K) (2 * halfVertices * (2 * halfVertices)) 1) (constructs : { inputCount := 2 * halfVertices * (2 * halfVertices), inputs := MvPolynomial.X, target := polynomial (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 nonnegative rationals.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.NNRat.central_circuit_exponential_lowerBound {K : Type u_1} {halfVertices : ℕ} (constant : K → ℚ≥0) (halfVerticesBig : 4 ≤ halfVertices) (circuit : Circuit (Arithmetic.signature K) (2 * halfVertices * (2 * halfVertices)) 1) (constructs : { inputCount := 2 * halfVertices * (2 * halfVertices), inputs := MvPolynomial.X, target := polynomial (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 nonnegative rationals.