A 2^√k lower bound for monotone CLIQUE circuits

We instantiate the finite approximation dichotomy of LowerBound.lean for every admissible pair of a vertex count n and a clique size k, not only along the special family of Exponential.lean.

For a width w we use w^2 sunflower petals. Writing F = Sunflower.bound (w^2) w ≤ (w + 1) * w^(3w), the two budgets become:

• positive: when 64 * w^6 * k ≤ n, the ratio between the number of k-sets of vertices and the number of those containing a fixed (w+1)-set is at least (64 * w^6)^(w+1), which exceeds F^2 * 64^w;
• negative: when 4 * w^2 ≤ k - 1, a fixed w^2-petal sunflower is plucked wrongly by at most a 4^-(w^2) fraction of the colorings, and 6 * F^2 * 64^w < 4^(w^2) once w ≥ 16.

So every circuit computing k-CLIQUE has more than 64^w = 2^(6w) gates (sixtyFourPow_lt_circuitSize). Choosing w = ⌊√(k-1)⌋ / 2 handles 1025 ≤ k (twoPow_two_mul_sqrt_lt_circuitSize_of_large). Smaller clique sizes are covered by Essential.lean: for 2 ≤ k ≤ 1024 every edge variable is essential, which already forces (n / 2)^2 - 1 gates, and for k ≤ 1 no constant-free circuit computes k-CLIQUE at all.

Together: for every k with k^4 ≤ n (that is, k ≤ n^(1/4)), every binary, constant-free monotone shared circuit computing k-CLIQUE on n vertices has more than 2^(2⌊√k⌋) gates (twoPow_two_mul_sqrt_lt_circuitSize) and hence more than 2^√k gates (rpow_sqrt_lt_circuitSize). This is the 2^(ε√k) bound of Razborov (1985) and Alon–Boppana (1987), in the form of Arora–Barak Theorem 14.7, with ε = 1, in the circuit model of the imported library (every AND and OR gate has fan-in two and is counted).

theorem Algebraic.Monotone.Clique.Asymptotic.pow_mul_choose_sub_le_choose (q n k d : ℕ) (qPositive : 1 ≤ q) (d_le_k : d ≤ k) (verticesLarge : q * k ≤ n) : q ^ d * (n - d).choose (k - d) ≤ n.choose k

A d-subset of a k-set lies in at most a q^-d fraction of the k-subsets of an n-set when q * k ≤ n, stated without division.

theorem Algebraic.Monotone.Clique.Asymptotic.sunflower_bound_le (w : ℕ) : Sunflower.bound (w ^ 2) w ≤ (w + 1) * w ^ (3 * w)

The elementary sunflower bound at w^2 petals is at most (w + 1) * w^(3w).

theorem Algebraic.Monotone.Clique.Asymptotic.mul_pow_six_le_four_pow (w : ℕ) (sixteen_le : 16 ≤ w) : 128 * w ^ 6 ≤ 4 ^ w

A sixth power is eventually dominated by 4^w.

theorem Algebraic.Monotone.Clique.Asymptotic.six_mul_succ_sq_lt_two_pow (w : ℕ) (sixteen_le : 16 ≤ w) : 6 * (w + 1) ^ 2 < 2 ^ w

A quadratic is eventually dominated by 2^w.

theorem Algebraic.Monotone.Clique.Asymptotic.positive_budget (n k w : ℕ) (one_le : 1 ≤ w) (width_succ_le_k : w + 1 ≤ k) (verticesLarge : 64 * w ^ 6 * k ≤ n) : LowerBound.positiveGateCap n k (w ^ 2) w * 64 ^ w < n.choose k

The positive truncation budget at width w, w^2 petals, and size bound 64^w is below the number of minimal positive clique graphs.

theorem Algebraic.Monotone.Clique.Asymptotic.negative_budget (n k w : ℕ) (sixteen_le : 16 ≤ w) (widthSmall : 4 * w ^ 2 ≤ k - 1) (petals_le_n : w ^ 2 ≤ n) : 2 * LowerBound.negativeGateCap n (k - 1) (w ^ 2) w * 64 ^ w < (k - 1) ^ n

The negative plucking budget at width w, w^2 petals, and size bound 64^w is below the number of colorings with k - 1 colors.

theorem Algebraic.Monotone.Clique.Asymptotic.sixtyFourPow_lt_circuitSize (n k w : ℕ) (sixteen_le : 16 ≤ w) (widthSmall : 4 * w ^ 2 ≤ k - 1) (verticesLarge : 64 * w ^ 6 * k ≤ n) (circuit : Circuit AndOr.signature (edgeCount n) 1) (computes : ∀ (assignment : Fin (edgeCount n) → Bool), circuit.eval AndOr.boolInterpretation assignment 0 = function n k assignment) : 64 ^ w < circuit.size

Every binary, constant-free monotone shared circuit computing k-CLIQUE on n vertices has more than 64^w gates, for every width w ≥ 16 with 4 * w^2 ≤ k - 1 and 64 * w^6 * k ≤ n.

theorem Algebraic.Monotone.Clique.Asymptotic.twoPow_two_mul_sqrt_lt_circuitSize_of_large (n k : ℕ) (cliqueLarge : 1025 ≤ k) (verticesLarge : k ^ 4 ≤ n) (circuit : Circuit AndOr.signature (edgeCount n) 1) (computes : ∀ (assignment : Fin (edgeCount n) → Bool), circuit.eval AndOr.boolInterpretation assignment 0 = function n k assignment) : 2 ^ (2 * k.sqrt) < circuit.size

The approximation bound for large cliques: for 1025 ≤ k and k^4 ≤ n, every binary, constant-free monotone shared circuit computing k-CLIQUE on n vertices has more than 2^(2⌊√k⌋) gates.

theorem Algebraic.Monotone.Clique.Asymptotic.fourPow_sqrt_add_two_le (k : ℕ) (two_le : 2 ≤ k) (k_le : k ≤ 1024) : 4 ^ k.sqrt + 2 ≤ (k ^ 4 / 2) ^ 2

For 2 ≤ k ≤ 1024, the edge count of k^4 vertices exceeds 4^⌊√k⌋ + 1.

theorem Algebraic.Monotone.Clique.Asymptotic.twoPow_two_mul_sqrt_lt_circuitSize (n k : ℕ) (verticesLarge : k ^ 4 ≤ n) (circuit : Circuit AndOr.signature (edgeCount n) 1) (computes : ∀ (assignment : Fin (edgeCount n) → Bool), circuit.eval AndOr.boolInterpretation assignment 0 = function n k assignment) : 2 ^ (2 * k.sqrt) < circuit.size

Monotone CLIQUE lower bound. For every k with k^4 ≤ n, that is k ≤ n^(1/4), every binary, constant-free monotone shared circuit computing k-CLIQUE on n vertices has more than 2^(2⌊√k⌋) gates. For k ≤ 1 no such circuit exists.

theorem Algebraic.Monotone.Clique.Asymptotic.rpow_sqrt_lt_circuitSize (n k : ℕ) (verticesLarge : k ^ 4 ≤ n) (circuit : Circuit AndOr.signature (edgeCount n) 1) (computes : ∀ (assignment : Fin (edgeCount n) → Bool), circuit.eval AndOr.boolInterpretation assignment 0 = function n k assignment) : 2 ^ √↑k < ↑circuit.size

Monotone CLIQUE lower bound, real form. For every k ≤ n^(1/4), every binary, constant-free monotone shared circuit computing k-CLIQUE on n vertices has more than 2^√k gates.