Formalizing Structural Graph Theory in Lean 4

Catalog/Sparsity/MulticolorRamsey/Full.lean
1import Mathlib.Combinatorics.SimpleGraph.Clique
2import Mathlib.Data.Fintype.EquivFin
3import Catalog.Sparsity.Ramsey.Full
4
5namespace Catalog.Sparsity.MulticolorRamsey
6
7/-- Multicolor Ramsey theorem: for any list of natural numbers
8 `sizes = [n₁, …, nₖ]`, there exists `N` such that every `k`-coloring of
9 edges of a complete graph on at least `N` vertices yields a monochromatic
10 clique of size `nᵢ` in color `i`, for some `i`. (Theorem 3.8) -/
11theorem multicolorRamsey (sizes : List ℕ) (hk : sizes ≠ []) :
12 ∃ N : ℕ, ∀ {V : Type} [DecidableEq V] [Fintype V],
13 N ≤ Fintype.card V →
14 ∀ (c : Sym2 V → Fin sizes.length),
15 ∃ (i : Fin sizes.length) (S : Finset V),
16 sizes.get i ≤ S.card ∧
17 (↑S : Set V).Pairwise (fun u v => c s(u, v) = i) := by
18 classical
19 induction sizes with
20 | nil =>
21 cases hk rfl
22 | cons n rest ih =>
23 cases rest with
24 | nil =>
25 refine ⟨n, ?_⟩
26 intro V _ _ hcard c
27 refine ⟨⟨0, by simp⟩, Finset.univ, ?_, ?_⟩
28 · simpa
29 · intro u _ v _ _
30 apply Fin.ext
31 simp
32 | cons m tail =>
33 obtain ⟨Nrest, hrest⟩ := ih (by simp)
34 obtain ⟨N, hN⟩ := Catalog.Sparsity.Ramsey.ramsey n Nrest
35 refine ⟨N, ?_⟩
36 intro V _ _ hcard c
37 let G : SimpleGraph V := {
38 Adj := fun u v => u ≠ v ∧ c s(u, v) = 0
39 symm := by
40 intro u v huv
41 exact ⟨huv.1.symm, by simpa [Sym2.eq_swap] using huv.2⟩
42 loopless := ⟨fun v hv => hv.1 rfl⟩
43 }
44 letI : DecidableRel G.Adj := fun u v => by
45 dsimp [G]
46 infer_instance
47 rcases hN G hcard with hClique | hCompl
48 · let f : (⊤ : SimpleGraph (Fin n)) ↪g G :=
49 SimpleGraph.topEmbeddingOfNotCliqueFree hClique
50 refine ⟨0, Finset.univ.map f.toEmbedding, ?_, ?_⟩
51 · simp
52 · intro u hu v hv huv
53 rcases Finset.mem_map.mp hu with ⟨a, _, rfl⟩
54 rcases Finset.mem_map.mp hv with ⟨b, _, rfl⟩
55 have hab : a ≠ b := by
56 intro hab
57 apply huv
58 simp [hab]
59 have hadj : G.Adj (f a) (f b) := by
60 exact (f.map_adj_iff).2 (by simpa [SimpleGraph.top_adj] using hab)
61 exact hadj.2
62 · let f : (⊤ : SimpleGraph (Fin Nrest)) ↪g Gᶜ :=
63 SimpleGraph.topEmbeddingOfNotCliqueFree hCompl
64 let colorRest :
65 Fin Nrest → Fin Nrest → Fin ((m :: tail).length) :=
66 fun a b =>
67 Fin.predAbove (0 : Fin ((m :: tail).length)) (c s(f a, f b))
68 have hcolorRest :
69 ∀ a b : Fin Nrest, colorRest a b = colorRest b a := by
70 intro a b
71 unfold colorRest
72 rw [Sym2.eq_swap]
73 let cRest : Sym2 (Fin Nrest) → Fin (List.length (m :: tail)) :=
74 Sym2.lift ⟨colorRest, hcolorRest⟩
75 obtain ⟨i, S, hsize, hpair⟩ := hrest (V := Fin Nrest) (by simp) cRest
76 refine ⟨i.succ, S.map f.toEmbedding, ?_, ?_⟩
77 · simpa using hsize
78 · intro u hu v hv huv
79 rcases Finset.mem_map.mp hu with ⟨a, ha, rfl⟩
80 rcases Finset.mem_map.mp hv with ⟨b, hb, rfl⟩
81 have hab : a ≠ b := by
82 intro hab
83 apply huv
84 simpa [hab]
85 have hpair' : cRest s(a, b) = i := hpair ha hb hab
86 have hadjCompl : Gᶜ.Adj (f a) (f b) := by
87 exact (f.map_adj_iff).2 (by simpa [SimpleGraph.top_adj] using hab)
88 rw [SimpleGraph.compl_adj] at hadjCompl
89 have hcolor_ne_zero : c s(f a, f b) ≠ 0 := by
90 intro hzero
91 exact hadjCompl.2 ⟨hadjCompl.1, hzero⟩
92 have hpred :
93 Fin.predAbove (0 : Fin ((m :: tail).length)) (c s(f a, f b)) = i := by
94 simpa [cRest, colorRest] using hpair'
95 calc
96 c s(f a, f b) =
97 Fin.succ (Fin.predAbove (0 : Fin ((m :: tail).length)) (c s(f a, f b))) := by
98 symm
99 exact Fin.succ_predAbove_zero hcolor_ne_zero
100 _ = i.succ := by rw [hpred]
101
102end Catalog.Sparsity.MulticolorRamsey
103