Catalog.Sparsity.MulticolorRamsey

Theorem

Let \(n_1, \ldots, n_k \in \mathbb{N}\). There exists a number \(R(n_1, \ldots, n_k)\) such that for every coloring of the edges of a complete graph on \(R(n_1, \ldots, n_k)\) vertices with \(k\) different colors \(c_1, \ldots, c_k\) we will find for some \(1 \leq i \leq k\) a clique on \(n_i\) vertices all of whose edges are colored with color \(c_i\).

Review notes

The source states the multicolor Ramsey theorem for \(k\) colors with sizes \(n_1, \ldots, n_k\). The Lean formulation:

Encodes the sizes as a List ℕ with a non-empty hypothesis.
A \(k\)-coloring of edges of \(K_N\) is a function c : Sym2 V → Fin sizes.length assigning a color to each unordered pair of vertices. Pairs \(\{v, v\}\) (self-loops) are colored but irrelevant since they cannot appear in a pairwise-distinct clique.
The conclusion asks for a monochromatic clique: a Finset V whose pairwise edge colors all equal some color \(i\), with cardinality at least sizes.get i.

The proof (Phase 4) follows by induction on the number of colors, reducing each step to the two-color case (Catalog.Sparsity.Ramsey).

Catalog/Sparsity/MulticolorRamsey/Contract.lean (full)

1	import Mathlib.Combinatorics.SimpleGraph.Clique
2
3	namespace Catalog.Sparsity.MulticolorRamsey
4
5	/-- Multicolor Ramsey theorem: for any list of natural numbers
6	`sizes = [n₁, …, nₖ]`, there exists `N` such that every `k`-coloring of
7	edges of a complete graph on at least `N` vertices yields a monochromatic
8	clique of size `nᵢ` in color `i`, for some `i`. (Theorem 3.8) -/
9	axiom multicolorRamsey (sizes : List ℕ) (hk : sizes ≠ []) :
10	∃ N : ℕ, ∀ {V : Type} [DecidableEq V] [Fintype V],
11	N ≤ Fintype.card V →
12	∀ (c : Sym2 V → Fin sizes.length),
13	∃ (i : Fin sizes.length) (S : Finset V),
14	sizes.get i ≤ S.card ∧
15	(↑S : Set V).Pairwise (fun u v => c s(u, v) = i)
16
17	end Catalog.Sparsity.MulticolorRamsey
18

Dependencies

Proof

Catalog.Sparsity.Ramsey

Used By

Proof