Clique-polynomial lower bounds with positive constants

This module combines the clique-support separation theorem with the generic positive-constant Schnorr measure. The resulting bounds allow an arbitrary alphabet of free named constants, provided their natural interpretation is strictly positive. Thus positive coefficients and reusable positive scalar gates do not weaken the clique-polynomial addition lower bound.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.PositiveConstants.circuit_addition_lowerBound_of_support_eq {K : Type u_1} {vertexCount cliqueSize : ℕ} (constant : K → ℕ) (positive : ∀ (scalar : K), 0 < constant scalar) (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, even when the circuit has free positive constants.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.PositiveConstants.circuit_addition_lowerBound {K : Type u_1} {vertexCount cliqueSize : ℕ} (constant : K → ℕ) (positive : ∀ (scalar : K), 0 < constant scalar) (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, allowing free positive named constants.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.PositiveConstants.central_circuit_addition_lowerBound {K : Type u_1} {halfVertices : ℕ} (constant : K → ℕ) (positive : ∀ (scalar : K), 0 < constant scalar) (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 in the presence of arbitrary positive constants.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Clique.PositiveConstants.central_circuit_exponential_lowerBound {K : Type u_1} {halfVertices : ℕ} (constant : K → ℕ) (positive : ∀ (scalar : K), 0 < constant scalar) (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, still valid for circuits with free positive named constants.