The clique function

A Boolean function of the possible edges of a graph on n vertices, the unordered pairs of distinct vertices (Cslib.Circuits.Clique.Edge), reads its input as a graph (Cslib.Circuits.Clique.graph). The k-clique function Cslib.Circuits.clique n k says whether that graph has a clique of k vertices.

Two families of inputs are used to prove lower bounds for it: the complete graph on a set of k vertices (Cslib.Circuits.Clique.ofFinset), which has a k-clique, and the complete multipartite graph of a colouring with fewer than k colours (Cslib.Circuits.Clique.ofColoring), which has none.

Main definitions

• Cslib.Circuits.Clique.Edge, Cslib.Circuits.Clique.edgeCount: the possible edges.
• Cslib.Circuits.Clique.graph: the graph of an input.
• Cslib.Circuits.Clique.Contains: the input contains all edges inside a set of vertices.
• Cslib.Circuits.clique: the k-clique function.
• Cslib.Circuits.Clique.ofFinset, Cslib.Circuits.Clique.ofColoring: test inputs.

Main results

• Cslib.Circuits.Clique.edgeCount_eq_choose: there are n.choose 2 possible edges.
• Cslib.Circuits.clique_eq_true_iff: the clique function in terms of SimpleGraph.IsNClique.
• Cslib.Circuits.clique_ofFinset, Cslib.Circuits.clique_ofColoring: the test inputs.

@[reducible, inline]

abbrev Cslib.Circuits.Clique.Edge (n : ℕ) : Type

The possible edges of a graph on n vertices: unordered pairs of distinct vertices.

@[reducible, inline]

abbrev Cslib.Circuits.Clique.edgeCount (n : ℕ) : ℕ

The number of possible edges of a graph on n vertices.

theorem Cslib.Circuits.Clique.edgeCount_eq_choose (n : ℕ) : edgeCount n = n.choose 2

noncomputable def Cslib.Circuits.Clique.edgeEquiv (n : ℕ) : Edge n ≃ Fin (edgeCount n)

A numbering of the possible edges by the inputs of a circuit.

def Cslib.Circuits.Clique.graph {n : ℕ} (x : Fin (edgeCount n) → Bool) : SimpleGraph (Fin n)

The graph of an input: its edges are the possible edges set to true.

def Cslib.Circuits.Clique.Contains {n : ℕ} (x : Fin (edgeCount n) → Bool) (s : Finset (Fin n)) : Prop

The input x contains all edges between the vertices of s.

@[instance_reducible]

noncomputable instance Cslib.Circuits.Clique.instDecidableContains {n : ℕ} (x : Fin (edgeCount n) → Bool) (s : Finset (Fin n)) : Decidable (Contains x s)

def Cslib.Circuits.Clique.edge {n : ℕ} {u v : Fin n} (h : u ≠ v) : Edge n

The edge between two distinct vertices.

@[simp]

theorem Cslib.Circuits.Clique.toFinset_edge {n : ℕ} {u v : Fin n} (h : u ≠ v) : (↑(edge h)).toFinset = {u, v}

theorem Cslib.Circuits.Clique.Contains.mono {n : ℕ} {x : Fin (edgeCount n) → Bool} {s t : Finset (Fin n)} (hst : s ⊆ t) (h : Contains x t) : Contains x s

theorem Cslib.Circuits.Clique.contains_iff_isClique {n : ℕ} {x : Fin (edgeCount n) → Bool} {s : Finset (Fin n)} : Contains x s ↔ (graph x).IsClique ↑s

Containing all edges inside s is being a clique of the graph.

noncomputable def Cslib.Circuits.Clique.ofFinset {n : ℕ} (s : Finset (Fin n)) : Fin (edgeCount n) → Bool

The complete graph on s, as an input.

@[simp]

theorem Cslib.Circuits.Clique.ofFinset_edgeEquiv {n : ℕ} (s : Finset (Fin n)) (e : Edge n) : ofFinset s ((edgeEquiv n) e) = decide ((↑e).toFinset ⊆ s)

theorem Cslib.Circuits.Clique.contains_ofFinset {n : ℕ} (s : Finset (Fin n)) : Contains (ofFinset s) s

theorem Cslib.Circuits.Clique.subset_of_contains_ofFinset {n : ℕ} {s t : Finset (Fin n)} (ht : 2 ≤ t.card) (h : Contains (ofFinset s) t) : t ⊆ s

In the complete graph on s, the sets of at least two vertices with all edges inside are the subsets of s.

noncomputable def Cslib.Circuits.Clique.ofColoring {n r : ℕ} (c : Fin n → Fin r) : Fin (edgeCount n) → Bool

The complete multipartite graph of a colouring, as an input: two vertices are adjacent when they have different colours.

theorem Cslib.Circuits.Clique.contains_ofColoring_iff {n r : ℕ} {c : Fin n → Fin r} {s : Finset (Fin n)} : Contains (ofColoring c) s ↔ Set.InjOn c ↑s

In the graph of a colouring, the sets with all edges inside are those coloured injectively.

theorem Cslib.Circuits.Clique.card_le_of_contains_ofColoring {n r : ℕ} {c : Fin n → Fin r} {s : Finset (Fin n)} (h : Contains (ofColoring c) s) : s.card ≤ r

A set with all edges inside in the graph of a colouring with r colours has at most r vertices.

@[reducible, inline]

abbrev Cslib.Circuits.Clique.CliqueSet (n k : ℕ) : Type

The sets of k vertices.

@[reducible, inline]

abbrev Cslib.Circuits.Clique.Coloring (n r : ℕ) : Type

The colourings of n vertices with r colours.

noncomputable def Cslib.Circuits.clique (n k : ℕ) : BooleanFunction (Clique.edgeCount n)

The k-clique function on graphs with n vertices: whether the graph of the input has a clique of k vertices.

theorem Cslib.Circuits.clique_eq_true_iff {n k : ℕ} {x : Fin (Clique.edgeCount n) → Bool} : clique n k x = true ↔ ∃ (s : Finset (Fin n)), (Clique.graph x).IsNClique k s

theorem Cslib.Circuits.clique_ofFinset {n k : ℕ} {s : Finset (Fin n)} (hs : s.card = k) : clique n k (Clique.ofFinset s) = true

The complete graph on k vertices has a k-clique.

theorem Cslib.Circuits.clique_ofColoring {n k r : ℕ} (hr : r < k) (c : Fin n → Fin r) : clique n k (Clique.ofColoring c) = false

The complete multipartite graph of a colouring with fewer than k colours has no k-clique.

theorem Cslib.Circuits.clique_le_clique {n k : ℕ} {x y : Fin (Clique.edgeCount n) → Bool} (h : ∀ (i : Fin (Clique.edgeCount n)), x i ≤ y i) : clique n k x ≤ clique n k y

The clique function is monotone.