Every edge is essential to the clique function

For 2 ≤ k ≤ n, removing one edge from the complete graph on a k-set through it destroys every k-clique, so the k-clique function depends on every edge (essentialAt_clique). A monotone circuit has fan-in at most two, so it has at least n.choose 2 - 1 gates (edgeCount_le_succ_size). This settles small clique sizes, where the method of approximations says nothing.

It also records that monotone circuits compute the clique function at all, as the disjunction over the k-sets of the conjunction of their edges (exists_computes_clique), so that the lower bounds for it are not vacuous.

Main results

• Cslib.Circuits.Monotone.exists_computes_clique: some monotone circuit computes k-clique.
• Cslib.Circuits.Monotone.essentialAt_clique: every edge is essential to k-clique.
• Cslib.Circuits.Monotone.edgeCount_le_succ_size, Cslib.Circuits.Monotone.edgeCount_le_two_pow_depth: the resulting size and depth bounds.

theorem Cslib.Circuits.Monotone.program_fanInAtMost_two {n g : ℕ} (p : Program signature n g) : p.FanInAtMost 2

Monotone programs have fan-in at most two.

theorem Cslib.Circuits.Monotone.exists_computes_clique (n k : ℕ) : ∃ (C : Circuit signature (Clique.edgeCount n) 1), C.Computes interpretation (single (clique n k))

Monotone circuits compute cliques: the disjunction over the k-sets of the conjunction of their edges.

theorem Cslib.Circuits.Monotone.ecomplexity_clique_ne_top (n k : ℕ) : ecomplexity interpretation (single (clique n k)) ≠ ⊤

The monotone circuit complexity of k-clique is finite.

theorem Cslib.Circuits.Monotone.essentialAt_clique {n k : ℕ} (hk : 2 ≤ k) (hkn : k ≤ n) (i : Fin (Clique.edgeCount n)) : EssentialAt (single (clique n k)) i

For 2 ≤ k ≤ n, every edge is essential to k-clique.

theorem Cslib.Circuits.Monotone.edgeCount_le_succ_size {n k : ℕ} (hk : 2 ≤ k) (hkn : k ≤ n) {C : Circuit signature (Clique.edgeCount n) 1} (hC : C.Computes interpretation (single (clique n k))) : Clique.edgeCount n ≤ 1 + C.size

For 2 ≤ k ≤ n, a monotone circuit computing k-clique has at least n.choose 2 - 1 gates.

theorem Cslib.Circuits.Monotone.edgeCount_le_two_pow_depth {n k : ℕ} (hk : 2 ≤ k) (hkn : k ≤ n) {C : Circuit signature (Clique.edgeCount n) 1} (hC : C.Computes interpretation (single (clique n k))) : Clique.edgeCount n ≤ 2 ^ C.depth

For 2 ≤ k ≤ n, a monotone circuit computing k-clique has depth at least log₂ C(n, 2).

theorem Cslib.Circuits.Monotone.sq_half_le_edgeCount (n : ℕ) : (n / 2) ^ 2 ≤ Clique.edgeCount n

There are at least (n / 2) ^ 2 possible edges.