From a1aab669373c45e25e454f3019b0248add48b6fc Mon Sep 17 00:00:00 2001 From: robo7179 Date: Tue, 21 Apr 2026 23:56:27 +0530 Subject: [PATCH 1/2] Feat(SimpleGraph/Coloring/VertexColoring): Matching is 2 colorable --- .../SimpleGraph/Coloring/VertexColoring.lean | 50 +++++++++++++++++++ 1 file changed, 50 insertions(+) diff --git a/Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean b/Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean index 99df79691738ff..35f750d51bc499 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean @@ -523,6 +523,56 @@ theorem CompleteBipartiteGraph.chromaticNumber {V W : Type*} [Nonempty V] [Nonem · exact ⟨_, he'⟩ · simpa using two_lt_card_iff.2 ⟨_, _, _, C.valid h, he, he'⟩ +theorem colorable_two_of_maxDegree_le_one [Fintype V] [DecidableEq V] [DecidableRel G.Adj] + (h : G.maxDegree = 1) : G.Colorable 2 := by + have unique_neighbor : ∀ x y z, G.Adj x y → G.Adj x z → y = z := by + intro x y z hxy hxz + by_contra h_neq + have h_sub : ({y, z} : Finset V) ⊆ G.neighborFinset x := by + intro a ha + simp only [Finset.mem_insert, Finset.mem_singleton] at ha + rcases ha with rfl | rfl + · rw [G.mem_neighborFinset] + exact hxy + · rw [G.mem_neighborFinset] + exact hxz + have h_card := Finset.card_le_card h_sub + rw [Finset.card_pair h_neq] at h_card + have h_deg : (G.neighborFinset x).card ≤ 1 := by + calc (G.neighborFinset x).card = G.degree x := rfl + _ ≤ G.maxDegree := G.degree_le_maxDegree x + _ = 1 := h + omega + letI : ∀ (p : Prop), Decidable p := fun _ => Classical.propDecidable _ + have e : V ≃ Fin (Fintype.card V) := Fintype.equivFin V + let c : V → Fin 2 := fun v => + if ∃ w, G.Adj v w ∧ e w < e v then 1 else 0 + use c + intro v w h_adj + dsimp [c] + rcases lt_trichotomy (e v) (e w) with h_lt | h_eq | h_gt + · have hw_cond : ∃ u, G.Adj w u ∧ e u < e w := ⟨v, h_adj.symm, h_lt⟩ + rw [if_pos hw_cond] + have hv_cond : ¬ ∃ u, G.Adj v u ∧ e u < e v := by + rintro ⟨u, h_adj_vu, h_lt_uv⟩ + have h_eq_uv := unique_neighbor v w u h_adj h_adj_vu + rw [← h_eq_uv] at h_lt_uv + exact lt_asymm h_lt h_lt_uv + rw [if_neg hv_cond] + simp + · have h_vw : v = w := e.injective h_eq + have h_ne := G.ne_of_adj h_adj + exact (h_ne h_vw).elim + · have hv_cond : ∃ u, G.Adj v u ∧ e u < e v := ⟨w, h_adj, h_gt⟩ + rw [if_pos hv_cond] + have hw_cond : ¬ ∃ u, G.Adj w u ∧ e u < e w := by + rintro ⟨u, h_adj_wu, h_lt_uw⟩ + have h_eq_uw := unique_neighbor w v u h_adj.symm h_adj_wu + rw [← h_eq_uw] at h_lt_uw + exact lt_asymm h_gt h_lt_uw + rw [if_neg hw_cond] + simp + /-! ### Cliques -/ theorem IsClique.card_le_of_colorable {s : Finset V} (h : G.IsClique s) (hc : G.Colorable n) : From 86612768320dc40f54e3fadbfc8cca1e690eb597 Mon Sep 17 00:00:00 2001 From: robo7179 Date: Wed, 22 Apr 2026 01:36:49 +0530 Subject: [PATCH 2/2] Corrected build errors --- Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean b/Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean index 35f750d51bc499..87d4cc1bd20d44 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean @@ -523,8 +523,9 @@ theorem CompleteBipartiteGraph.chromaticNumber {V W : Type*} [Nonempty V] [Nonem · exact ⟨_, he'⟩ · simpa using two_lt_card_iff.2 ⟨_, _, _, C.valid h, he, he'⟩ -theorem colorable_two_of_maxDegree_le_one [Fintype V] [DecidableEq V] [DecidableRel G.Adj] +theorem colorable_two_of_maxDegree_le_one [Fintype V] [DecidableRel G.Adj] (h : G.maxDegree = 1) : G.Colorable 2 := by + classical have unique_neighbor : ∀ x y z, G.Adj x y → G.Adj x z → y = z := by intro x y z hxy hxz by_contra h_neq