Constant clique sizes and essential edges

Two elementary facts about binary, constant-free AND/OR circuits and the CLIQUE function of Basic.lean. They give lower bounds for small clique sizes, where the approximation method has nothing to say.

• Such a circuit outputs false on the empty graph, while 0-CLIQUE and 1-CLIQUE accept it. So no such circuit computes either (not_computes_of_le_one).
• For 2 ≤ k ≤ n, every edge variable is essential to k-CLIQUE: removing one edge from the minimal graph of a k-set through it destroys every k-clique. The fan-in bound then gives edgeCount n ≤ 1 + size (edgeCount_le_succ_size), and (n / 2)^2 ≤ edgeCount n.

theorem Algebraic.Monotone.Clique.program_eval_allFalse {inputCount gateCount : ℕ} (program : Program AndOr.signature inputCount gateCount) (gate : Fin gateCount) : program.eval AndOr.boolInterpretation (fun (x : Fin inputCount) => false) gate = false

Every gate of a binary AND/OR program is false on the all-false input.

theorem Algebraic.Monotone.Clique.circuit_eval_allFalse {inputCount : ℕ} (circuit : Circuit AndOr.signature inputCount 1) : circuit.eval AndOr.boolInterpretation (fun (x : Fin inputCount) => false) 0 = false

A binary AND/OR circuit outputs false on the all-false input.

theorem Algebraic.Monotone.Clique.function_allFalse {n k : ℕ} (k_le_one : k ≤ 1) (k_le_n : k ≤ n) : (function n k fun (x : Fin (edgeCount n)) => false) = true

With at most one vertex, a clique has no edges, so the empty graph contains a k-clique whenever k ≤ 1 and k ≤ n.

theorem Algebraic.Monotone.Clique.not_computes_of_le_one {n k : ℕ} (k_le_one : k ≤ 1) (k_le_n : k ≤ n) (circuit : Circuit AndOr.signature (edgeCount n) 1) : ¬∀ (assignment : Fin (edgeCount n) → Bool), circuit.eval AndOr.boolInterpretation assignment 0 = function n k assignment

No binary, constant-free AND/OR circuit computes k-CLIQUE for k ≤ 1 (when k ≤ n): the empty graph is accepted but the circuit rejects it.

theorem Algebraic.Monotone.Clique.essentialAt_function {n k : ℕ} (two_le : 2 ≤ k) (k_le_n : k ≤ n) (input : Fin (edgeCount n)) : EssentialAt (fun (assignment : Fin (edgeCount n) → Bool) (x : Fin 1) => function n k assignment) input

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

theorem Algebraic.Monotone.Clique.program_fanInAtMost_two {inputCount gateCount : ℕ} (program : Program AndOr.signature inputCount gateCount) : program.FanInAtMost 2

Every binary AND/OR program has fan-in at most two.

theorem Algebraic.Monotone.Clique.edgeCount_le_succ_size {n k : ℕ} (two_le : 2 ≤ k) (k_le_n : 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) : edgeCount n ≤ 1 + circuit.size

For 2 ≤ k ≤ n, a binary AND/OR circuit computing k-CLIQUE reads every edge variable, so it has at least edgeCount n - 1 gates.

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

The edges between the first n / 2 vertices and the next n / 2 vertices give (n / 2)^2 ≤ edgeCount n.