Erdős–Ramsey model: monochromatic -sets on a graph
Definitionerdos1947extremal-combinatoricsgraph-theoryprobabilistic-methodramsey-theory
The foundational model for the probabilistic Ramsey lower bound. Let be a simple graph on a vertex set and let be a natural number. A -element vertex subset is monochromatic in when it is either a -clique or an independent set of size — the two monochromatic color classes of the 2-edge-coloring of the complete graph given by and its complement. monoCount N k G counts the monochromatic -sets of a graph on labeled vertices, and NoMonoK k G asserts that contains none of them: neither a -clique nor an independent -set. The absence of monochromatic -sets on vertices is exactly the content of Erdős's lower bound . This file supplies the vocabulary used by all theorems of the mission.
Definition code
import Mathlib
namespace Erdos1947
/-- A `k`-element vertex subset is **monochromatic** in `G` when it is either a
`k`-clique or an independent set of size `k` — i.e. it is monochromatic in the
two-coloring of the complete graph given by `G` and its complement. -/
def MonochromaticK {V : Type} (k : ℕ) (G : SimpleGraph V) (s : Finset V) : Prop :=
s.card = k ∧ (G.IsClique s ∨ G.IsIndepSet s)
/-- The number of monochromatic `k`-sets of `G` on `N` vertices. -/
noncomputable def monoCount (N k : ℕ) (G : SimpleGraph (Fin N)) : ℕ := by
classical
exact (Finset.univ.filter (fun s : Finset (Fin N) => MonochromaticK k G s)).card
/-- A graph with **no monochromatic `k`-set**: it contains neither a `k`-clique
nor an independent set of size `k`. -/
def NoMonoK {V : Type} (k : ℕ) (G : SimpleGraph V) : Prop :=
∀ s : Finset V, ¬ MonochromaticK k G s
end Erdos1947Source
Erdős, Some remarks on the theory of graphs, Bulletin of the American Mathematical Society 53(4) (1947) 292–294, https://doi.org/10.1090/S0002-9904-1947-08785-X — main construction (the lower bound R(k) > 2^(k/2)).
Human review
Confirmed by the mission captain (proposal self-audit).