Razborov's lower bound for monotone circuits computing cliques

Evaluate a monotone circuit computing k-clique in the approximate interpretation. On the complete graphs on k-sets the circuit is right, so the approximator at its output is wrong on at most C(n, k)-many of them only if the circuit is large (Positive.scheme); if it is right on one, it is nonempty. A nonempty approximator accepts at least half of the colourings with k - 1 colours, on which the circuit is right and says false, so it is wrong on half of them, which again needs a large circuit (Negative.scheme). Either way the circuit is large (choose_le_or_pow_le_mul_size), with explicit bounds (lt_size_of_computes_clique) Razborov, Arora and Barak, Theorem 14.7.

Main results

• Cslib.Circuits.Monotone.choose_le_or_pow_le_mul_size: the dichotomy.
• Cslib.Circuits.Monotone.lt_size_of_computes_clique: the lower bound with explicit parameters.

References

• A. A. Razborov, Lower bounds on the monotone complexity of some Boolean functions
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 14.3
• S. Jukna, Boolean Function Complexity: Advances and Frontiers, Chapter 9

def Cslib.Circuits.Monotone.negativeGateCap (n r p w : ℕ) : ℕ

The number of negative errors charged to any gate.

theorem Cslib.Circuits.Monotone.Positive.errorCost_le {n k p w : ℕ} (op : Op) : errorCost n k p w op ≤ errorCap n k p w

theorem Cslib.Circuits.Monotone.Negative.errorCost_le {n p w : ℕ} (hp : 2 ≤ p) (r : ℕ) (op : Op) : errorCost n r p w op ≤ negativeGateCap n r p w

noncomputable def Cslib.Circuits.Monotone.outputApproximator {n p w : ℕ} [Fact (2 ≤ p)] (C : Circuit signature (Clique.edgeCount n) 1) : Approximator n p w

The approximator of the output of a circuit.

theorem Cslib.Circuits.Monotone.nonempty_outputApproximator {n k p w : ℕ} [Fact (2 ≤ p)] (hw : 2 ≤ w) (hk : w + 1 ≤ k) {C : Circuit signature (Clique.edgeCount n) 1} (hC : C.Computes interpretation (single (clique n k))) (hC' : Positive.errorCap n k p w * C.size < n.choose k) : (outputApproximator C).terms.Nonempty

If the circuit is small, the approximator of its output is right on some complete graph on a k-set, and so is nonempty.

theorem Cslib.Circuits.Monotone.card_acceptedColorings_le {n k p w : ℕ} [Fact (2 ≤ p)] (hw : 2 ≤ w) (hk : 0 < k) {C : Circuit signature (Clique.edgeCount n) 1} (hC : C.Computes interpretation (single (clique n k))) : (Negative.acceptedColorings (k - 1) (outputApproximator C).terms).card ≤ C.program.cost (Negative.errorCost n (k - 1) p w)

The approximator of the output of a circuit computing k-clique accepts only colourings with k - 1 colours on which it is wrong, and so at most as many as the negative cost of the circuit.

theorem Cslib.Circuits.Monotone.choose_le_or_pow_le_mul_size {n k p w : ℕ} [Fact (2 ≤ p)] (hw : 2 ≤ w) (hk : w + 1 ≤ k) (hr : 2 * w ^ 2 ≤ k - 1) {C : Circuit signature (Clique.edgeCount n) 1} (hC : C.Computes interpretation (single (clique n k))) : n.choose k ≤ Positive.errorCap n k p w * C.size ∨ (k - 1) ^ n ≤ 2 * negativeGateCap n (k - 1) p w * C.size

Razborov's dichotomy. A monotone circuit computing k-clique on n vertices exhausts the positive or the negative error budget of the approximators with p petals and width w.

theorem Cslib.Circuits.Monotone.lt_size_of_computes_clique {n k p w : ℕ} (hp : 2 ≤ p) (hw : 2 ≤ w) (hk : w + 1 ≤ k) (hr : 2 * w ^ 2 ≤ k - 1) {s : ℕ} (hpos : Positive.errorCap n k p w * s < n.choose k) (hneg : 2 * negativeGateCap n (k - 1) p w * s < (k - 1) ^ n) {C : Circuit signature (Clique.edgeCount n) 1} (hC : C.Computes interpretation (single (clique n k))) : s < C.size

Razborov's lower bound. Every monotone circuit computing k-clique on n vertices has more than s gates, for every s below both error budgets of the approximators with p ≥ 2 petals and width w ≥ 2, if w + 1 ≤ k and 2 w ^ 2 ≤ k - 1.