Schnorr's clique-polynomial addition lower bound

For a k-element vertex set S, its clique monomial contains every ordered edge in S × S (including diagonal variables). The family of all such monomials is separated: if C × C is contained in (A × A) ∪ (B × B) and all three vertex sets have the same cardinality, then C = A or C = B.

Combining this finite combinatorics with Schnorr's substitution-closed separation measure proves that every polynomial with this support needs at least Nat.choose n k - 1 addition gates in every constant-free monotone arithmetic circuit. Taking a middle layer gives the classical exponential family over n² variables.

def Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.edgeEmbedding (vertexCount : ℕ) : Fin vertexCount × Fin vertexCount ↪ Fin (vertexCount * vertexCount)

Encode an ordered pair of vertices as one of n² circuit inputs.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.edgeEmbedding vertexCount = finProdFinEquiv.toEmbedding

def Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.edgeSet {vertexCount : ℕ} (vertices : Finset (Fin vertexCount)) : Finset (Fin (vertexCount * vertexCount))

Ordered edges induced by a finite vertex set, represented in the flattened Fin (n²) input space.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.edgeSet vertices = Finset.map (Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.edgeEmbedding vertexCount) (vertices ×ˢ vertices)

@[simp]

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.encoded_edge_mem_edgeSet {vertexCount : ℕ} (vertices : Finset (Fin vertexCount)) (left right : Fin vertexCount) : (edgeEmbedding vertexCount) (left, right) ∈ edgeSet vertices ↔ left ∈ vertices ∧ right ∈ vertices

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.cliqueExponent {vertexCount : ℕ} (vertices : Finset (Fin vertexCount)) : Fin (vertexCount * vertexCount) →₀ ℕ

Characteristic exponent vector of the ordered clique on vertices.

Equations

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

@[simp]

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.cliqueExponent_encoded_edge {vertexCount : ℕ} (vertices : Finset (Fin vertexCount)) (left right : Fin vertexCount) : (cliqueExponent vertices) ((edgeEmbedding vertexCount) (left, right)) = if left ∈ vertices ∧ right ∈ vertices then 1 else 0

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.cliqueExponent_injective {vertexCount : ℕ} : Function.Injective cliqueExponent

The diagonal coordinates recover the underlying vertex set.

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.cliqueExponentEmbedding (vertexCount : ℕ) : Finset (Fin vertexCount) ↪ Fin (vertexCount * vertexCount) →₀ ℕ

Embedding used to form the finite support of the clique polynomial.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.cliqueExponentEmbedding vertexCount = { toFun := Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.cliqueExponent, inj' := ⋯ }

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.cliqueSupport (vertexCount cliqueSize : ℕ) : Finset (Fin (vertexCount * vertexCount) →₀ ℕ)

The exponent support of the k-clique polynomial on vertexCount vertices.

Equations

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

@[simp]

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.card_cliqueSupport (vertexCount cliqueSize : ℕ) : (cliqueSupport vertexCount cliqueSize).card = vertexCount.choose cliqueSize

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.vertices_eq_left_or_right_of_cliqueExponent_le {vertexCount cliqueSize : ℕ} {left right middle : Finset (Fin vertexCount)} (leftCard : left.card = cliqueSize) (rightCard : right.card = cliqueSize) (middleCard : middle.card = cliqueSize) (divides : cliqueExponent middle ≤ cliqueExponent left + cliqueExponent right) : middle = left ∨ middle = right

Equal-size clique exponent vectors satisfy Schnorr separation.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.cliqueSupport_isSeparated (vertexCount cliqueSize : ℕ) : IsSeparated (cliqueSupport vertexCount cliqueSize) (cliqueSupport vertexCount cliqueSize)

All k-clique monomials form a separated family.

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

Schnorr's coefficient-one k-clique polynomial on ordered edge variables.

Equations

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

@[simp]

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

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

The clique polynomial has exactly choose vertexCount cliqueSize monomials.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.circuit_addition_lowerBound_of_support_eq {vertexCount cliqueSize : ℕ} (target : MvPolynomial (Fin (vertexCount * vertexCount)) ℕ) (supportEqual : target.support = cliqueSupport vertexCount cliqueSize) (circuit : Circuit (Arithmetic.signature PEmpty.{u_1 + 1}) (vertexCount * vertexCount) 1) (constructs : { inputCount := vertexCount * vertexCount, inputs := MvPolynomial.X, target := target }.Constructs circuit (polynomialInterpretation (Fin (vertexCount * vertexCount)))) : vertexCount.choose cliqueSize - 1 ≤ circuit.cost Arithmetic.additionCost

Every polynomial with exactly the clique-monomial support needs choose vertexCount cliqueSize - 1 additions, independently of its positive coefficients.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.circuit_addition_lowerBound {vertexCount cliqueSize : ℕ} (circuit : Circuit (Arithmetic.signature PEmpty.{u_1 + 1}) (vertexCount * vertexCount) 1) (constructs : { inputCount := vertexCount * vertexCount, inputs := MvPolynomial.X, target := polynomial vertexCount cliqueSize }.Constructs circuit (polynomialInterpretation (Fin (vertexCount * vertexCount)))) : vertexCount.choose cliqueSize - 1 ≤ circuit.cost Arithmetic.additionCost

Schnorr's addition lower bound for the clique polynomial.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.central_circuit_addition_lowerBound {halfVertices : ℕ} (circuit : Circuit (Arithmetic.signature PEmpty.{u_1 + 1}) (2 * halfVertices * (2 * halfVertices)) 1) (constructs : { inputCount := 2 * halfVertices * (2 * halfVertices), inputs := MvPolynomial.X, target := polynomial (2 * halfVertices) halfVertices }.Constructs circuit (polynomialInterpretation (Fin (2 * halfVertices * (2 * halfVertices))))) : halfVertices.centralBinom - 1 ≤ circuit.cost Arithmetic.additionCost

Middle-layer clique polynomials pay the central binomial coefficient, minus one, in additions.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.central_circuit_exponential_lowerBound {halfVertices : ℕ} (halfVerticesBig : 4 ≤ halfVertices) (circuit : Circuit (Arithmetic.signature PEmpty.{u_1 + 1}) (2 * halfVertices * (2 * halfVertices)) 1) (constructs : { inputCount := 2 * halfVertices * (2 * halfVertices), inputs := MvPolynomial.X, target := polynomial (2 * halfVertices) halfVertices }.Constructs circuit (polynomialInterpretation (Fin (2 * halfVertices * (2 * halfVertices))))) : 4 ^ halfVertices < halfVertices * (circuit.cost Arithmetic.additionCost + 1)

An explicit exponential form of the middle-layer lower bound. For at least eight vertices, 4^halfVertices is strictly smaller than halfVertices times one plus the circuit's addition count.