Formalizing Structural Graph Theory in Lean 4

Catalog/Sparsity/Ramsey/Full.lean
1import Mathlib.Combinatorics.SimpleGraph.Clique
2import Mathlib.Combinatorics.SimpleGraph.Maps
3import Mathlib.Data.Fintype.Card
4
5namespace Catalog.Sparsity.Ramsey
6
7open SimpleGraph Finset
8
9/-! ## Ramsey's theorem (two colors)
10
11We prove the classical Ramsey theorem by well-founded induction on `a + b`.
12The bound is `R(a, b) ≤ R(a-1, b) + R(a, b-1)` with `R(0, _) = 0`.
13-/
14
15/-- The complement of an induced subgraph equals the induced subgraph
16of the complement. -/
17theorem compl_induce_eq {V : Type} {s : Set V} (G : SimpleGraph V) :
18 (G.induce s)ᶜ = Gᶜ.induce s := by
19 ext ⟨u, hu⟩ ⟨v, hv⟩
20 simp only [compl_adj, induce_adj, ne_eq, Subtype.mk.injEq]
21
22/-- Ramsey's theorem (two colors): for any `a b : ℕ` there exists `N` such that
23 every graph on at least `N` vertices either contains a clique of size `a` or
24 an independent set of size `b`. (Theorem 3.7) -/
25theorem ramsey (a b : ℕ) : ∃ N : ℕ,
26 ∀ {V : Type} [DecidableEq V] [Fintype V] (G : SimpleGraph V)
27 [DecidableRel G.Adj],
28 N ≤ Fintype.card V → ¬G.CliqueFree a ∨ ¬Gᶜ.CliqueFree b := by
29 classical
30 suffices h : ∀ n a b, a + b = n →
31 ∃ N : ℕ, ∀ {V : Type} [DecidableEq V] [Fintype V] (G : SimpleGraph V)
32 [DecidableRel G.Adj],
33 N ≤ Fintype.card V → ¬G.CliqueFree a ∨ ¬Gᶜ.CliqueFree b from
34 h (a + b) a b rfl
35 intro n
36 induction n using Nat.strongRecOn with
37 | _ n ih =>
38 intro a b hab
39 -- Base cases: a = 0 or b = 0
40 match a, b, hab with
41 | 0, _, _ =>
42 exact ⟨0, fun _ _ _ => Or.inl not_cliqueFree_zero⟩
43 | _, 0, _ =>
44 exact ⟨0, fun _ _ _ => Or.inr not_cliqueFree_zero⟩
45 | a' + 1, b' + 1, hab =>
46 -- IH for (a', b'+1) and (a'+1, b')
47 obtain ⟨N1, hN1⟩ := ih _ (by omega) a' (b' + 1) rfl
48 obtain ⟨N2, hN2⟩ := ih _ (by omega) (a' + 1) b' rfl
49 refine ⟨N1 + N2 + 1,
50 fun {V} [DecidableEq V] [Fintype V] G [DecidableRel G.Adj] hcard => ?_⟩
51 -- Pick a vertex v
52 have hne : 0 < Fintype.card V := by omega
53 obtain ⟨v⟩ := Fintype.card_pos_iff.mp hne
54 -- Neighbors and non-neighbors of v
55 set A := G.neighborFinset v with hA_def
56 set B := Finset.univ.erase v \ A with hB_def
57 -- A ⊆ univ.erase v (since v is not its own neighbor)
58 have hA_sub : A ⊆ Finset.univ.erase v := by
59 intro w hw
60 rw [Finset.mem_erase]
61 exact ⟨(G.ne_of_adj ((G.mem_neighborFinset v w).mp hw)).symm, Finset.mem_univ _⟩
62 -- |A| + |B| = |V| - 1
63 have hAB : A.card + B.card + 1 = Fintype.card V := by
64 have h1 : B ∪ A = Finset.univ.erase v :=
65 Finset.sdiff_union_of_subset hA_sub
66 have h2 : Disjoint B A := Finset.sdiff_disjoint
67 have h3 := Finset.card_union_of_disjoint h2
68 have h4 := Finset.card_erase_of_mem (Finset.mem_univ v)
69 rw [h1] at h3; rw [Finset.card_univ] at h4
70 omega
71 -- Pigeonhole: |A| ≥ N1 or |B| ≥ N2
72 rcases Nat.lt_or_ge A.card N1 with hAlt | hAge
73 · -- Case 2: |A| < N1, so |B| ≥ N2
74 have hBge : N2 ≤ B.card := by omega
75 have hcB : N2 ≤ Fintype.card ↑(B : Set V) := by
76 rw [Fintype.card_of_finset' B (fun x => Iff.rfl)]
77 exact hBge
78 rcases hN2 (G.induce (↑B : Set V)) hcB with h1 | h2
79 · exact Or.inl <| mt
80 (SimpleGraph.CliqueFree.comap
81 (G := G) (H := G.induce (↑B : Set V))
82 (SimpleGraph.Embedding.induce (G := G) (↑B : Set V)).isContained)
83 h1
84 · have h2' : ¬(Gᶜ.induce (↑B : Set V)).CliqueFree b' := by
85 simpa [compl_induce_eq G] using h2
86 obtain ⟨t, ht⟩ := Classical.not_forall.mp h2'
87 have ht : (Gᶜ.induce (↑B : Set V)).IsNClique b' t := not_not.mp ht
88 let t' : Finset V := t.map ⟨Subtype.val, Subtype.val_injective⟩
89 have ht_coe : (((⊤ : Subgraph Gᶜ).induce (↑B : Set V)).coe).IsNClique b' t := by
90 simpa [SimpleGraph.induce_eq_coe_induce_top] using ht
91 have ht' : Gᶜ.IsNClique b' t' := by
92 simpa [t'] using
93 (SimpleGraph.IsNClique.of_induce
94 (G := Gᶜ) (S := (⊤ : Subgraph Gᶜ)) (F := (↑B : Set V)) ht_coe)
95 have hv_adj : ∀ w ∈ t', Gᶜ.Adj v w := by
96 intro w hw
97 rcases Finset.mem_map.mp hw with ⟨x, hx, rfl⟩
98 have hxB : x.1 ∈ Finset.univ.erase v \ A := by
99 simpa [hB_def] using (show x.1 ∈ B from x.2)
100 have hxsdiff : x.1 ∈ Finset.univ.erase v ∧ x.1 ∉ A := by
101 exact Finset.mem_sdiff.mp hxB
102 have hxne : v ≠ x.1 := by
103 exact (Finset.mem_erase.mp hxsdiff.1).1.symm
104 have hxnotadj : ¬G.Adj v x.1 := by
105 intro hvx
106 exact hxsdiff.2 ((G.mem_neighborFinset v x.1).2 hvx)
107 rw [SimpleGraph.compl_adj]
108 exact ⟨hxne, hxnotadj⟩
109 exact Or.inr (ht'.insert hv_adj).not_cliqueFree
110 · -- Case 1: |A| ≥ N1 — apply IH to G.induce ↑A
111 have hcA : N1 ≤ Fintype.card ↑(A : Set V) := by
112 rw [Fintype.card_of_finset' A (fun x => Iff.rfl)]
113 exact hAge
114 rcases hN1 (G.induce (↑A : Set V)) hcA with h1 | h2
115 · -- Found a'-clique in induced subgraph — extend with v
116 obtain ⟨s, hs⟩ := Classical.not_forall.mp h1
117 have hs : (G.induce (↑A : Set V)).IsNClique a' s := not_not.mp hs
118 let s' : Finset V := s.map ⟨Subtype.val, Subtype.val_injective⟩
119 have hs_coe : (((⊤ : Subgraph G).induce (↑A : Set V)).coe).IsNClique a' s := by
120 simpa [SimpleGraph.induce_eq_coe_induce_top] using hs
121 have hs' : G.IsNClique a' s' := by
122 simpa [s'] using
123 (SimpleGraph.IsNClique.of_induce
124 (G := G) (S := (⊤ : Subgraph G)) (F := (↑A : Set V)) hs_coe)
125 have hv_adj : ∀ w ∈ s', G.Adj v w := by
126 intro w hw
127 rcases Finset.mem_map.mp hw with ⟨x, hx, rfl⟩
128 have hxA : x.1 ∈ G.neighborFinset v := by
129 exact x.2
130 simpa using (G.mem_neighborFinset v x.1).mp hxA
131 exact Or.inl (hs'.insert hv_adj).not_cliqueFree
132 · -- Found (b'+1)-independent set — transfer to Gᶜ
133 have h2' : ¬(Gᶜ.induce (↑A : Set V)).CliqueFree (b' + 1) := by
134 simpa [compl_induce_eq G] using h2
135 exact Or.inr <| mt
136 (SimpleGraph.CliqueFree.comap
137 (G := Gᶜ) (H := Gᶜ.induce (↑A : Set V))
138 (SimpleGraph.Embedding.induce (G := Gᶜ) (↑A : Set V)).isContained)
139 h2'
140
141end Catalog.Sparsity.Ramsey
142