Total-gate bounds for clique polynomials

Schnorr separation controls additions in a clique-polynomial circuit. Exact support Fusion independently controls multiplications when the supports at multiplication inputs have bounded width. This module proves the elementary support side conditions for clique monomials and combines both certificates into a single lower bound on all nonconstant arithmetic gates.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.cliqueExponent_sum {vertexCount : ℕ} (vertices : Finset (Fin vertexCount)) : ((cliqueExponent vertices).sum fun (x : Fin (vertexCount * vertexCount)) (multiplicity : ℕ) => multiplicity) = vertices.card * vertices.card

Total degree of an ordered-clique exponent. Loops are included, so a clique on k vertices has degree k * k.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.zero_not_mem_cliqueSupport {cliqueSize vertexCount : ℕ} (positive : 0 < cliqueSize) : 0 ∉ cliqueSupport vertexCount cliqueSize

A positive-size clique support contains no constant exponent.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.cliqueSupport_disjoint_single {cliqueSize vertexCount : ℕ} (two_le : 2 ≤ cliqueSize) (coordinate : Fin (vertexCount * vertexCount)) : Disjoint (cliqueSupport vertexCount cliqueSize) {Finsupp.single coordinate 1}

For clique size at least two, no clique exponent is the exponent of one input variable.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.Exact.zero_not_mem_polynomial_support {R : Type u_1} [CommSemiring R] [Nontrivial R] [ExactSupport.ZeroSumFree R] {cliqueSize vertexCount : ℕ} (positive : 0 < cliqueSize) : 0 ∉ (polynomial R vertexCount cliqueSize).support

A positive-size exact-semiring clique polynomial has no constant monomial.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.Exact.polynomial_support_disjoint_X {R : Type u_1} [CommSemiring R] [Nontrivial R] [ExactSupport.ZeroSumFree R] {cliqueSize vertexCount : ℕ} (two_le : 2 ≤ cliqueSize) (coordinate : Fin (vertexCount * vertexCount)) : Disjoint (polynomial R vertexCount cliqueSize).support (MvPolynomial.X coordinate).support

When the clique size is at least two, the target support is disjoint from every individual input-variable support.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.Exact.circuit_multiplication_lowerBound {R : Type u_2} [CommSemiring R] [Nontrivial R] [NoZeroDivisors R] [ExactSupport.ZeroSumFree R] {K : Type u_1} {cliqueSize vertexCount : ℕ} (constant : K → R) (two_le : 2 ≤ cliqueSize) (width : ℕ) (positiveWidth : 0 < width) (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)))) (widthBound : MonotonePolynomial.Exact.MultiplicationSupportWidthAtMost constant circuit MvPolynomial.X width) : vertexCount.choose cliqueSize ⌈/⌉ (width * width) ≤ circuit.cost Arithmetic.multiplicationCost

Exact-support Fusion gives a multiplication lower bound for the clique polynomial under the circuit-local support-width promise.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.Exact.circuit_gate_lowerBound {R : Type u_2} [CommSemiring R] [Nontrivial R] [NoZeroDivisors R] [ExactSupport.ZeroSumFree R] {K : Type u_1} {cliqueSize vertexCount : ℕ} (constant : K → R) (two_le : 2 ≤ cliqueSize) (width : ℕ) (positiveWidth : 0 < width) (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)))) (widthBound : MonotonePolynomial.Exact.MultiplicationSupportWidthAtMost constant circuit MvPolynomial.X width) : vertexCount.choose cliqueSize - 1 + vertexCount.choose cliqueSize ⌈/⌉ (width * width) ≤ circuit.cost Arithmetic.gateCost

Addition and multiplication Fusion certificates combine into one lower bound for all nonconstant gates in a clique-polynomial circuit.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.Exact.circuit_size_lowerBound {R : Type u_2} [CommSemiring R] [Nontrivial R] [NoZeroDivisors R] [ExactSupport.ZeroSumFree R] {K : Type u_1} {cliqueSize vertexCount : ℕ} (constant : K → R) (two_le : 2 ≤ cliqueSize) (width : ℕ) (positiveWidth : 0 < width) (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)))) (widthBound : MonotonePolynomial.Exact.MultiplicationSupportWidthAtMost constant circuit MvPolynomial.X width) : vertexCount.choose cliqueSize - 1 + vertexCount.choose cliqueSize ⌈/⌉ (width * width) ≤ circuit.size

The combined lower bound also applies to raw circuit size, which may additionally count scalar-constant gates.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.Exact.central_circuit_gate_lowerBound {R : Type u_2} [CommSemiring R] [Nontrivial R] [NoZeroDivisors R] [ExactSupport.ZeroSumFree R] {K : Type u_1} (constant : K → R) (halfVertices : ℕ) (two_le : 2 ≤ halfVertices) (width : ℕ) (positiveWidth : 0 < width) (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))))) (widthBound : MonotonePolynomial.Exact.MultiplicationSupportWidthAtMost constant circuit MvPolynomial.X width) : halfVertices.centralBinom - 1 + halfVertices.centralBinom ⌈/⌉ (width * width) ≤ circuit.cost Arithmetic.gateCost

Middle-layer specialization of the combined total-gate lower bound.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.Exact.central_four_pow_lt_mul_width_sq_gateCost {R : Type u_2} [CommSemiring R] [Nontrivial R] [NoZeroDivisors R] [ExactSupport.ZeroSumFree R] {K : Type u_1} (constant : K → R) (halfVertices : ℕ) (halfVerticesBig : 4 ≤ halfVertices) (width : ℕ) (positiveWidth : 0 < width) (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))))) (widthBound : MonotonePolynomial.Exact.MultiplicationSupportWidthAtMost constant circuit MvPolynomial.X width) : 4 ^ halfVertices < halfVertices * (width * width * circuit.cost Arithmetic.gateCost)

The middle-layer clique family yields an explicit exponential support-width versus total-gate tradeoff.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.Exact.central_four_pow_lt_mul_width_sq_size {R : Type u_2} [CommSemiring R] [Nontrivial R] [NoZeroDivisors R] [ExactSupport.ZeroSumFree R] {K : Type u_1} (constant : K → R) (halfVertices : ℕ) (halfVerticesBig : 4 ≤ halfVertices) (width : ℕ) (positiveWidth : 0 < width) (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))))) (widthBound : MonotonePolynomial.Exact.MultiplicationSupportWidthAtMost constant circuit MvPolynomial.X width) : 4 ^ halfVertices < halfVertices * (width * width * circuit.size)

Raw circuit size satisfies the same exponential support-width tradeoff.