An explicit exponential lower bound for monotone CLIQUE circuits

We instantiate the finite approximation dichotomy with

• width w,
• clique size w^4,
• vertex count w^20, and
• w^2 sunflower petals.

For every w ≥ 16, a binary, constant-free monotone shared circuit computing this CLIQUE function has more than w^w gates. Taking w = 2^t gives the closed form 2^(t * 2^t) gates on 2^(20*t) vertices.

This is an explicit finite specialization of Razborov's monotone approximation method (1985).

theorem Algebraic.Monotone.Clique.Exponential.pow_mul_descFactorial_le (q k d : ℕ) (qPositive : 1 ≤ q) (d_le_k : d ≤ k) : q ^ d * k.descFactorial d ≤ (q * k).descFactorial d

Scaling the ambient set by q scales every factor in a descending factorial by at least q.

theorem Algebraic.Monotone.Clique.Exponential.pow_mul_choose_le_choose_mul (q k d : ℕ) (qPositive : 1 ≤ q) (d_le_k : d ≤ k) : q ^ d * k.choose d ≤ (q * k).choose d

Binomial coefficients inherit the descending-factorial scaling bound.

theorem Algebraic.Monotone.Clique.Exponential.pow_mul_containing_choose_le (q k d : ℕ) (qPositive : 1 ≤ q) (d_le_k : d ≤ k) : q ^ d * (q * k - d).choose (k - d) ≤ (q * k).choose k

A d-set occurs in at most a q^-d fraction of the k-sets of a q*k-element universe, stated without division.

theorem Algebraic.Monotone.Clique.Exponential.mul_containing_choose_lt (q k d budget : ℕ) (qPositive : 1 ≤ q) (d_le_k : d ≤ k) (budgetSmall : budget < q ^ d) : budget * (q * k - d).choose (k - d) < (q * k).choose k

Strict form used by the positive approximation budget.

theorem Algebraic.Monotone.Clique.Exponential.sunflower_bound_le_pow (w : ℕ) (two_le : 2 ≤ w) : Sunflower.bound (w ^ 2) w ≤ w ^ (4 * w)

The elementary sunflower bound at w^2 petals is at most w^(4w).

theorem Algebraic.Monotone.Clique.Exponential.positive_budget (w : ℕ) (sixteen_le : 16 ≤ w) : LowerBound.positiveGateCap (w ^ 20) (w ^ 4) (w ^ 2) w * w ^ w < (w ^ 20).choose (w ^ 4)

The positive truncation budget is strictly smaller than the number of minimal positive clique graphs.

theorem Algebraic.Monotone.Clique.Exponential.negative_budget (w : ℕ) (sixteen_le : 16 ≤ w) : 2 * LowerBound.negativeGateCap (w ^ 20) (w ^ 4 - 1) (w ^ 2) w * w ^ w < (w ^ 4 - 1) ^ w ^ 20

The negative plucking budget is also strictly below the full coloring space for the chosen parameters.

theorem Algebraic.Monotone.Clique.Exponential.powSelf_lt_circuitSize (w : ℕ) (sixteen_le : 16 ≤ w) (circuit : Circuit AndOr.signature (edgeCount (w ^ 20)) 1) (computes : ∀ (assignment : Fin (edgeCount (w ^ 20)) → Bool), circuit.eval AndOr.boolInterpretation assignment 0 = function (w ^ 20) (w ^ 4) assignment) : w ^ w < circuit.size

Explicit exponential lower bound in the width parameter for binary, constant-free monotone shared circuits.

theorem Algebraic.Monotone.Clique.Exponential.twoPow_lt_circuitSize (t : ℕ) (four_le : 4 ≤ t) (circuit : Circuit AndOr.signature (edgeCount ((2 ^ t) ^ 20)) 1) (computes : ∀ (assignment : Fin (edgeCount ((2 ^ t) ^ 20)) → Bool), circuit.eval AndOr.boolInterpretation assignment 0 = function ((2 ^ t) ^ 20) ((2 ^ t) ^ 4) assignment) : 2 ^ (t * 2 ^ t) < circuit.size

Closed power-of-two specialization. On N = 2^(20t) vertices, the 2^(4t)-CLIQUE function needs more than 2^(t*2^t) monotone gates.