Clique-polynomial lower bounds with arbitrary natural constants

Weighted Schnorr closure permits zero-weight substitutions, so it remains a valid addition measure even when the circuit has free named constants whose natural values may vanish. Combining it with clique-support separation gives the full clique-polynomial lower-bound family without any positivity premise on constants.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.NaturalConstants.circuit_addition_lowerBound_of_support_eq {K : Type u_1} {vertexCount cliqueSize : ℕ} (constant : K → ℕ) (target : MvPolynomial (Fin (vertexCount * vertexCount)) ℕ) (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, for any natural interpretation of named constants.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.NaturalConstants.circuit_addition_lowerBound {K : Type u_1} {vertexCount cliqueSize : ℕ} (constant : K → ℕ) (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

Schnorr's addition lower bound for the clique polynomial with arbitrary natural constants, including zero.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.NaturalConstants.central_circuit_addition_lowerBound {K : Type u_1} {halfVertices : ℕ} (constant : K → ℕ) (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

The central-binomial clique family retains its addition bound for every natural constant alphabet.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.NaturalConstants.central_circuit_exponential_lowerBound {K : Type u_1} {halfVertices : ℕ} (constant : K → ℕ) (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 addition lower bound for the middle clique layer, valid even with free zero constants.