The monotone Boolean CLIQUE function

This file fixes a concrete, one-variable-per-undirected-edge encoding of CLIQUE. Edges are ordered pairs (u,v) with u < v; the noncomputable equivalence with Fin (Fintype.card (Edge n)) is only the boundary required by Circuit's Fin-indexed input interface.

Two finite test families are provided for the approximation argument:

• CliqueSet n k, the k-subsets of the vertex set, represented by their minimal positive graphs; and
• Coloring n r, whose assignments are complete r-partite graphs.

For r = k - 1, every coloring assignment is a negative CLIQUE input. This is the pigeonhole separation used in Razborov's monotone approximation method.

@[reducible, inline]

abbrev Algebraic.Monotone.Clique.Edge (n : ℕ) : Type

A canonical undirected edge on Fin n.

Equations

• Algebraic.Monotone.Clique.Edge n = { edge : Fin n × Fin n // edge.1 < edge.2 }

@[instance_reducible]

noncomputable instance Algebraic.Monotone.Clique.instFintypeEdge {n : ℕ} : Fintype (Edge n)

Equations

• Algebraic.Monotone.Clique.instFintypeEdge = Fintype.subtype {edge : Fin n × Fin n | edge.1 < edge.2} ⋯

@[reducible, inline]

noncomputable abbrev Algebraic.Monotone.Clique.edgeCount (n : ℕ) : ℕ

The number of undirected edges in the chosen encoding.

Equations

• Algebraic.Monotone.Clique.edgeCount n = Fintype.card (Algebraic.Monotone.Clique.Edge n)

noncomputable def Algebraic.Monotone.Clique.edgeEquiv (n : ℕ) : Edge n ≃ Fin (edgeCount n)

Reindex canonical edges by the Fin input type expected by circuits.

Equations

• Algebraic.Monotone.Clique.edgeEquiv n = Fintype.equivFin (Algebraic.Monotone.Clique.Edge n)

def Algebraic.Monotone.Clique.Edge.Inside {n : ℕ} (edge : Edge n) (vertices : Finset (Fin n)) : Prop

Both endpoints of an edge lie in a vertex set.

Equations

• edge.Inside vertices = ((↑edge).1 ∈ vertices ∧ (↑edge).2 ∈ vertices)

@[instance_reducible]

instance Algebraic.Monotone.Clique.instDecidableInside {n : ℕ} (edge : Edge n) (vertices : Finset (Fin n)) : Decidable (edge.Inside vertices)

Equations

• Algebraic.Monotone.Clique.instDecidableInside edge vertices = id inferInstance

@[reducible, inline]

abbrev Algebraic.Monotone.Clique.CliqueSet (n k : ℕ) : Type

The family of k-element vertex sets.

Equations

• Algebraic.Monotone.Clique.CliqueSet n k = ↥(Finset.powersetCard k Finset.univ)

@[reducible, inline]

abbrev Algebraic.Monotone.Clique.Coloring (n r : ℕ) : Type

The family of vertex colorings with r colors.

Equations

• Algebraic.Monotone.Clique.Coloring n r = (Fin n → Fin r)

noncomputable def Algebraic.Monotone.Clique.cliqueAssignment {n : ℕ} (vertices : Finset (Fin n)) : Fin (edgeCount n) → Bool

The minimal positive graph consisting exactly of the edges induced by a vertex set.

Equations

• Algebraic.Monotone.Clique.cliqueAssignment vertices input = decide (((Algebraic.Monotone.Clique.edgeEquiv n).symm input).Inside vertices)

@[simp]

theorem Algebraic.Monotone.Clique.cliqueAssignment_edge {n : ℕ} (vertices : Finset (Fin n)) (edge : Edge n) : cliqueAssignment vertices ((edgeEquiv n) edge) = decide (edge.Inside vertices)

noncomputable def Algebraic.Monotone.Clique.coloringAssignment {n r : ℕ} (coloring : Coloring n r) : Fin (edgeCount n) → Bool

The complete multipartite graph induced by a coloring: vertices are adjacent exactly when they receive different colors.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebraic.Monotone.Clique.coloringAssignment_edge {n r : ℕ} (coloring : Coloring n r) (edge : Edge n) : coloringAssignment coloring ((edgeEquiv n) edge) = decide (coloring (↑edge).1 ≠ coloring (↑edge).2)

def Algebraic.Monotone.Clique.Contains {n : ℕ} (assignment : Fin (edgeCount n) → Bool) (vertices : Finset (Fin n)) : Prop

An assignment contains every edge induced by vertices.

Equations

• Algebraic.Monotone.Clique.Contains assignment vertices = ∀ (edge : Algebraic.Monotone.Clique.Edge n), edge.Inside vertices → assignment ((Algebraic.Monotone.Clique.edgeEquiv n) edge) = true

theorem Algebraic.Monotone.Clique.Contains.mono_vertices {n : ℕ} {assignment : Fin (edgeCount n) → Bool} {small large : Finset (Fin n)} (subset : small ⊆ large) (contains : Contains assignment large) : Contains assignment small

Containing the clique on a vertex set implies containing every smaller clique.

theorem Algebraic.Monotone.Clique.subset_of_contains_cliqueAssignment {n : ℕ} {vertices test : Finset (Fin n)} (two_le : 2 ≤ test.card) (contains : Contains (cliqueAssignment vertices) test) : test ⊆ vertices

On a minimal clique graph, every contained vertex set of size at least two lies inside the generating clique.

@[instance_reducible]

noncomputable instance Algebraic.Monotone.Clique.instDecidableContains {n : ℕ} (assignment : Fin (edgeCount n) → Bool) (vertices : Finset (Fin n)) : Decidable (Contains assignment vertices)

Equations

• Algebraic.Monotone.Clique.instDecidableContains assignment vertices = Fintype.decidableForallFintype

noncomputable def Algebraic.Monotone.Clique.function (n k : ℕ) (assignment : Fin (edgeCount n) → Bool) : Bool

The ordinary monotone Boolean k-CLIQUE function on n vertices.

Equations

• Algebraic.Monotone.Clique.function n k assignment = decide (∃ (vertices : Algebraic.Monotone.Clique.CliqueSet n k), Algebraic.Monotone.Clique.Contains assignment ↑vertices)

@[simp]

theorem Algebraic.Monotone.Clique.function_cliqueAssignment {n k : ℕ} (vertices : CliqueSet n k) : function n k (cliqueAssignment ↑vertices) = true

The minimal graph of a k-set is a positive CLIQUE input.

theorem Algebraic.Monotone.Clique.coloring_injectiveOn_of_contains {n r : ℕ} (coloring : Coloring n r) (vertices : Finset (Fin n)) (contains : Contains (coloringAssignment coloring) vertices) : Set.InjOn coloring ↑vertices

If a coloring graph contains a clique on vertices, then the coloring is injective on those vertices.

theorem Algebraic.Monotone.Clique.card_le_colors_of_contains_coloring {n r : ℕ} (coloring : Coloring n r) (vertices : Finset (Fin n)) (contains : Contains (coloringAssignment coloring) vertices) : vertices.card ≤ r

A complete r-partite graph has no clique larger than its color set.

theorem Algebraic.Monotone.Clique.function_coloringAssignment_eq_false {k n : ℕ} (positive : 0 < k) (coloring : Coloring n (k - 1)) : function n k (coloringAssignment coloring) = false

Every complete (k-1)-partite graph is a negative k-CLIQUE input.

theorem Algebraic.Monotone.Clique.function_monotone {n k : ℕ} : Monotone (function n k)

CLIQUE is monotone in its edge variables.