Monotone clique bounds with logarithmically many petals per unit width

Razborov's approximation theorem permits a free choice of the number p of sunflower petals. For a dyadic width w = 2 ^ t, choose p = 4 * w * t, instead of w ^ 2 as in Complexity/Computability/Circuit/Monotone/Clique/Asymptotic.lean. The bound sunflowerBound p w ≤ (4 * t * w ^ 2) ^ w then gives two improvements using the same approximation theorem:

• For t ≥ 3, 4 * w ^ 2 ≤ k - 1, and k ^ 4 ≤ n, every monotone circuit for k-clique on n vertices has more than w ^ w = 2 ^ (t * 2 ^ t) gates.
• For t ≥ 4 and the same width constraint, more than 64 ^ w gates suffice as a lower bound already when 1024 * t ^ 2 * w ^ 4 * k ≤ n.

Thus taking w within a factor two of √k / 2 recovers a log k factor in the exponent in the first regime, or replaces the fourth-power vertex requirement by O(k ^ 3 * log(k) ^ 2) in the second. The formal statements below give the finite, integer parameter bounds. The variable n counts vertices; the number of Boolean inputs is edgeCount n.

These are new parameter instantiations of the library's existing proof, not new lower bounds against the monotone model beyond the literature.

Main results

• Cslib.Circuits.Monotone.two_pow_mul_two_pow_lt_size_of_computes_clique: the stronger exponent under the fourth-power vertex hypothesis.
• Cslib.Circuits.Monotone.sixtyFour_pow_two_pow_lt_size_of_computes_clique: the wider range of clique sizes for the 64 ^ w bound.
• Cslib.Circuits.Monotone.two_pow_mul_two_pow_lt_ecomplexity_clique, Cslib.Circuits.Monotone.sixtyFour_pow_two_pow_lt_ecomplexity_clique: the corresponding minimum circuit complexity bounds.

References

• A. A. Razborov, Lower bounds on the monotone complexity of some Boolean functions, for the approximation method.
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 14.3, for the approximation theorem instantiated here.

theorem Cslib.Circuits.Monotone.two_pow_mul_two_pow_lt_size_of_computes_clique {n k t : ℕ} (ht : 3 ≤ t) (hk : 4 * (2 ^ t) ^ 2 ≤ k - 1) (hn : k ^ 4 ≤ n) {C : Circuit signature (Clique.edgeCount n) 1} (hC : C.Computes interpretation (single (clique n k))) : 2 ^ (t * 2 ^ t) < C.size

With dyadic width w = 2 ^ t, t ≥ 3, 4 w² ≤ k - 1, and k⁴ ≤ n, every monotone circuit computing k-clique on n vertices has more than w ^ w = 2 ^ (t * 2 ^ t) gates. The proof uses 4 * w * t sunflower petals.

theorem Cslib.Circuits.Monotone.sixtyFour_pow_two_pow_lt_size_of_computes_clique {n k t : ℕ} (ht : 4 ≤ t) (hk : 4 * (2 ^ t) ^ 2 ≤ k - 1) (hn : 1024 * t ^ 2 * (2 ^ t) ^ 4 * k ≤ n) {C : Circuit signature (Clique.edgeCount n) 1} (hC : C.Computes interpretation (single (clique n k))) : 64 ^ 2 ^ t < C.size

With dyadic width w = 2 ^ t, t ≥ 4, and 4 w² ≤ k - 1, every monotone circuit for k-clique on n vertices has more than 64 ^ w gates when 1024 * t ^ 2 * w ^ 4 * k ≤ n. The proof uses 4 * w * t sunflower petals.

theorem Cslib.Circuits.Monotone.two_pow_mul_two_pow_lt_ecomplexity_clique {n k t : ℕ} (ht : 3 ≤ t) (hk : 4 * (2 ^ t) ^ 2 ≤ k - 1) (hn : k ^ 4 ≤ n) : ↑(2 ^ (t * 2 ^ t)) < ecomplexity interpretation (single (clique n k))

The minimum monotone circuit size for k-clique exceeds 2 ^ (t * 2 ^ t) under the dyadic-width and fourth-power vertex hypotheses.

theorem Cslib.Circuits.Monotone.sixtyFour_pow_two_pow_lt_ecomplexity_clique {n k t : ℕ} (ht : 4 ≤ t) (hk : 4 * (2 ^ t) ^ 2 ≤ k - 1) (hn : 1024 * t ^ 2 * (2 ^ t) ^ 4 * k ≤ n) : ↑(64 ^ 2 ^ t) < ecomplexity interpretation (single (clique n k))

The minimum monotone circuit size for k-clique exceeds 64 ^ (2 ^ t) under the dyadic-width and 1024 * t ^ 2 * (2 ^ t) ^ 4 * k ≤ n vertex hypotheses.