A 2 ^ √k lower bound for monotone circuits computing cliques

With width w and w ^ 2 petals, sunflowerBound (w ^ 2) w ≤ (w + 1) w ^ (3 w), and the two error budgets of Razborov's dichotomy (Cslib.Circuits.Monotone.lt_size_of_computes_clique) are satisfied by the size 64 ^ w = 2 ^ (6 w) as soon as w ≥ 16, 4 w ^ 2 ≤ k - 1 and 64 w ^ 6 k ≤ n (pow_lt_size_of_computes_clique). Taking w = ⌊√(k - 1)⌋ / 2 handles k ≥ 1025; for 2 ≤ k ≤ 1024, every edge is essential (edgeCount_le_succ_size), which already forces (n / 2) ^ 2 - 1 gates.

So for 2 ≤ k with k ^ 4 ≤ n, every monotone circuit computing k-clique on n vertices has more than 2 ^ (2 ⌊√k⌋) gates (two_pow_two_mul_sqrt_lt_size), hence more than 2 ^ √k (two_rpow_sqrt_lt_size). This is the 2 ^ (ε √k) bound of Razborov and of Alon and Boppana, in the form of Arora and Barak, Theorem 14.7, with ε = 1.

Main results

• Cslib.Circuits.Monotone.two_pow_two_mul_sqrt_lt_ecomplexity_clique: the lower bound for the monotone circuit complexity of k-clique.
• Cslib.Circuits.Monotone.two_rpow_sqrt_lt_size: the real form.

References

• A. A. Razborov, Lower bounds on the monotone complexity of some Boolean functions
• N. Alon, R. B. Boppana, The monotone circuit complexity of Boolean functions
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 14.3

theorem Cslib.Circuits.Monotone.pow_lt_size_of_computes_clique {n k w : ℕ} (hw : 16 ≤ w) (hk : 4 * w ^ 2 ≤ k - 1) (hn : 64 * w ^ 6 * k ≤ n) {C : Circuit signature (Clique.edgeCount n) 1} (hC : C.Computes interpretation (single (clique n k))) : 64 ^ w < C.size

A monotone 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 Cslib.Circuits.Monotone.two_pow_two_mul_sqrt_lt_size {n k : ℕ} (hk : 2 ≤ k) (hn : k ^ 4 ≤ n) {C : Circuit signature (Clique.edgeCount n) 1} (hC : C.Computes interpretation (single (clique n k))) : 2 ^ (2 * k.sqrt) < C.size

The monotone lower bound for cliques. For 2 ≤ k with k ^ 4 ≤ n, every monotone circuit computing k-clique on n vertices has more than 2 ^ (2 ⌊√k⌋) gates.

theorem Cslib.Circuits.Monotone.two_pow_two_mul_sqrt_lt_ecomplexity_clique {n k : ℕ} (hk : 2 ≤ k) (hn : k ^ 4 ≤ n) : ↑(2 ^ (2 * k.sqrt)) < ecomplexity interpretation (single (clique n k))

The monotone circuit complexity of cliques. For 2 ≤ k with k ^ 4 ≤ n, the monotone circuit complexity of k-clique on n vertices exceeds 2 ^ (2 ⌊√k⌋).

theorem Cslib.Circuits.Monotone.two_rpow_sqrt_lt_size {n k : ℕ} (hk : 2 ≤ k) (hn : k ^ 4 ≤ n) {C : Circuit signature (Clique.edgeCount n) 1} (hC : C.Computes interpretation (single (clique n k))) : 2 ^ √↑k < ↑C.size

The monotone lower bound for cliques, real form. For 2 ≤ k with k ^ 4 ≤ n, every monotone circuit computing k-clique on n vertices has more than 2 ^ √k gates.