From ba44f80656986dd1eb7d1656e6f77ead7926016a Mon Sep 17 00:00:00 2001 From: Juan Pablo Traverso Gianini <13575211+jtraverso@users.noreply.github.com> Date: Mon, 19 Oct 2026 08:19:14 -0300 Subject: [PATCH 1/6] feat: add classical graph colouring collection --- LeanPool/ClassicalGraphColouring.lean | 62 ++++ .../Galvin/GaleShapley.lean | 102 ++++++ .../Galvin/Galvin.lean | 114 ++++++ .../Galvin/Kernel.lean | 122 +++++++ .../Galvin/Orientation.lean | 241 +++++++++++++ LeanPool/ClassicalGraphColouring/Imports.lean | 16 + .../ClassicalGraphColouring/Konig/Basic.lean | 248 ++++++++++++++ .../Orientations/GallaiRoy.lean | 170 +++++++++ .../Spectrum/Bounds.lean | 324 ++++++++++++++++++ .../projects/classical-graph-colouring.yaml | 121 +++++++ 10 files changed, 1520 insertions(+) create mode 100644 LeanPool/ClassicalGraphColouring.lean create mode 100644 LeanPool/ClassicalGraphColouring/Galvin/GaleShapley.lean create mode 100644 LeanPool/ClassicalGraphColouring/Galvin/Galvin.lean create mode 100644 LeanPool/ClassicalGraphColouring/Galvin/Kernel.lean create mode 100644 LeanPool/ClassicalGraphColouring/Galvin/Orientation.lean create mode 100644 LeanPool/ClassicalGraphColouring/Imports.lean create mode 100644 LeanPool/ClassicalGraphColouring/Konig/Basic.lean create mode 100644 LeanPool/ClassicalGraphColouring/Orientations/GallaiRoy.lean create mode 100644 LeanPool/ClassicalGraphColouring/Spectrum/Bounds.lean create mode 100644 LeanPool/projects/classical-graph-colouring.yaml diff --git a/LeanPool/ClassicalGraphColouring.lean b/LeanPool/ClassicalGraphColouring.lean new file mode 100644 index 000000000..252aeca9b --- /dev/null +++ b/LeanPool/ClassicalGraphColouring.lean @@ -0,0 +1,62 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import LeanPool.ClassicalGraphColouring.Konig.Basic +public import LeanPool.ClassicalGraphColouring.Galvin.Galvin +public import LeanPool.ClassicalGraphColouring.Orientations.GallaiRoy +public import LeanPool.ClassicalGraphColouring.Spectrum.Bounds + +/-! +# Classical graph colouring by degree, orientations, lists and eigenvalues + +Kőnig's edge-colouring theorem supplies a proper colouring of a finite bipartite graph with +`Δ(G)` colours. Galvin's orientation and kernel argument upgrades this to a colouring from +arbitrary edge lists of size at least `Δ(G)`. The development also proves the Gale–Shapley +stable-matching theorem used to construct the kernels and deduces the Dinitz array theorem. +Gallai–Hasse–Roy–Vitaver relates proper colourings to longest directed paths in orientations. +Wilf's and Hoffman's bounds compare the chromatic and independence numbers with adjacency +eigenvalues. Two interface corollaries below transfer the spectral colouring bounds to directed +path statements. + +The proof of Kőnig's theorem reuses `LeanPool.Vizing` directly. The matching-cover and finite +poset results from the registered Kőnig source are already available in +`LeanPool.ClassicalMatchingFactors` and are not duplicated here. + +Source: doi:10.1006/jctb.1995.1011, +url:https://github.com/jtraverso/galvin-dinitz/tree/0aa98fc17e1e96ec408f7bad3198ce37a08d26fc +Authors: Juan Pablo Traverso Gianini +Status: verified +Main declarations: `Konig.lineGraph_colorable_of_colorable_two`, `Galvin.galvin`, + `GallaiRoy.colorable_of_orientation`, `SpectralBounds.hoffman_chromatic` +Tags: graph-theory, graph-colouring, edge-colouring, orientations, spectral-graph-theory +MSC: 05C15, 05C20, 05C50, 91B68 +-/ + +@[expose] public section + +open SimpleGraph + +namespace ClassicalGraphColouring + +/-- Hoffman's chromatic lower bound also bounds the directed path length of every orientation. -/ +theorem hoffman_le_directed_path_bound {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V] + (G : SimpleGraph V) [DecidableRel G.Adj] (hA : (G.adjMatrix ℝ).IsHermitian) + (hE : G.edgeSet.Nonempty) (o : V → V → Prop) (ho : GallaiRoy.IsOrientation G o) + (k : ℕ) (hk : ∀ (m : ℕ) (f : Fin m → V), GallaiRoy.IsDirectedPath o f → m ≤ k) : + 1 - (⨆ i, hA.eigenvalues i) / (⨅ i, hA.eigenvalues i) ≤ k := + SpectralBounds.hoffman_chromatic G hA hE + (GallaiRoy.colorable_of_orientation G o ho k hk) + +/-- Wilf's spectral colouring bound gives an orientation with the same bound on directed paths. -/ +theorem exists_orientation_of_wilf_bound {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V] + (G : SimpleGraph V) [DecidableRel G.Adj] (hA : (G.adjMatrix ℝ).IsHermitian) : + ∃ o : V → V → Prop, GallaiRoy.IsOrientation G o ∧ + ∀ (m : ℕ) (f : Fin m → V), GallaiRoy.IsDirectedPath o f → + m ≤ ⌊⨆ i, hA.eigenvalues i⌋₊ + 1 := + GallaiRoy.exists_orientation_of_colorable G _ (SpectralBounds.wilf G hA) + +end ClassicalGraphColouring diff --git a/LeanPool/ClassicalGraphColouring/Galvin/GaleShapley.lean b/LeanPool/ClassicalGraphColouring/Galvin/GaleShapley.lean new file mode 100644 index 000000000..741151cb1 --- /dev/null +++ b/LeanPool/ClassicalGraphColouring/Galvin/GaleShapley.lean @@ -0,0 +1,102 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex +public import Mathlib.Tactic + +/-! +# Existence of stable matchings + +An inductive proof of the Gale–Shapley theorem. If no two men share the same favourite woman, +matching every man to his favourite is stable. Otherwise two men `m₁ ≠ m₂` share the favourite +`w`; if `w` prefers `m₁`, the pair `(m₂, w)` may be deleted: in a stable matching of the smaller +instance, `w` is matched to someone at least as good as `m₁` (because `m₁` cannot prefer anybody +to `w`), so the deleted pair is blocked. +-/ + +@[expose] public section + +namespace Galvin + +/-- `IsTop E r m w`: `w` is an acceptable partner of `m` of minimal rank. -/ +def IsTop {M W : Type*} (E : M → W → Prop) (rm : M → W → ℕ) (m : M) (w : W) : Prop := + E m w ∧ ∀ w', E m w' → rm m w ≤ rm m w' + +/-- The stable matching property. -/ +def IsStable {M W : Type*} (E : M → W → Prop) (rm : M → W → ℕ) (rw : W → M → ℕ) + (μ : M → W → Prop) : Prop := + (∀ m w, μ m w → E m w) ∧ + (∀ m w w', μ m w → μ m w' → w = w') ∧ (∀ m m' w, μ m w → μ m' w → m = m') ∧ + ∀ m w, E m w → ¬ μ m w → + (∃ w', μ m w' ∧ rm m w' < rm m w) ∨ (∃ m', μ m' w ∧ rw w m' < rw w m) + +theorem exists_isTop {M W : Type*} (E : M → W → Prop) (rm : M → W → ℕ) (m : M) (w : W) + (h : E m w) : ∃ w', IsTop E rm m w' := by + classical + have hex : ∃ k, ∃ w, E m w ∧ rm m w = k := ⟨_, w, h, rfl⟩ + obtain ⟨w', hw', hk⟩ := Nat.find_spec hex + refine ⟨w', hw', fun v hv => ?_⟩ + rw [hk] + exact Nat.find_min' hex ⟨v, hv, rfl⟩ + +theorem isStable_of_removal {M W : Type*} (E : M → W → Prop) + (rm : M → W → ℕ) (rw : W → M → ℕ) + {m₁ m₂ : M} {w : W} (h₁ : IsTop E rm m₁ w) (hlt : rw w m₁ < rw w m₂) + (μ : M → W → Prop) + (hμ : IsStable (fun m v => E m v ∧ ¬ (m = m₂ ∧ v = w)) rm rw μ) (hne : m₁ ≠ m₂) : + IsStable E rm rw μ := by + obtain ⟨hsub, hm, hw, hst⟩ := hμ + refine ⟨fun m v h => (hsub m v h).1, hm, hw, fun m v hE hnot => ?_⟩ + by_cases hrem : m = m₂ ∧ v = w + · obtain ⟨rfl, rfl⟩ := hrem + right + by_cases hμ₁ : μ m₁ v + · exact ⟨m₁, hμ₁, hlt⟩ + · rcases hst m₁ v ⟨h₁.1, fun h => hne h.1⟩ hμ₁ with ⟨w', hw', hr⟩ | ⟨m', hm', hr⟩ + · exact absurd (h₁.2 w' (hsub _ _ hw').1) (not_le.mpr hr) + · exact ⟨m', hm', hr.trans hlt⟩ + · exact hst m v ⟨hE, hrem⟩ hnot + +theorem exists_isStable {M W : Type*} [Finite M] [Finite W] + (rm : M → W → ℕ) (rw : W → M → ℕ) (hrm : ∀ m, Function.Injective (rm m)) + (hrw : ∀ w, Function.Injective (rw w)) : + ∀ (n : ℕ) (E : M → W → Prop), {p : M × W | E p.1 p.2}.ncard = n → + ∃ μ, IsStable E rm rw μ := by + intro n + induction n using Nat.strong_induction_on with + | _ n ih => + intro E hn + by_cases hsh : ∃ m₁ m₂ w, m₁ ≠ m₂ ∧ IsTop E rm m₁ w ∧ IsTop E rm m₂ w + · obtain ⟨m₁, m₂, w, hne, h₁, h₂⟩ := hsh + have key : ∀ a b : M, a ≠ b → IsTop E rm a w → IsTop E rm b w → rw w a < rw w b → + ∃ μ, IsStable E rm rw μ := by + intro a b hab ha hb hlt + let E' : M → W → Prop := fun m v => E m v ∧ ¬ (m = b ∧ v = w) + have hlt' : {p : M × W | E' p.1 p.2}.ncard < n := by + rw [← hn] + apply Set.ncard_lt_ncard _ (Set.toFinite _) + refine ⟨fun p hp => hp.1, fun h => ?_⟩ + have := h (show (b, w) ∈ {p : M × W | E p.1 p.2} from hb.1) + exact this.2 ⟨rfl, rfl⟩ + obtain ⟨μ, hμ⟩ := ih _ hlt' E' rfl + exact ⟨μ, isStable_of_removal E rm rw ha hlt μ hμ hab⟩ + rcases lt_or_gt_of_ne (fun h => hne (hrw w h)) with h | h + · exact key m₁ m₂ hne h₁ h₂ h + · exact key m₂ m₁ (Ne.symm hne) h₂ h₁ h + · push Not at hsh + refine ⟨IsTop E rm, fun m w h => h.1, fun m w w' h h' => ?_, fun m m' w h h' => ?_, + fun m w hE hnot => ?_⟩ + · exact hrm m (le_antisymm (h.2 _ h'.1) (h'.2 _ h.1)) + · by_contra hc + exact hsh m m' w hc h h' + · obtain ⟨w', hw'⟩ := exists_isTop E rm m w hE + left + refine ⟨w', hw', lt_of_le_of_ne (hw'.2 w hE) fun heq => ?_⟩ + rw [hrm m heq] at hw' + exact hnot hw' + +end Galvin diff --git a/LeanPool/ClassicalGraphColouring/Galvin/Galvin.lean b/LeanPool/ClassicalGraphColouring/Galvin/Galvin.lean new file mode 100644 index 000000000..dc2f65881 --- /dev/null +++ b/LeanPool/ClassicalGraphColouring/Galvin/Galvin.lean @@ -0,0 +1,114 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex +public import Mathlib.Tactic +public import LeanPool.ClassicalGraphColouring.Konig.Basic +public import LeanPool.ClassicalGraphColouring.Galvin.Orientation + +/-! +# Galvin's theorem, the Dinitz problem and stable matchings + +* `Galvin.gale_shapley`: **Gale–Shapley (1962).** Let `E` be a bipartite acceptability relation + between finite sets `M` and `W`, and let every element rank its potential partners by an + injective rank function (smaller rank = preferred). Then there is a *stable matching*: a + matching `μ ⊆ E` such that every acceptable pair `(m, w)` outside `μ` is blocked, i.e. `m` is + matched to someone it prefers to `w`, or `w` is matched to someone it prefers to `m`. +* `Galvin.galvin`: **Galvin (1995).** The list chromatic index of a finite bipartite graph equals + its maximum degree: if every edge `e` of a bipartite graph `G` has a list of at least `Δ(G)` + colours, there is a proper edge colouring (a colouring of Mathlib's `SimpleGraph.lineGraph`) + choosing the colour of every edge from its list. +* `Galvin.dinitz`: **the Dinitz problem.** If every cell of an `n × n` array has a list of at least + `n` symbols, one can choose a symbol from each list so that the symbols in every row and in every + column are distinct. +-/ + +@[expose] public section + +namespace Galvin + +/-- **Gale–Shapley (1962).** For a bipartite acceptability relation `E` between finite sets `M` +and `W`, with strict preferences given by injective rank functions (`rm m w < rm m w'` means that +`m` prefers `w` to `w'`), there is a stable matching. -/ +theorem gale_shapley {M W : Type*} [Finite M] [Finite W] (E : M → W → Prop) + (rm : M → W → ℕ) (rw : W → M → ℕ) (hrm : ∀ m, Function.Injective (rm m)) + (hrw : ∀ w, Function.Injective (rw w)) : + ∃ μ : M → W → Prop, (∀ m w, μ m w → E m w) ∧ + (∀ m w w', μ m w → μ m w' → w = w') ∧ (∀ m m' w, μ m w → μ m' w → m = m') ∧ + ∀ m w, E m w → ¬ μ m w → + (∃ w', μ m w' ∧ rm m w' < rm m w) ∨ (∃ m', μ m' w ∧ rw w m' < rw w m) := by + exact exists_isStable rm rw hrm hrw _ E rfl + +/-- **Galvin's theorem (1995).** If every edge of a finite bipartite graph `G` has a list of at +least `Δ(G)` colours, then `G` has a proper edge colouring choosing every colour from the list of +its edge. -/ +theorem galvin {V Color : Type*} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] + (hG : G.Colorable 2) (lists : G.edgeSet → Finset Color) + (hLists : ∀ e, G.maxDegree ≤ (lists e).card) : + ∃ coloring : G.lineGraph.Coloring Color, ∀ e, coloring e ∈ lists e := by + classical + obtain ⟨c⟩ := hG + obtain ⟨φ⟩ := Konig.lineGraph_colorable_of_colorable_two G ⟨c⟩ + exact exists_listColoring G.lineGraph (arc c φ) (hasKernels_arc c φ) lists + fun e => lt_of_lt_of_le (card_arc_lt c φ e) (hLists e) + +/-- **The Dinitz problem** (Galvin 1995). If every cell of an `n × n` array has a list of at least +`n` symbols, there is a choice of one symbol from each list with all symbols in each row distinct +and all symbols in each column distinct. -/ +theorem dinitz {Symbol : Type*} (n : ℕ) (lists : Fin n → Fin n → Finset Symbol) + (hLists : ∀ i j, n ≤ (lists i j).card) : + ∃ f : Fin n → Fin n → Symbol, (∀ i j, f i j ∈ lists i j) ∧ + (∀ i j j', j ≠ j' → f i j ≠ f i j') ∧ (∀ i i' j, i ≠ i' → f i j ≠ f i' j) := by + classical + let G := completeBipartiteGraph (Fin n) (Fin n) + have hG : G.Colorable 2 := + ⟨SimpleGraph.Coloring.mk (fun v => Sum.elim (fun _ => 0) (fun _ => 1) v) (by + rintro (i | i) (j | j) h <;> simp [G] at h ⊢)⟩ + have hdeg : G.maxDegree ≤ n := by + refine G.maxDegree_le_of_forall_degree_le n fun v => ?_ + rw [← SimpleGraph.card_neighborFinset_eq_degree] + rcases v with i | i + · calc (G.neighborFinset (Sum.inl i)).card + ≤ (Finset.univ.image (Sum.inr : Fin n → _)).card := + Finset.card_le_card fun w hw => by + rcases w with j | j <;> simp [G] at hw ⊢ + _ ≤ n := Finset.card_image_le.trans (by simp) + · calc (G.neighborFinset (Sum.inr i)).card + ≤ (Finset.univ.image (Sum.inl : Fin n → _)).card := + Finset.card_le_card fun w hw => by + rcases w with j | j <;> simp [G] at hw ⊢ + _ ≤ n := Finset.card_image_le.trans (by simp) + let cell : Fin n ⊕ Fin n → Fin n ⊕ Fin n → Finset Symbol := fun a b => + match a, b with + | Sum.inl i, Sum.inr j => lists i j + | Sum.inr j, Sum.inl i => lists i j + | _, _ => ∅ + have hcell : ∀ a b, cell a b = cell b a := by + rintro (i | i) (j | j) <;> rfl + let L : G.edgeSet → Finset Symbol := fun e => Sym2.lift ⟨cell, hcell⟩ e + have hL : ∀ e, G.maxDegree ≤ (L e).card := by + rintro ⟨e, he⟩ + induction e using Sym2.ind with + | _ a b => + refine hdeg.trans ?_ + rcases a with i | i <;> rcases b with j | j <;> + simp [G, L, cell, Sym2.lift_mk, hLists] at he ⊢ + obtain ⟨col, hcol⟩ := galvin G hG L hL + have hadj : ∀ i j, G.Adj (Sum.inl i) (Sum.inr j) := fun i j => by simp [G] + let edge : Fin n → Fin n → G.edgeSet := fun i j => ⟨s(Sum.inl i, Sum.inr j), hadj i j⟩ + refine ⟨fun i j => col (edge i j), fun i j => ?_, fun i j j' hjj => ?_, fun i i' j hii => ?_⟩ + · simpa [L, edge, cell, Sym2.lift_mk] using hcol (edge i j) + · refine col.valid ?_ + rw [SimpleGraph.lineGraph_adj_iff_exists] + refine ⟨fun h => hjj ?_, Sum.inl i, by simp [edge], by simp [edge]⟩ + simpa [edge] using congrArg Subtype.val h + · refine col.valid ?_ + rw [SimpleGraph.lineGraph_adj_iff_exists] + refine ⟨fun h => hii ?_, Sum.inr j, by simp [edge], by simp [edge]⟩ + simpa [edge] using congrArg Subtype.val h + +end Galvin diff --git a/LeanPool/ClassicalGraphColouring/Galvin/Kernel.lean b/LeanPool/ClassicalGraphColouring/Galvin/Kernel.lean new file mode 100644 index 000000000..a5cc949a3 --- /dev/null +++ b/LeanPool/ClassicalGraphColouring/Galvin/Kernel.lean @@ -0,0 +1,122 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex +public import Mathlib.Tactic + +/-! +# List colourings from kernels + +Let `D` be a relation (the arcs of an orientation) on the vertices of a finite graph `G`. Suppose +every finite set `S` of vertices has a *kernel*: a `G`-independent `K ⊆ S` such that every +`x ∈ S \ K` has an arc `D x y` into `K`. If the list of every vertex is longer than its +out-degree, then there is a proper colouring choosing every colour from the corresponding list. +-/ + +@[expose] public section + +namespace Galvin + +open Finset + +/-- Every finite set of vertices has a kernel with respect to the arcs `D`. -/ +def HasKernels {α : Type*} (G : SimpleGraph α) (D : α → α → Prop) : Prop := + ∀ S : Finset α, ∃ K ⊆ S, (∀ x ∈ K, ∀ y ∈ K, ¬ G.Adj x y) ∧ + ∀ x ∈ S, x ∉ K → ∃ y ∈ K, D x y + +theorem exists_listColoring_on {α Color : Type*} [Nonempty Color] + (G : SimpleGraph α) (D : α → α → Prop) [DecidableRel D] (hK : HasKernels G D) : + ∀ (n : ℕ) (U : Finset α), U.card = n → ∀ L : α → Finset Color, + (∀ x ∈ U, (U.filter (D x ·)).card < (L x).card) → + ∃ c : α → Color, (∀ x ∈ U, c x ∈ L x) ∧ + ∀ x ∈ U, ∀ y ∈ U, G.Adj x y → c x ≠ c y := by + classical + intro n + induction n using Nat.strong_induction_on with + | _ n ih => + intro U hn L hL + rcases U.eq_empty_or_nonempty with rfl | ⟨x₀, hx₀⟩ + · exact ⟨fun _ => Classical.arbitrary _, by simp, by simp⟩ + obtain ⟨κ, hκ⟩ : (L x₀).Nonempty := + Finset.card_pos.mp (lt_of_le_of_lt (Nat.zero_le _) (hL x₀ hx₀)) + set S := U.filter (κ ∈ L ·) with hS + obtain ⟨K, hKS, hKind, hKabs⟩ := hK S + have hx₀S : x₀ ∈ S := by simp [hS, hx₀, hκ] + have hKU : K ⊆ U := hKS.trans (filter_subset _ _) + have hKne : K.Nonempty := by + by_contra h + rw [Finset.not_nonempty_iff_eq_empty] at h + by_cases hx : x₀ ∈ K + · simp [h] at hx + · obtain ⟨y, hy, -⟩ := hKabs x₀ hx₀S hx + simp [h] at hy + have hlt : (U \ K).card < n := by + rw [← hn] + exact Finset.card_lt_card (Finset.sdiff_ssubset hKU hKne) + obtain ⟨c', hc'L, hc'p⟩ := ih _ hlt (U \ K) rfl (fun x => (L x).erase κ) (by + intro x hx + rw [Finset.mem_sdiff] at hx + by_cases hκx : κ ∈ L x + · rw [Finset.card_erase_of_mem hκx] + obtain ⟨y, hy, hD⟩ := hKabs x (by simp [hS, hx.1, hκx]) hx.2 + have hsub : insert y ((U \ K).filter (D x ·)) ⊆ U.filter (D x ·) := by + intro z hz + rw [Finset.mem_insert] at hz + rcases hz with rfl | hz + · simp [hKU hy, hD] + · simp only [Finset.mem_filter, Finset.mem_sdiff] at hz ⊢ + exact ⟨hz.1.1, hz.2⟩ + have hyn : y ∉ (U \ K).filter (D x ·) := by simp [hy] + have := Finset.card_le_card hsub + rw [Finset.card_insert_of_notMem hyn] at this + have := hL x hx.1 + omega + · rw [Finset.erase_eq_of_notMem hκx] + refine lt_of_le_of_lt (Finset.card_le_card ?_) (hL x hx.1) + exact Finset.filter_subset_filter _ Finset.sdiff_subset) + refine ⟨fun x => if x ∈ K then κ else c' x, fun x hx => ?_, fun x hx y hy hxy => ?_⟩ + · by_cases hxK : x ∈ K + · simp only [hxK, ite_true] + have := hKS hxK + simp only [hS, Finset.mem_filter] at this + exact this.2 + · simp only [hxK, ite_false] + exact Finset.mem_of_mem_erase (hc'L x (by simp [hx, hxK])) + · by_cases hxK : x ∈ K <;> by_cases hyK : y ∈ K <;> simp only [hxK, hyK, ite_true, ite_false] + · exact (hKind x hxK y hyK hxy).elim + · intro h + have := hc'L y (by simp [hy, hyK]) + rw [← h] at this + simp at this + · intro h + have := hc'L x (by simp [hx, hxK]) + rw [h] at this + simp at this + · exact hc'p x (by simp [hx, hxK]) y (by simp [hy, hyK]) hxy + +/-- **Kernel lemma.** If every finite set of vertices has a kernel and every list is longer than +the out-degree of its vertex, there is a proper list colouring. -/ +theorem exists_listColoring {α Color : Type*} [Fintype α] + (G : SimpleGraph α) (D : α → α → Prop) [DecidableRel D] (hK : HasKernels G D) + (L : α → Finset Color) + (hL : ∀ x, (Finset.univ.filter (D x ·)).card < (L x).card) : + ∃ c : G.Coloring Color, ∀ x, c x ∈ L x := by + classical + cases isEmpty_or_nonempty α with + | inl _ => exact ⟨SimpleGraph.Coloring.mk (fun x => isEmptyElim x) fun {x} => isEmptyElim x, + fun x => isEmptyElim x⟩ + | inr hα => ?_ + have : Nonempty Color := by + obtain ⟨x⟩ := hα + obtain ⟨k, -⟩ := Finset.card_pos.mp (lt_of_le_of_lt (Nat.zero_le _) (hL x)) + exact ⟨k⟩ + obtain ⟨c, hcL, hcp⟩ := exists_listColoring_on G D hK _ Finset.univ rfl L + (fun x _ => hL x) + exact ⟨SimpleGraph.Coloring.mk c fun {x y} h => hcp x (mem_univ _) y (mem_univ _) h, + fun x => hcL x (mem_univ _)⟩ + +end Galvin diff --git a/LeanPool/ClassicalGraphColouring/Galvin/Orientation.lean b/LeanPool/ClassicalGraphColouring/Galvin/Orientation.lean new file mode 100644 index 000000000..af4db532f --- /dev/null +++ b/LeanPool/ClassicalGraphColouring/Galvin/Orientation.lean @@ -0,0 +1,241 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import LeanPool.ClassicalGraphColouring.Galvin.GaleShapley +public import LeanPool.ClassicalGraphColouring.Galvin.Kernel +public import Mathlib.Combinatorics.SimpleGraph.LineGraph + +/-! +# Galvin's orientation of the line graph of a bipartite graph + +Fix a `2`-colouring `c` of `G` (sides `0` and `1`) and a proper edge colouring `φ` with colours +in `Fin Δ`. Every edge `e` has an endpoint `endA c e` on side `0` and `endB c e` on side `1`. For +edges sharing their side-`0` endpoint, the arc goes from the larger to the smaller colour; for +edges sharing their side-`1` endpoint, from the smaller to the larger colour. Every out-degree is +less than `Δ`, and every set of edges has a kernel (a stable matching). +-/ + +@[expose] public section + +namespace Galvin + +open Finset SimpleGraph + +variable {V : Type*} {G : SimpleGraph V} + +theorem exists_ends (c : G.Coloring (Fin 2)) (e : G.edgeSet) : + ∃ a b : V, (e : Sym2 V) = s(a, b) ∧ c a = 0 := by + obtain ⟨e, he⟩ := e + induction e using Sym2.ind with + | _ x y => + have hne : c x ≠ c y := c.valid he + by_cases hx : c x = 0 + · exact ⟨x, y, rfl, hx⟩ + · refine ⟨y, x, Sym2.eq_swap, ?_⟩ + revert hne hx + generalize c x = i + generalize c y = j + revert i j + decide + +/-- The endpoint of an edge on side `0`. -/ +noncomputable def endA (c : G.Coloring (Fin 2)) (e : G.edgeSet) : V := + (exists_ends c e).choose + +/-- The endpoint of an edge on side `1`. -/ +noncomputable def endB (c : G.Coloring (Fin 2)) (e : G.edgeSet) : V := + (exists_ends c e).choose_spec.choose + +theorem edge_eq_ends (c : G.Coloring (Fin 2)) (e : G.edgeSet) : + (e : Sym2 V) = s(endA c e, endB c e) := + (exists_ends c e).choose_spec.choose_spec.1 + +theorem colour_endA (c : G.Coloring (Fin 2)) (e : G.edgeSet) : c (endA c e) = 0 := + (exists_ends c e).choose_spec.choose_spec.2 + +theorem adj_ends (c : G.Coloring (Fin 2)) (e : G.edgeSet) : G.Adj (endA c e) (endB c e) := by + have := e.2 + rw [edge_eq_ends c e] at this + exact this + +theorem colour_endB (c : G.Coloring (Fin 2)) (e : G.edgeSet) : c (endB c e) = 1 := by + have h1 := c.valid (adj_ends c e) + rw [colour_endA] at h1 + revert h1 + generalize c (endB c e) = i + revert i + decide + +theorem eq_of_ends (c : G.Coloring (Fin 2)) {e f : G.edgeSet} (hA : endA c e = endA c f) + (hB : endB c e = endB c f) : e = f := by + apply Subtype.ext + rw [edge_eq_ends c e, edge_eq_ends c f, hA, hB] + +theorem mem_edge_iff (c : G.Coloring (Fin 2)) (e : G.edgeSet) (v : V) : + v ∈ (e : Sym2 V) ↔ v = endA c e ∨ v = endB c e := by + rw [edge_eq_ends c e, Sym2.mem_iff] + +theorem lineGraph_adj_iff_ends (c : G.Coloring (Fin 2)) {e f : G.edgeSet} : + G.lineGraph.Adj e f ↔ e ≠ f ∧ (endA c e = endA c f ∨ endB c e = endB c f) := by + rw [lineGraph_adj_iff_exists] + refine and_congr_right fun _ => ⟨?_, ?_⟩ + · rintro ⟨v, hve, hvf⟩ + rw [mem_edge_iff c] at hve hvf + have hA := colour_endA c e + have hA' := colour_endA c f + have hB := colour_endB c e + have hB' := colour_endB c f + rcases hve with rfl | rfl <;> rcases hvf with h | h + · exact Or.inl h + · rw [h, hB'] at hA; exact absurd hA (by decide) + · rw [h, hA'] at hB; exact absurd hB (by decide) + · exact Or.inr h + · rintro (h | h) + · exact ⟨endA c e, (mem_edge_iff c e _).2 (Or.inl rfl), (mem_edge_iff c f _).2 (Or.inl h)⟩ + · exact ⟨endB c e, (mem_edge_iff c e _).2 (Or.inr rfl), (mem_edge_iff c f _).2 (Or.inr h)⟩ + +theorem eq_of_colour_eq (c : G.Coloring (Fin 2)) {Δ : ℕ} (φ : G.lineGraph.Coloring (Fin Δ)) + {e f : G.edgeSet} (hφ : φ e = φ f) (h : endA c e = endA c f ∨ endB c e = endB c f) : + e = f := by + by_contra hne + exact φ.valid ((lineGraph_adj_iff_ends c).2 ⟨hne, h⟩) hφ + +/-- Galvin's orientation of the line graph. -/ +def arc (c : G.Coloring (Fin 2)) {Δ : ℕ} (φ : G.lineGraph.Coloring (Fin Δ)) + (e f : G.edgeSet) : Prop := + (endA c e = endA c f ∧ φ f < φ e) ∨ (endB c e = endB c f ∧ φ e < φ f) + +/-- Every out-degree of Galvin's orientation is less than `Δ`. -/ +theorem card_arc_lt [Fintype G.edgeSet] (c : G.Coloring (Fin 2)) {Δ : ℕ} + (φ : G.lineGraph.Coloring (Fin Δ)) (e : G.edgeSet) [DecidablePred (arc c φ e)] : + (univ.filter (arc c φ e)).card < Δ := by + classical + have hsub : univ.filter (arc c φ e) ⊆ + univ.filter (fun f => endA c e = endA c f ∧ φ f < φ e) ∪ + univ.filter (fun f => endB c e = endB c f ∧ φ e < φ f) := by + intro f hf + simp only [arc, mem_filter, mem_univ, true_and, mem_union] at hf ⊢ + exact hf + have h1 : (univ.filter (fun f => endA c e = endA c f ∧ φ f < φ e)).card ≤ + (Iio (φ e)).card := by + refine card_le_card_of_injOn (fun f => φ f) (fun f hf => ?_) (fun f hf f' hf' h => ?_) + · simp only [coe_filter, mem_univ, true_and, Set.mem_ofPred_eq] at hf + simpa using hf.2 + · simp only [coe_filter, mem_univ, true_and, Set.mem_ofPred_eq] at hf hf' + exact eq_of_colour_eq c φ h (Or.inl (hf.1.symm.trans hf'.1)) + have h2 : (univ.filter (fun f => endB c e = endB c f ∧ φ e < φ f)).card ≤ + (Ioi (φ e)).card := by + refine card_le_card_of_injOn (fun f => φ f) (fun f hf => ?_) (fun f hf f' hf' h => ?_) + · simp only [coe_filter, mem_univ, true_and, Set.mem_ofPred_eq] at hf + simpa using hf.2 + · simp only [coe_filter, mem_univ, true_and, Set.mem_ofPred_eq] at hf hf' + exact eq_of_colour_eq c φ h (Or.inr (hf.1.symm.trans hf'.1)) + rw [Fin.card_Iio] at h1 + rw [Fin.card_Ioi] at h2 + have h3 := (card_le_card hsub).trans (card_union_le _ _) + have h4 := (φ e).isLt + omega + +/-- Rank of `w` for the man `m`: the colour of the edge `mw` (smaller colours preferred). -/ +noncomputable def rankA (c : G.Coloring (Fin 2)) {Δ : ℕ} (φ : G.lineGraph.Coloring (Fin Δ)) + (idx : V → ℕ) (m w : V) : ℕ := + open Classical in + if h : ∃ e : G.edgeSet, endA c e = m ∧ endB c e = w then (φ h.choose : ℕ) else Δ + idx w + +/-- Rank of `m` for the woman `w`: `Δ` minus the colour of the edge `mw` (larger colours +preferred). -/ +noncomputable def rankB (c : G.Coloring (Fin 2)) {Δ : ℕ} (φ : G.lineGraph.Coloring (Fin Δ)) + (idx : V → ℕ) (w m : V) : ℕ := + open Classical in + if h : ∃ e : G.edgeSet, endA c e = m ∧ endB c e = w then Δ - (φ h.choose : ℕ) + else Δ + 1 + idx m + +theorem choose_ends_eq (c : G.Coloring (Fin 2)) (e : G.edgeSet) + (h : ∃ f : G.edgeSet, endA c f = endA c e ∧ endB c f = endB c e) : h.choose = e := + eq_of_ends c h.choose_spec.1 h.choose_spec.2 + +theorem rankA_ends (c : G.Coloring (Fin 2)) {Δ : ℕ} (φ : G.lineGraph.Coloring (Fin Δ)) + (idx : V → ℕ) (e : G.edgeSet) : rankA c φ idx (endA c e) (endB c e) = φ e := by + have h : ∃ f : G.edgeSet, endA c f = endA c e ∧ endB c f = endB c e := ⟨e, rfl, rfl⟩ + rw [rankA] + split_ifs + rw [choose_ends_eq c e h] + +theorem rankB_ends (c : G.Coloring (Fin 2)) {Δ : ℕ} (φ : G.lineGraph.Coloring (Fin Δ)) + (idx : V → ℕ) (e : G.edgeSet) : rankB c φ idx (endB c e) (endA c e) = Δ - φ e := by + have h : ∃ f : G.edgeSet, endA c f = endA c e ∧ endB c f = endB c e := ⟨e, rfl, rfl⟩ + rw [rankB] + split_ifs + rw [choose_ends_eq c e h] + +theorem rankA_injective (c : G.Coloring (Fin 2)) {Δ : ℕ} (φ : G.lineGraph.Coloring (Fin Δ)) + {idx : V → ℕ} (hidx : Function.Injective idx) (m : V) : + Function.Injective (rankA c φ idx m) := by + intro w w' hww + unfold rankA at hww + split_ifs at hww with h h' + · have := eq_of_colour_eq c φ (Fin.ext hww) + (Or.inl (h.choose_spec.1.trans h'.choose_spec.1.symm)) + rw [← h.choose_spec.2, ← h'.choose_spec.2, this] + · have := (φ h.choose).isLt; omega + · rename_i h₂; have := (φ h₂.choose).isLt; omega + · exact hidx (by omega) + +theorem rankB_injective (c : G.Coloring (Fin 2)) {Δ : ℕ} (φ : G.lineGraph.Coloring (Fin Δ)) + {idx : V → ℕ} (hidx : Function.Injective idx) (w : V) : + Function.Injective (rankB c φ idx w) := by + intro m m' hmm + unfold rankB at hmm + split_ifs at hmm with h h' + · have h1 := (φ h.choose).isLt + have h2 := (φ h'.choose).isLt + have := eq_of_colour_eq c φ (Fin.ext (by omega)) + (Or.inr (h.choose_spec.2.trans h'.choose_spec.2.symm)) + rw [← h.choose_spec.1, ← h'.choose_spec.1, this] + · omega + · omega + · exact hidx (by omega) + +/-- Every set of edges has a kernel for Galvin's orientation: a stable matching. -/ +theorem hasKernels_arc [Finite V] (c : G.Coloring (Fin 2)) {Δ : ℕ} + (φ : G.lineGraph.Coloring (Fin Δ)) : HasKernels G.lineGraph (arc c φ) := by + classical + intro S + obtain ⟨N, ⟨eqv⟩⟩ := Finite.exists_equiv_fin V + let idx : V → ℕ := fun v => (eqv v : ℕ) + have hidx : Function.Injective idx := fun a b h => eqv.injective (Fin.ext h) + let E : V → V → Prop := fun m w => ∃ e ∈ S, endA c e = m ∧ endB c e = w + obtain ⟨μ, hsub, hm, hw, hst⟩ := exists_isStable (rankA c φ idx) (rankB c φ idx) + (rankA_injective c φ hidx) (rankB_injective c φ hidx) _ E rfl + refine ⟨S.filter (fun e => μ (endA c e) (endB c e)), filter_subset _ _, ?_, ?_⟩ + · intro x hx y hy hxy + simp only [mem_filter] at hx hy + obtain ⟨hne, h | h⟩ := (lineGraph_adj_iff_ends c).1 hxy + · rw [h] at hx + exact hne (eq_of_ends c h (hm _ _ _ hx.2 hy.2)) + · rw [h] at hx + exact hne (eq_of_ends c (hw _ _ _ hx.2 hy.2) h) + · intro x hxS hxK + simp only [mem_filter, hxS, true_and] at hxK + rcases hst _ _ ⟨x, hxS, rfl, rfl⟩ hxK with ⟨w', hμ, hlt⟩ | ⟨m', hμ, hlt⟩ + · obtain ⟨f, hfS, hfA, hfB⟩ := hsub _ _ hμ + subst hfB + rw [← hfA] at hμ hlt + refine ⟨f, mem_filter.2 ⟨hfS, hμ⟩, Or.inl ⟨hfA.symm, ?_⟩⟩ + rw [rankA_ends, hfA, rankA_ends] at hlt + exact hlt + · obtain ⟨f, hfS, hfA, hfB⟩ := hsub _ _ hμ + subst hfA + rw [← hfB] at hμ hlt + refine ⟨f, mem_filter.2 ⟨hfS, hμ⟩, Or.inr ⟨hfB.symm, ?_⟩⟩ + rw [rankB_ends, hfB, rankB_ends] at hlt + have := (φ f).isLt + have := (φ x).isLt + change (φ x : ℕ) < φ f + omega + +end Galvin diff --git a/LeanPool/ClassicalGraphColouring/Imports.lean b/LeanPool/ClassicalGraphColouring/Imports.lean new file mode 100644 index 000000000..320025beb --- /dev/null +++ b/LeanPool/ClassicalGraphColouring/Imports.lean @@ -0,0 +1,16 @@ +/- +Copyright (c) 2026 Lean Pool contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lean Pool contributors +-/ +module -- shake: keep-all --deprecated_module: ignore + +-- Generated project imports; run `lake exe mk_all`. +public import LeanPool.ClassicalGraphColouring +public import LeanPool.ClassicalGraphColouring.Galvin.GaleShapley +public import LeanPool.ClassicalGraphColouring.Galvin.Galvin +public import LeanPool.ClassicalGraphColouring.Galvin.Kernel +public import LeanPool.ClassicalGraphColouring.Galvin.Orientation +public import LeanPool.ClassicalGraphColouring.Konig.Basic +public import LeanPool.ClassicalGraphColouring.Orientations.GallaiRoy +public import LeanPool.ClassicalGraphColouring.Spectrum.Bounds diff --git a/LeanPool/ClassicalGraphColouring/Konig/Basic.lean b/LeanPool/ClassicalGraphColouring/Konig/Basic.lean new file mode 100644 index 000000000..9ee330dad --- /dev/null +++ b/LeanPool/ClassicalGraphColouring/Konig/Basic.lean @@ -0,0 +1,248 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import LeanPool.Vizing.Main + +/-! +# Kőnig's edge-colouring theorem + +`lineGraph_colorable_of_colorable_two`: a finite bipartite graph has a proper edge colouring with +`Δ(G)` colours. The proof colours the edges one at a time with the partial proper edge colourings +`LeanPool.Vizing.PEC` of the Vizing development. To colour an uncoloured edge `xy`, take a colour +`a` free at `x` and a colour `b` free at `y` (both exist since `xy` is uncoloured and there are +`Δ(G)` colours). If neither colours `xy` directly, swap `a` and `b` on the `a/b` Kempe component +of `y`. Since `b` is free at `y`, the colours along any Kempe path ending at `y` alternate, the +edge farthest from `y` having colour `a` exactly when the path has odd length; and a Kempe path +from `y` to `x` has odd length because `G` is bipartite. So `x` is not in the component, `a` is +still free at `x`, and `a` becomes free at `y`. +-/ + +@[expose] public section + +open SimpleGraph Finset + +namespace Konig + +open LeanPool.Vizing LeanPool.Vizing.PEC + +variable {V : Type*} {C : Type*} {G : SimpleGraph V} + +/-- At an endpoint of an uncoloured edge some colour is free, provided there are at least `Δ(G)` +colours. -/ +theorem exists_free_of_none [Fintype V] [Fintype C] [DecidableRel G.Adj] (c : PEC G C) + (hcard : G.maxDegree ≤ Fintype.card C) {x y : V} (hadj : G.Adj x y) + (hnone : c.col x y = none) : ∃ γ, c.IsFree x γ := by + classical + by_contra hcon + push Not at hcon + simp only [IsFree, not_forall, not_not] at hcon + choose g hg using hcon + have hginj : Set.InjOn g (univ : Finset C) := by + intro γ₁ _ γ₂ _ h + have : (some γ₁ : Option C) = some γ₂ := by rw [← hg γ₁, ← hg γ₂, h] + exact Option.some_injective _ this + have hmem : ∀ γ ∈ (univ : Finset C), g γ ∈ (G.neighborFinset x).erase y := by + intro γ _ + refine Finset.mem_erase.2 ⟨fun h => ?_, (mem_neighborFinset _ _ _).2 (c.col_adj (hg γ))⟩ + have := hg γ + rw [h, hnone] at this + simp at this + have hcards := Finset.card_le_card_of_injOn g hmem hginj + rw [card_univ, Finset.card_erase_of_mem ((mem_neighborFinset _ _ _).2 hadj), + card_neighborFinset_eq_degree] at hcards + have hdeg := G.degree_le_maxDegree x + have hpos : 0 < G.degree x := G.degree_pos_iff_exists_adj x |>.2 ⟨y, hadj⟩ + omega + +/-- Along a walk of a graph contained in `G`, a proper 2-colouring of `G` changes at every step. -/ +theorem colour_walk {H : SimpleGraph V} (hHG : H ≤ G) (s : G.Coloring (Fin 2)) {u v : V} + (p : H.Walk u v) : (s v : ℕ) % 2 = ((s u : ℕ) + p.length) % 2 := by + induction p with + | nil => simp + | @cons u w v h p ih => + rw [Walk.length_cons, ih] + have hne : (s u : ℕ) ≠ (s w : ℕ) := fun he => s.valid (hHG h) (Fin.ext he) + have hu := (s u).isLt + have hw := (s w).isLt + omega + +/-- **Alternation along a Kempe path.** If `b` is free at `y`, then on every path of the `a/b` +Kempe graph ending at `y`, the first edge has colour `a` if the length is odd and `b` if it is +even (and positive). -/ +theorem col_snd_of_kempe_path (c : PEC G C) {a b : C} {y : V} + (hy : c.IsFree y b) {u : V} (p : (c.kempeGraph a b).Walk u y) (hp : p.IsPath) + (hlen : 0 < p.length) : + c.col u p.snd = some (if p.length % 2 = 1 then a else b) := by + induction p with + | nil => simp at hlen + | @cons u w y h r ih => + have hcol := h.2 + rw [Walk.snd_cons] + rw [Walk.cons_isPath_iff] at hp + rcases Nat.eq_zero_or_pos r.length with h0 | hpos + · -- `r` is trivial: `w = y` + have hwy : w = y := Walk.eq_of_length_eq_zero h0 + subst hwy + rw [Walk.length_cons, h0, zero_add] + rcases hcol with hcol | hcol + · simpa using hcol + · exact absurd ((c.col_symm w u).trans hcol) (hy u) + · have hih := ih hy hp.1 hpos + have hne : u ≠ r.snd := by + intro he + exact hp.2 (by rw [he]; exact r.getVert_mem_support 1) + rw [Walk.length_cons] + -- the colours of `w u` and `w r.snd` differ + have hdiff : c.col w u ≠ c.col w r.snd := by + intro he + rw [hih] at he + exact hne (c.col_proper he hih) + rw [c.col_symm w u] at hdiff + rcases Nat.mod_two_eq_zero_or_one r.length with hr | hr + · have h1 : (r.length + 1) % 2 = 1 := by omega + rw [hr] at hih + simp only [zero_ne_one, ite_false] at hih + rw [hih] at hdiff + simp only [h1, ite_true] + rcases hcol with hcol | hcol + · exact hcol + · exact absurd hcol hdiff + · have h1 : (r.length + 1) % 2 = 0 := by omega + rw [hr] at hih + simp only [ite_true] at hih + rw [hih] at hdiff + simp only [h1, zero_ne_one, ite_false] + rcases hcol with hcol | hcol + · exact absurd hcol hdiff + · exact hcol + +/-- The Kempe graph is a subgraph of `G`. -/ +theorem kempeGraph_le (c : PEC G C) (a b : C) : c.kempeGraph a b ≤ G := by + intro u v h + rcases h.2 with h | h <;> exact c.col_adj h + +/-- **Kőnig's extension step.** In a bipartite graph with at least `Δ(G)` colours, any uncoloured +edge can be coloured after recolouring. -/ +theorem konig_step [Fintype V] [Fintype C] [DecidableRel G.Adj] + (s : G.Coloring (Fin 2)) (c : PEC G C) + (hcard : G.maxDegree ≤ Fintype.card C) {x y : V} (hadj : G.Adj x y) + (hnone : c.col x y = none) : + ∃ c' : PEC G C, Extends c c' ∧ c'.col x y ≠ none := by + classical + obtain ⟨a, ha⟩ := exists_free_of_none c hcard hadj hnone + obtain ⟨b, hb⟩ := exists_free_of_none c hcard hadj.symm (by rw [c.col_symm]; exact hnone) + by_cases hay : c.IsFree y a + · exact ⟨c.setEdge a hadj ha hay, extends_setEdge c a hadj ha hay, by + simp [setEdge]⟩ + have hab : a ≠ b := fun h => hay (h ▸ hb) + -- `x` is not in the `a/b` Kempe component of `y` + have hxy : ¬ (c.kempeGraph a b).Reachable y x := by + rintro ⟨q⟩ + set p := q.toPath.1.reverse with hpdef + have hp : p.IsPath := q.toPath.2.reverse + have hpar := colour_walk (kempeGraph_le c a b) s p + have hsx : s x ≠ s y := s.valid hadj + have hodd : p.length % 2 = 1 := by + have hx := (s x).isLt + have hy' := (s y).isLt + have : (s x : ℕ) ≠ (s y : ℕ) := fun h => hsx (Fin.ext h) + omega + have hlen : 0 < p.length := by omega + have := col_snd_of_kempe_path c hb p hp hlen + simp only [hodd, ↓reduceIte] at this + exact ha _ this + set c1 := c.kempeSwap a b y + have ha1 : c1.IsFree x a := (isFree_kempeSwap_of_not_reachable c a b hxy a).2 ha + have hay1 : c1.IsFree y a := by + rw [isFree_kempeSwap_of_reachable c a b (Reachable.refl y) a, Equiv.swap_apply_left] + exact hb + refine ⟨c1.setEdge a hadj ha1 hay1, (extends_kempeSwap c a b y).trans + (extends_setEdge c1 a hadj ha1 hay1), by simp [setEdge]⟩ + +/-- **Kőnig's theorem.** A finite bipartite graph has a total proper partial edge colouring with +any colour type of size at least `Δ(G)`. -/ +theorem exists_total_of_bipartite [Fintype V] [Fintype C] [DecidableRel G.Adj] + (s : G.Coloring (Fin 2)) + (hcard : G.maxDegree ≤ Fintype.card C) : + ∃ c : PEC G C, ∀ u v, G.Adj u v → c.col u v ≠ none := by + classical + suffices H : ∀ (k : ℕ) (c : PEC G C), c.uncoloured.card ≤ k → + ∃ c' : PEC G C, ∀ u v, G.Adj u v → c'.col u v ≠ none by + exact H (empty G C).uncoloured.card (empty G C) le_rfl + intro k + induction k with + | zero => + intro c hk + refine ⟨c, fun u v huv hcol => ?_⟩ + have hmem : (u, v) ∈ c.uncoloured := (c.mem_uncoloured (u, v)).2 ⟨huv, hcol⟩ + have := Finset.card_pos.2 ⟨_, hmem⟩ + omega + | succ k ih => + intro c hk + by_cases hall : ∀ u v, G.Adj u v → c.col u v ≠ none + · exact ⟨c, hall⟩ + · push Not at hall + obtain ⟨x, y, hadj, hnone⟩ := hall + obtain ⟨c1, hext, hc1⟩ := konig_step s c hcard hadj hnone + refine ih c1 ?_ + have hsub : c1.uncoloured ⊆ c.uncoloured := by + intro p hp + rw [mem_uncoloured] at hp ⊢ + refine ⟨hp.1, ?_⟩ + by_contra hcon + exact (hext p.1 p.2 hcon) hp.2 + have hxy : (x, y) ∈ c.uncoloured := (c.mem_uncoloured (x, y)).2 ⟨hadj, hnone⟩ + have hxy' : (x, y) ∉ c1.uncoloured := by + rw [mem_uncoloured] + rintro ⟨-, h⟩ + exact hc1 h + have hlt : c1.uncoloured.card < c.uncoloured.card := + Finset.card_lt_card ⟨hsub, fun hcon => hxy' (hcon hxy)⟩ + omega + +/-- **Kőnig's edge-colouring theorem.** The line graph of a finite bipartite graph is +`Δ(G)`-colourable. -/ +theorem lineGraph_colorable_of_colorable_two [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] + (h : G.Colorable 2) : G.lineGraph.Colorable G.maxDegree := by + classical + obtain ⟨s⟩ := h + obtain ⟨c, hc⟩ := exists_total_of_bipartite (C := Fin G.maxDegree) s (by simp) + exact ⟨c.lineGraphColoring hc⟩ + +/-- The edges at a vertex of maximum degree are pairwise adjacent in the line graph, so +`Δ(G) ≤ χ'(G)`. -/ +theorem maxDegree_le_lineGraph_chromaticNumber [Fintype V] (G : SimpleGraph V) + [DecidableRel G.Adj] : (G.maxDegree : ℕ∞) ≤ G.lineGraph.chromaticNumber := by + classical + rcases isEmpty_or_nonempty V with hV | hV + · have : G.maxDegree = 0 := by + rw [← Nat.le_zero] + exact G.maxDegree_le_of_forall_degree_le 0 (fun v => isEmptyElim v) + rw [this, Nat.cast_zero] + exact zero_le + · obtain ⟨v, hv⟩ := G.exists_maximal_degree_vertex + rw [hv] + refine le_chromaticNumber_of_pairwise_adj (ι := G.neighborSet v) ?_ + (fun u => (⟨s(v, u), u.2⟩ : G.edgeSet)) ?_ + · rw [Nat.card_eq_fintype_card, card_neighborSet_eq_degree] + · intro u u' huu + rw [lineGraph_adj_iff_exists] + refine ⟨fun h => huu (Subtype.ext ?_), v, Sym2.mem_mk_left _ _, Sym2.mem_mk_left _ _⟩ + have : (u : V) = u' ∨ v = u' ∧ (u : V) = v := by simpa using congrArg Subtype.val h + rcases this with h' | ⟨-, h'⟩ + · exact h' + · exact absurd h' (G.ne_of_adj u.2).symm + +/-- **Kőnig's edge-colouring theorem**, chromatic-number form: `χ'(G) = Δ(G)` for a finite +bipartite graph. -/ +theorem lineGraph_chromaticNumber_of_colorable_two [Fintype V] (G : SimpleGraph V) + [DecidableRel G.Adj] (h : G.Colorable 2) : + G.lineGraph.chromaticNumber = G.maxDegree := + le_antisymm (lineGraph_colorable_of_colorable_two G h).chromaticNumber_le + (maxDegree_le_lineGraph_chromaticNumber G) + +end Konig diff --git a/LeanPool/ClassicalGraphColouring/Orientations/GallaiRoy.lean b/LeanPool/ClassicalGraphColouring/Orientations/GallaiRoy.lean new file mode 100644 index 000000000..48f5b9a1a --- /dev/null +++ b/LeanPool/ClassicalGraphColouring/Orientations/GallaiRoy.lean @@ -0,0 +1,170 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex +public import Mathlib.Tactic + +/-! +# The Gallai–Hasse–Roy–Vitaver theorem + +An orientation of a simple graph `G` is a relation `o` such that every edge `uv` of `G` is +oriented in at least one direction (`o u v ∨ o v u`) and every arc is an edge of `G`. A directed +path with `m` vertices is an injective map `f : Fin m → V` with an arc from `f i` to `f (i + 1)` +for all consecutive indices. + +* `GallaiRoy.colorable_of_orientation`: **Gallai (1968), Hasse (1965), Roy (1967), + Vitaver (1962).** If some orientation of `G` has no directed path with more than `k` vertices, + then `G` is `k`-colourable. +* `GallaiRoy.exists_orientation_of_colorable`: conversely, a `k`-colourable graph has an + (acyclic) orientation without directed paths on more than `k` vertices. Together: the + chromatic number is the minimum, over orientations, of the number of vertices of a longest + directed path. +-/ + +@[expose] public section + +open SimpleGraph + +namespace GallaiRoy + +variable {V : Type*} + +/-- `o` is an orientation of `G`: every edge is oriented in at least one direction and every arc +is an edge. -/ +def IsOrientation (G : SimpleGraph V) (o : V → V → Prop) : Prop := + (∀ u v, G.Adj u v → o u v ∨ o v u) ∧ ∀ u v, o u v → G.Adj u v + +/-- `f` is a directed path of `o` with `m` vertices. -/ +def IsDirectedPath (o : V → V → Prop) {m : ℕ} (f : Fin m → V) : Prop := + Function.Injective f ∧ ∀ (i : ℕ) (h : i + 1 < m), o (f ⟨i, by omega⟩) (f ⟨i + 1, h⟩) + +private lemma transGen_of_mem_isChain {D : V → V → Prop} : + ∀ {a : V} {l : List V}, List.IsChain D (a :: l) → ∀ w ∈ l, Relation.TransGen D a w + | a, [], _, w, hw => by simp at hw + | a, b :: l, h, w, hw => by + rw [List.isChain_cons_cons] at h + rcases List.mem_cons.1 hw with rfl | hw + · exact .single h.1 + · exact .head h.1 (transGen_of_mem_isChain h.2 w hw) + +private lemma nodup_of_isChain {D : V → V → Prop} (hD : ∀ x, ¬ Relation.TransGen D x x) : + ∀ {l : List V}, List.IsChain D l → l.Nodup + | [], _ => List.nodup_nil + | a :: l, h => by + refine List.nodup_cons.2 ⟨fun ha => hD a (transGen_of_mem_isChain h a ha), ?_⟩ + exact nodup_of_isChain hD h.tail + +private lemma isDirectedPath_of_isChain {D o : V → V → Prop} (hDo : ∀ a b, D a b → o a b) + (hD : ∀ x, ¬ Relation.TransGen D x x) {l : List V} (h : List.IsChain D l) : + IsDirectedPath o l.get := by + refine ⟨List.nodup_iff_injective_get.1 (nodup_of_isChain hD h), fun i hi => ?_⟩ + exact hDo _ _ (List.isChain_iff_getElem.1 h i hi) + +private lemma exists_longer_of_transGen {D : V → V → Prop} {a b : V} (hab : Relation.TransGen D a b) + {l : List V} (hl : List.IsChain D (b :: l)) : + ∃ l', List.IsChain D (a :: l') ∧ l.length < l'.length := by + induction hab using Relation.TransGen.head_induction_on generalizing l with + | single h => exact ⟨b :: l, List.isChain_cons_cons.2 ⟨h, hl⟩, by simp⟩ + | head h _ ih => + obtain ⟨l', hl', hlen⟩ := ih hl + exact ⟨_ :: l', List.isChain_cons_cons.2 ⟨h, hl'⟩, by simp; omega⟩ + +private lemma transGen_sup_edge {D : V → V → Prop} {u v a b : V} + (h : Relation.TransGen (fun x y => D x y ∨ (x = u ∧ y = v)) a b) : + Relation.TransGen D a b ∨ (Relation.ReflTransGen D a u ∧ Relation.ReflTransGen D v b) := by + induction h with + | single h => + rcases h with h | ⟨rfl, rfl⟩ + · exact .inl (.single h) + · exact .inr ⟨.refl, .refl⟩ + | tail _ h ih => + rcases h with h | ⟨rfl, rfl⟩ + · rcases ih with ih | ⟨h1, h2⟩ + · exact .inl (ih.tail h) + · exact .inr ⟨h1, h2.tail h⟩ + · rcases ih with ih | ⟨h1, _⟩ + · exact .inr ⟨ih.to_reflTransGen, .refl⟩ + · exact .inr ⟨h1, .refl⟩ + +/-- **Gallai–Hasse–Roy–Vitaver.** If an orientation of a finite graph has no directed path on more +than `k` vertices, the graph is `k`-colourable. -/ +theorem colorable_of_orientation [Finite V] (G : SimpleGraph V) (o : V → V → Prop) + (ho : IsOrientation G o) (k : ℕ) + (hk : ∀ (m : ℕ) (f : Fin m → V), IsDirectedPath o f → m ≤ k) : G.Colorable k := by + classical + -- a maximal acyclic sub-relation of `o` + obtain ⟨D, ⟨hDo, hDac⟩, hmax⟩ := (Set.toFinite + {D : V → V → Prop | (∀ a b, D a b → o a b) ∧ ∀ x, ¬ Relation.TransGen D x x}).exists_maximal + ⟨fun _ _ => False, fun _ _ h => h.elim, fun x h => by + cases h with | single h => exact h | tail _ h => exact h⟩ + have hbound : ∀ {v : V} {l : List V}, List.IsChain D (v :: l) → l.length + 1 ≤ k := by + intro v l hl + simpa using hk _ _ (isDirectedPath_of_isChain hDo hDac hl) + let P : V → ℕ → Prop := fun v m => ∃ l : List V, List.IsChain D (v :: l) ∧ l.length = m + let h : V → ℕ := fun v => Nat.findGreatest (P v) k + have hP0 : ∀ v, P v 0 := fun v => ⟨[], by simp, rfl⟩ + have hspec : ∀ v, P v (h v) := fun v => Nat.findGreatest_spec (Nat.zero_le _) (hP0 v) + have hlt : ∀ v, h v < k := by + intro v + obtain ⟨l, hl, hlen⟩ := hspec v + have := hbound hl + omega + have hmono : ∀ {a b : V}, Relation.TransGen D a b → h b < h a := by + intro a b hab + obtain ⟨l, hl, hlen⟩ := hspec b + obtain ⟨l', hl', hlen'⟩ := exists_longer_of_transGen hab hl + have : l'.length ≤ h a := + Nat.le_findGreatest (by have := hbound hl'; omega) ⟨l', hl', rfl⟩ + omega + have key : ∀ {u v : V}, o u v → u ≠ v → h u ≠ h v := by + intro u v huv hne + by_cases hD : D u v + · exact (hmono (.single hD)).ne' + · have hvu : Relation.ReflTransGen D v u := by + by_contra hvu + have hmem : (fun x y => D x y ∨ (x = u ∧ y = v)) ∈ + {D : V → V → Prop | (∀ a b, D a b → o a b) ∧ ∀ x, ¬ Relation.TransGen D x x} := by + refine ⟨fun a b hab => ?_, fun x hx => ?_⟩ + · rcases hab with hab | ⟨rfl, rfl⟩ + · exact hDo a b hab + · exact huv + · rcases transGen_sup_edge hx with hx | ⟨h1, h2⟩ + · exact hDac x hx + · exact hvu (h2.trans h1) + have := hmax hmem (fun a b hab => Or.inl hab) + exact hD (this u v (Or.inr ⟨rfl, rfl⟩)) + rcases Relation.reflTransGen_iff_eq_or_transGen.1 hvu with h1 | h1 + · exact absurd h1 hne + · exact (hmono h1).ne + refine ⟨Coloring.mk (fun v => ⟨h v, hlt v⟩) fun {u v} huv => ?_⟩ + intro heq + have heq' : h u = h v := congrArg Fin.val heq + rcases ho.1 u v huv with h1 | h1 + · exact key h1 huv.ne heq' + · exact key h1 huv.ne.symm heq'.symm + +/-- Conversely, a `k`-colourable graph has an orientation without directed paths on more than `k` +vertices (orient every edge towards the larger colour). -/ +theorem exists_orientation_of_colorable (G : SimpleGraph V) (k : ℕ) (h : G.Colorable k) : + ∃ o : V → V → Prop, IsOrientation G o ∧ + ∀ (m : ℕ) (f : Fin m → V), IsDirectedPath o f → m ≤ k := by + obtain ⟨c⟩ := h + refine ⟨fun u v => G.Adj u v ∧ c u < c v, ⟨fun u v huv => ?_, fun u v h => h.1⟩, ?_⟩ + · rcases lt_or_gt_of_ne (c.valid huv) with h | h + · exact .inl ⟨huv, h⟩ + · exact .inr ⟨huv.symm, h⟩ + · intro m f hf + cases m with + | zero => exact Nat.zero_le _ + | succ n => + have hmono : StrictMono (fun i : Fin (n + 1) => c (f i)) := by + refine Fin.strictMono_iff_lt_succ.2 fun i => ?_ + have := hf.2 i.1 (by omega) + exact this.2 + simpa using Fintype.card_le_of_injective _ hmono.injective + +end GallaiRoy diff --git a/LeanPool/ClassicalGraphColouring/Spectrum/Bounds.lean b/LeanPool/ClassicalGraphColouring/Spectrum/Bounds.lean new file mode 100644 index 000000000..cf814a671 --- /dev/null +++ b/LeanPool/ClassicalGraphColouring/Spectrum/Bounds.lean @@ -0,0 +1,324 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex +public import Mathlib.Combinatorics.SimpleGraph.AdjMatrix +public import Mathlib.Combinatorics.SimpleGraph.DegreeSum +public import Mathlib.Analysis.Matrix.Spectrum +public import Mathlib.Tactic + +/-! +# Spectral bounds on the chromatic number and the independence number + +Let `G` be a finite simple graph on a nonempty vertex type, `A` its real adjacency matrix +(Mathlib's `SimpleGraph.adjMatrix`), which is Hermitian, and `λ_max`, `λ_min` its largest and +smallest eigenvalues (`Matrix.IsHermitian.eigenvalues`). + +* `SpectralBounds.average_degree_le` and `SpectralBounds.le_maxDegree`: the average degree + `2|E|/n` is at most `λ_max`, and `λ_max` is at most the maximum degree. +* `SpectralBounds.wilf`: **Wilf (1967).** `G` is `(⌊λ_max⌋ + 1)`-colourable. +* `SpectralBounds.hoffman_chromatic`: **Hoffman (1970).** If `G` has an edge, every proper + colouring uses at least `1 - λ_max / λ_min` colours. +* `SpectralBounds.hoffman_ratio`: **Hoffman's ratio bound.** If `G` is `k`-regular with `k ≥ 1`, + every independent set has at most `n (−λ_min) / (k − λ_min)` vertices. +-/ + +@[expose] public section + +open Finset SimpleGraph + +namespace SpectralBounds + +variable {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) + [DecidableRel G.Adj] (hA : (G.adjMatrix ℝ).IsHermitian) + +section Spectral + +variable {W : Type*} [Fintype W] [DecidableEq W] {M : Matrix W W ℝ} + +open Matrix + +/-- Expansion of the quadratic form of a real symmetric matrix in an orthonormal eigenbasis. -/ +theorem exists_quadForm_eq (hM : M.IsHermitian) (x : W → ℝ) : + ∃ y : W → ℝ, x ⬝ᵥ (M *ᵥ x) = ∑ i, hM.eigenvalues i * y i ^ 2 ∧ + x ⬝ᵥ x = ∑ i, y i ^ 2 := by + set U : Matrix W W ℝ := (hM.eigenvectorUnitary : Matrix W W ℝ) with hU + have hUU : U * star U = 1 := Unitary.coe_mul_star_self _ + have hs : star U = Uᵀ := by + rw [star_eq_conjTranspose, conjTranspose_eq_transpose_of_trivial] + refine ⟨Uᵀ *ᵥ x, ?_, ?_⟩ + · conv_lhs => rw [hM.spectral_theorem] + simp only [Unitary.conjStarAlgAut_apply] + rw [← hU, hs, ← mulVec_mulVec, ← mulVec_mulVec, dotProduct_mulVec, ← mulVec_transpose] + simp [dotProduct, mulVec_diagonal, sq, mul_left_comm] + · have : ∑ i, (Uᵀ *ᵥ x) i ^ 2 = (Uᵀ *ᵥ x) ⬝ᵥ (Uᵀ *ᵥ x) := by simp [dotProduct, sq] + rw [this, dotProduct_mulVec, vecMul_transpose, mulVec_mulVec, ← hs, hUU, one_mulVec, + dotProduct_comm] + +/-- Rayleigh upper bound: `xᵀ M x ≤ λ_max ‖x‖²`. -/ +theorem quadForm_le_iSup (hM : M.IsHermitian) (x : W → ℝ) : + x ⬝ᵥ (M *ᵥ x) ≤ (⨆ i, hM.eigenvalues i) * (x ⬝ᵥ x) := by + obtain ⟨y, h1, h2⟩ := exists_quadForm_eq hM x + rw [h1, h2, mul_sum] + gcongr with i + exact le_ciSup (Set.finite_range _).bddAbove i + +/-- Rayleigh lower bound: `λ_min ‖x‖² ≤ xᵀ M x`. -/ +theorem iInf_le_quadForm (hM : M.IsHermitian) (x : W → ℝ) : + (⨅ i, hM.eigenvalues i) * (x ⬝ᵥ x) ≤ x ⬝ᵥ (M *ᵥ x) := by + obtain ⟨y, h1, h2⟩ := exists_quadForm_eq hM x + rw [h1, h2, mul_sum] + gcongr with i + exact ciInf_le (Set.finite_range _).bddBelow i + +/-- There is a unit eigenvector for the largest eigenvalue. -/ +theorem exists_unit_eigenvector_iSup [Nonempty W] (hM : M.IsHermitian) : + ∃ x : W → ℝ, M *ᵥ x = (⨆ i, hM.eigenvalues i) • x ∧ x ⬝ᵥ x = 1 := by + obtain ⟨i, hi⟩ := exists_eq_ciSup_of_finite (f := hM.eigenvalues) + refine ⟨⇑(hM.eigenvectorBasis i), ?_, ?_⟩ + · rw [hM.mulVec_eigenvectorBasis, hi] + · have h1 := hM.eigenvectorBasis.orthonormal.1 i + have h2 := real_inner_self_eq_norm_sq (hM.eigenvectorBasis i) + rw [h1, one_pow, EuclideanSpace.inner_eq_star_dotProduct] at h2 + simpa [dotProduct_comm] using h2 + +end Spectral + +open Matrix + +omit [DecidableEq V] [Nonempty V] in +/-- The quadratic form of the adjacency matrix vanishes on vectors supported on an +independent set. -/ +theorem quadForm_eq_zero_of_indep (z : V → ℝ) (hz : ∀ u v, G.Adj u v → z u = 0 ∨ z v = 0) : + z ⬝ᵥ (G.adjMatrix ℝ *ᵥ z) = 0 := by + simp only [dotProduct, mulVec, mul_sum] + refine sum_eq_zero fun v _ => sum_eq_zero fun u _ => ?_ + classical + rw [adjMatrix_apply] + split_ifs with h + · rcases hz v u h with h | h <;> simp [h] + · simp + +omit [DecidableEq V] [Nonempty V] in +theorem dotProduct_adjMatrix_mulVec_comm (x z : V → ℝ) : + x ⬝ᵥ (G.adjMatrix ℝ *ᵥ z) = z ⬝ᵥ (G.adjMatrix ℝ *ᵥ x) := by + rw [dotProduct_mulVec, ← mulVec_transpose, transpose_adjMatrix, dotProduct_comm] + +omit [Nonempty V] in +/-- The key inequality behind both Hoffman bounds: apply the Rayleigh lower bound to +`z - t • x`, where `x` is an eigenvector and `z` has vanishing quadratic form. -/ +theorem hoffman_key (x z : V → ℝ) (θ t : ℝ) (hx : G.adjMatrix ℝ *ᵥ x = θ • x) + (hz : z ⬝ᵥ (G.adjMatrix ℝ *ᵥ z) = 0) : + (⨅ i, hA.eigenvalues i) * (z ⬝ᵥ z - 2 * t * (z ⬝ᵥ x) + t ^ 2 * (x ⬝ᵥ x)) ≤ + -2 * t * θ * (z ⬝ᵥ x) + t ^ 2 * θ * (x ⬝ᵥ x) := by + have h := iInf_le_quadForm hA (z - t • x) + have hxz : x ⬝ᵥ (G.adjMatrix ℝ *ᵥ z) = θ * (z ⬝ᵥ x) := by + rw [dotProduct_adjMatrix_mulVec_comm, hx, dotProduct_smul, smul_eq_mul] + have hzx : z ⬝ᵥ x = x ⬝ᵥ z := dotProduct_comm _ _ + simp only [mulVec_sub, mulVec_smul, hx, sub_dotProduct, dotProduct_sub, smul_dotProduct, + dotProduct_smul, smul_eq_mul, hz] at h + rw [hxz] at h + rw [← hzx] at h + nlinarith [h] + +theorem iInf_eigenvalues_nonpos : (⨅ i, hA.eigenvalues i) ≤ 0 := by + obtain ⟨v⟩ := ‹Nonempty V› + have h := iInf_le_quadForm hA (Pi.single v 1) + simpa using h + +omit [Nonempty V] in +theorem iInf_eigenvalues_le_neg_one (hE : G.edgeSet.Nonempty) : + (⨅ i, hA.eigenvalues i) ≤ -1 := by + obtain ⟨e, he⟩ := hE + induction e using Sym2.ind with + | _ u v => + rw [mem_edgeSet] at he + have huv : u ≠ v := he.ne + have h := iInf_le_quadForm hA (Pi.single u 1 - Pi.single v 1) + simp [mulVec_sub, dotProduct_sub, sub_dotProduct, huv, huv.symm, he, he.symm] at h + linarith + +omit [Nonempty V] in +theorem exists_low_degree (S : Finset V) (hS : S.Nonempty) : + ∃ v ∈ S, (#(G.neighborFinset v ∩ S) : ℝ) ≤ ⨆ i, hA.eigenvalues i := by + set x : V → ℝ := fun w => if w ∈ S then 1 else 0 + have h := quadForm_le_iSup hA x + have hxx : x ⬝ᵥ x = #S := by simp [x, dotProduct] + have hq : x ⬝ᵥ (G.adjMatrix ℝ *ᵥ x) = ∑ v ∈ S, (#(G.neighborFinset v ∩ S) : ℝ) := by + simp [x, dotProduct] + rw [hxx, hq] at h + refine exists_le_of_sum_le hS ?_ + simpa [mul_comm] using h + +omit [Nonempty V] in +theorem exists_coloring_of_low_degree (m : ℕ) + (h : ∀ S : Finset V, S.Nonempty → ∃ v ∈ S, #(G.neighborFinset v ∩ S) ≤ m) + (S : Finset V) : ∃ f : V → Fin (m + 1), ∀ u ∈ S, ∀ w ∈ S, G.Adj u w → f u ≠ f w := by + induction S using Finset.strongInduction with + | H S ih => + rcases S.eq_empty_or_nonempty with rfl | hS + · exact ⟨fun _ => 0, by simp⟩ + obtain ⟨v, hv, hdeg⟩ := h S hS + obtain ⟨f, hf⟩ := ih (S.erase v) (erase_ssubset hv) + have hcard : #(({u ∈ G.neighborFinset v | u ∈ S}).image f) < #(univ : Finset (Fin (m + 1))) := + by + rw [card_univ, Fintype.card_fin] + exact lt_of_le_of_lt (card_image_le.trans hdeg) (Nat.lt_succ_self m) + obtain ⟨c, -, hc⟩ := exists_mem_notMem_of_card_lt_card hcard + refine ⟨Function.update f v c, fun u hu w hw huw => ?_⟩ + have key : ∀ y ∈ S, G.Adj v y → c ≠ f y := by + intro y hy hvy hcy + exact hc (mem_image.2 ⟨y, by simp [hy, hvy], hcy.symm⟩) + by_cases huv : u = v + · subst huv + have hwv : w ≠ u := huw.ne.symm + simpa [hwv] using key w hw huw + by_cases hwv : w = v + · subst hwv + simpa [huv] using (key u hu huw.symm).symm + simpa [huv, hwv] using hf u (mem_erase.2 ⟨huv, hu⟩) w (mem_erase.2 ⟨hwv, hw⟩) huw + +/-- The average degree `2 |E| / n` is at most the largest adjacency eigenvalue. -/ +theorem average_degree_le : + 2 * (#G.edgeFinset : ℝ) / Fintype.card V ≤ ⨆ i, hA.eigenvalues i := by + have h := quadForm_le_iSup hA (fun _ : V => (1 : ℝ)) + have hxx : (fun _ : V => (1 : ℝ)) ⬝ᵥ (fun _ : V => (1 : ℝ)) = Fintype.card V := by + simp [dotProduct] + have hq : (fun _ : V => (1 : ℝ)) ⬝ᵥ (G.adjMatrix ℝ *ᵥ fun _ : V => (1 : ℝ)) = + 2 * (#G.edgeFinset : ℝ) := by + simp only [dotProduct, adjMatrix_mulVec_apply, sum_const, one_mul, + card_neighborFinset_eq_degree, nsmul_eq_mul, mul_one] + exact_mod_cast G.sum_degrees_eq_twice_card_edges + rw [hxx, hq] at h + have hn : (0 : ℝ) < Fintype.card V := by exact_mod_cast Fintype.card_pos + rwa [div_le_iff₀ hn] + +/-- The largest adjacency eigenvalue is at most the maximum degree. -/ +theorem le_maxDegree : ⨆ i, hA.eigenvalues i ≤ G.maxDegree := by + obtain ⟨x, hx, hxx⟩ := exists_unit_eigenvector_iSup hA + set lam := ⨆ i, hA.eigenvalues i + obtain ⟨u, -, hu⟩ := exists_max_image univ (fun v => |x v|) univ_nonempty + have hpos : 0 < |x u| := by + by_contra hneg + have h0 : ∀ v, x v = 0 := fun v => + abs_eq_zero.1 (le_antisymm ((hu v (mem_univ v)).trans (not_lt.1 hneg)) (abs_nonneg _)) + simp [dotProduct, h0] at hxx + have hxu : lam * x u = ∑ w ∈ G.neighborFinset u, x w := by + rw [← adjMatrix_mulVec_apply, hx] + simp + have hbound : |lam| * |x u| ≤ G.maxDegree * |x u| := by + rw [← abs_mul, hxu] + calc |∑ w ∈ G.neighborFinset u, x w| ≤ ∑ w ∈ G.neighborFinset u, |x w| := + abs_sum_le_sum_abs _ _ + _ ≤ ∑ w ∈ G.neighborFinset u, |x u| := sum_le_sum fun w _ => hu w (mem_univ w) + _ = G.degree u * |x u| := by simp + _ ≤ G.maxDegree * |x u| := by + gcongr + exact_mod_cast G.degree_le_maxDegree u + exact (le_abs_self lam).trans (le_of_mul_le_mul_right hbound hpos) + +omit [Nonempty V] in +/-- **Wilf's theorem (1967).** A finite graph is `(⌊λ_max⌋ + 1)`-colourable, where `λ_max` is +the largest eigenvalue of its adjacency matrix. -/ +theorem wilf : G.Colorable (⌊⨆ i, hA.eigenvalues i⌋₊ + 1) := by + obtain ⟨f, hf⟩ := exists_coloring_of_low_degree G ⌊⨆ i, hA.eigenvalues i⌋₊ + (fun S hS => by + obtain ⟨v, hv, hdeg⟩ := exists_low_degree G hA S hS + exact ⟨v, hv, Nat.le_floor hdeg⟩) univ + exact ⟨Coloring.mk f fun {u w} huw => hf u (mem_univ u) w (mem_univ w) huw⟩ + +/-- **Hoffman's bound (1970).** If a finite graph has at least one edge, every proper colouring +with `c` colours satisfies `1 - λ_max / λ_min ≤ c`. -/ +theorem hoffman_chromatic (hE : G.edgeSet.Nonempty) {c : ℕ} (hc : G.Colorable c) : + 1 - (⨆ i, hA.eigenvalues i) / (⨅ i, hA.eigenvalues i) ≤ c := by + obtain ⟨C⟩ := hc + obtain ⟨x, hx, hxx⟩ := exists_unit_eigenvector_iSup hA + set lam := ⨆ i, hA.eigenvalues i + set mu := ⨅ i, hA.eigenvalues i + have hmu : mu ≤ -1 := iInf_eigenvalues_le_neg_one G hA hE + set z : Fin c → V → ℝ := fun j v => if C v = j then x v else 0 + have hzz : ∀ j, z j ⬝ᵥ z j = z j ⬝ᵥ x := fun j => by + simp only [z, dotProduct] + refine sum_congr rfl fun v _ => ?_ + split_ifs <;> simp + have hz0 : ∀ j, 0 ≤ z j ⬝ᵥ x := fun j => by + rw [← hzz] + exact sum_nonneg fun v _ => mul_self_nonneg _ + have hclass : ∀ j, (lam - mu) * (z j ⬝ᵥ x) ≤ -mu := fun j => by + have hind : z j ⬝ᵥ (G.adjMatrix ℝ *ᵥ z j) = 0 := by + refine quadForm_eq_zero_of_indep G _ fun u v huv => ?_ + by_contra hne + push Not at hne + simp only [z, ne_eq, ite_eq_right_iff, not_forall] at hne + exact C.valid huv (hne.1.1.trans hne.2.1.symm) + have h := hoffman_key G hA x (z j) lam (z j ⬝ᵥ x) hx hind + rw [hzz, hxx] at h + rcases (hz0 j).lt_or_eq with hs | hs + · nlinarith + · rw [← hs]; linarith + have hsum : ∑ j, z j ⬝ᵥ x = 1 := by + rw [← hxx] + simp only [z, dotProduct, ite_mul, zero_mul] + rw [sum_comm] + simp + have htot : lam - mu ≤ -(c * mu) := by + have := sum_le_sum fun j (_ : j ∈ (univ : Finset (Fin c))) => hclass j + rw [← mul_sum, hsum] at this + simpa using this + have hneg : mu < 0 := by linarith + have h1 : 1 - (c : ℝ) ≤ lam / mu := by + rw [le_div_iff_of_neg hneg] + linarith + linarith + +/-- **Hoffman's ratio bound.** If a finite graph is `k`-regular with `k ≥ 1`, every independent +set has at most `n (−λ_min) / (k − λ_min)` vertices. -/ +theorem hoffman_ratio {k : ℕ} (hk : 1 ≤ k) (hreg : G.IsRegularOfDegree k) {s : Finset V} + (hs : G.IsIndepSet (s : Set V)) : + (#s : ℝ) ≤ Fintype.card V * (-(⨅ i, hA.eigenvalues i)) / (k - ⨅ i, hA.eigenvalues i) := by + set mu := ⨅ i, hA.eigenvalues i + have hmu : mu ≤ 0 := iInf_eigenvalues_nonpos G hA + set x : V → ℝ := fun _ => 1 + set z : V → ℝ := fun v => if v ∈ s then 1 else 0 + set n : ℝ := (Fintype.card V : ℝ) + set a : ℝ := (#s : ℝ) + have hn : 0 < n := by simp only [n]; exact_mod_cast (Fintype.card_pos : 0 < Fintype.card V) + have hx : G.adjMatrix ℝ *ᵥ x = (k : ℝ) • x := by + ext v + simp [x, hreg v] + have hind : z ⬝ᵥ (G.adjMatrix ℝ *ᵥ z) = 0 := by + refine quadForm_eq_zero_of_indep G _ fun u v huv => ?_ + by_contra hne + push Not at hne + simp only [z, ne_eq, ite_eq_right_iff, not_forall] at hne + exact hs hne.1.1 hne.2.1 huv.ne huv + have hzz : z ⬝ᵥ z = a := by simp [z, a, dotProduct] + have hzx : z ⬝ᵥ x = a := by simp [z, x, a, dotProduct] + have hxx : x ⬝ᵥ x = n := by simp [x, n, dotProduct] + have h := hoffman_key G hA x z k (a / n) hx hind + rw [hzz, hzx, hxx] at h + have hk' : (1 : ℝ) ≤ k := by exact_mod_cast hk + have hden : 0 < (k : ℝ) - mu := by linarith + rw [le_div_iff₀ hden] + have ht : a / n * n = a := div_mul_cancel₀ a hn.ne' + set t := a / n + have ha : 0 ≤ a := by positivity + have h' : mu * (t * n) * (1 - t) ≤ -(k * t ^ 2 * n) := by + have : a = t * n := ht.symm + rw [this] at h + nlinarith + rcases ha.lt_or_eq with hapos | ha0 + · have htpos : 0 < t := by positivity + have h2 : mu * (1 - t) ≤ -(k * t) := by + have h3 : t * n * (mu * (1 - t)) ≤ t * n * (-(k * t)) := by nlinarith + exact le_of_mul_le_mul_left h3 (by positivity) + rw [← ht] + nlinarith + · rw [← ha0] + nlinarith + +end SpectralBounds diff --git a/LeanPool/projects/classical-graph-colouring.yaml b/LeanPool/projects/classical-graph-colouring.yaml new file mode 100644 index 000000000..6be519245 --- /dev/null +++ b/LeanPool/projects/classical-graph-colouring.yaml @@ -0,0 +1,121 @@ +slug: classical-graph-colouring +title: Classical graph colouring through lists, orientations and spectra +summary: >- + Proves Kőnig's edge-colouring theorem for finite bipartite simple graphs by + reusing Lean Pool's Vizing partial-colouring and Kempe-chain infrastructure. + A stable-matching theorem for strict preferences and incomplete acceptability + lists supplies kernels for Galvin's orientation of the line graph. This gives + list edge colouring from lists of size at least the maximum degree and the + Dinitz array theorem. Gallai–Hasse–Roy–Vitaver relates graph colourings to + directed paths, while Wilf's and Hoffman's eigenvalue bounds control the + chromatic and independence numbers. Two interface corollaries turn the + spectral colouring bounds into directed-path bounds. Existing Vizing, + matching-cover, poset and equitable-colouring results are reused or left + in their established Lean Pool projects rather than copied. +branch: graph theory and combinatorics +entry_module: LeanPool.ClassicalGraphColouring +authors: +- Juan Pablo Traverso Gianini +source: + title: The List Chromatic Index of a Bipartite Multigraph + authors: + - Fred Galvin + doi: 10.1006/jctb.1995.1011 + url: https://github.com/jtraverso/galvin-dinitz/tree/0aa98fc17e1e96ec408f7bad3198ce37a08d26fc + github_repo: jtraverso/galvin-dinitz + commit: 0aa98fc17e1e96ec408f7bad3198ce37a08d26fc + note: >- + Formalizes the finite simple-graph case. The Kőnig edge-colouring proof + comes from jtraverso/konig-edge-colouring at + 7c60f7efb69c1747aaf39e5dfa7a89d907cd84ef (Palomar + PALOMAR-2026-10-15-000019). The Galvin, Dinitz and stable-matching + proofs come from PALOMAR-2026-10-18-000029. Gallai–Roy comes from + jtraverso/gallai-roy at e737218bf80c3d3684d670f5f8aa9a8257e1a52f + (PALOMAR-2026-10-16-000015), and the spectral bounds from + jtraverso/spectral-graph-bounds at 8d8b4ce17e56165b5f1ad3b285fb141666804e1c + (PALOMAR-2026-10-18-000016). The source's copied Vizing files are omitted + in favour of the existing Lean Pool project. +license: Apache-2.0 +status: verified +provenance: AI +main_declarations: +- Konig.lineGraph_colorable_of_colorable_two +- Galvin.galvin +- GallaiRoy.colorable_of_orientation +- SpectralBounds.hoffman_chromatic +main_results: +- declaration: Konig.lineGraph_colorable_of_colorable_two + informal: >- + A finite bipartite simple graph has a proper edge colouring using its + maximum degree many colours. + source_ref: Kőnig (1916), doi:10.1007/BF01456961; PALOMAR-2026-10-15-000019. +- declaration: Konig.lineGraph_chromaticNumber_of_colorable_two + informal: The chromatic index of a finite bipartite simple graph equals its maximum degree. + source_ref: Kőnig (1916), doi:10.1007/BF01456961; PALOMAR-2026-10-15-000019. +- declaration: Galvin.gale_shapley + informal: >- + Finite strict-preference matching instances with incomplete acceptability + lists have a stable matching. + source_ref: Gale and Shapley (1962), doi:10.1080/00029890.1962.11989827; PALOMAR-2026-10-18-000029. +- declaration: Galvin.galvin + informal: >- + Every finite bipartite simple graph admits a proper edge colouring from + arbitrary edge lists of size at least its maximum degree. + source_ref: Galvin (1995), doi:10.1006/jctb.1995.1011; PALOMAR-2026-10-18-000029. +- declaration: Galvin.dinitz + informal: >- + An n by n array of lists of at least n symbols per cell admits a choice + of symbols distinct within every row and every column. + source_ref: Galvin (1995), doi:10.1006/jctb.1995.1011; PALOMAR-2026-10-18-000029. +- declaration: GallaiRoy.colorable_of_orientation + informal: >- + If every directed path in an orientation of a finite graph has at most k + vertices, then the graph is k-colourable. + source_ref: Gallai (1968), Hasse (1965), Roy (1967), Vitaver (1962); PALOMAR-2026-10-16-000015. +- declaration: GallaiRoy.exists_orientation_of_colorable + informal: >- + Every k-colourable finite graph has an orientation with no directed path + on more than k vertices. + source_ref: Gallai–Hasse–Roy–Vitaver theorem; PALOMAR-2026-10-16-000015. +- declaration: SpectralBounds.average_degree_le + informal: The average degree of a finite graph is at most its largest adjacency eigenvalue. + source_ref: Collatz–Sinogowitz; PALOMAR-2026-10-18-000016. +- declaration: SpectralBounds.le_maxDegree + informal: The largest adjacency eigenvalue is at most the maximum degree. + source_ref: Collatz–Sinogowitz; PALOMAR-2026-10-18-000016. +- declaration: SpectralBounds.wilf + informal: A finite graph is colourable with floor of its largest adjacency eigenvalue plus one colours. + source_ref: Wilf (1967); PALOMAR-2026-10-18-000016. +- declaration: SpectralBounds.hoffman_chromatic + informal: >- + If a finite graph has an edge, every proper colouring uses at least one + minus the ratio of the largest and smallest adjacency eigenvalues colours. + source_ref: Hoffman (1970); PALOMAR-2026-10-18-000016. +- declaration: SpectralBounds.hoffman_ratio + informal: >- + Every independent set in a finite regular graph satisfies Hoffman's + adjacency-eigenvalue ratio bound. + source_ref: Hoffman (1970); PALOMAR-2026-10-18-000016. +- declaration: ClassicalGraphColouring.hoffman_le_directed_path_bound + informal: >- + Hoffman's spectral lower bound for chromatic number bounds the maximum + directed path length in every orientation. + source_ref: Interface corollary of the proved Hoffman and Gallai–Roy theorems. +- declaration: ClassicalGraphColouring.exists_orientation_of_wilf_bound + informal: >- + Every finite graph has an orientation whose directed paths have at most + floor of its largest adjacency eigenvalue plus one vertices. + source_ref: Interface corollary of the proved Wilf and Gallai–Roy theorems. +tags: +- graph-theory +- bipartite-graphs +- edge-colouring +- list-colouring +- stable-matchings +- orientations +- spectral-graph-theory +msc: +- 05C15 +- 05C70 +- 91B68 +- 05C50 From 28b74d8a8b6d4528c766f4ad4e529076c37e6b38 Mon Sep 17 00:00:00 2001 From: Juan Pablo Traverso Gianini <13575211+jtraverso@users.noreply.github.com> Date: Mon, 19 Oct 2026 08:30:10 -0300 Subject: [PATCH 2/6] docs: clarify spectral hypotheses and bridge digraph paths --- LeanPool/ClassicalGraphColouring.lean | 1 + .../Orientations/GallaiRoy.lean | 12 +++++++++++- LeanPool/projects/classical-graph-colouring.yaml | 7 ++++--- 3 files changed, 16 insertions(+), 4 deletions(-) diff --git a/LeanPool/ClassicalGraphColouring.lean b/LeanPool/ClassicalGraphColouring.lean index 252aeca9b..d5b69f236 100644 --- a/LeanPool/ClassicalGraphColouring.lean +++ b/LeanPool/ClassicalGraphColouring.lean @@ -18,6 +18,7 @@ Kőnig's edge-colouring theorem supplies a proper colouring of a finite bipartit arbitrary edge lists of size at least `Δ(G)`. The development also proves the Gale–Shapley stable-matching theorem used to construct the kernels and deduces the Dinitz array theorem. Gallai–Hasse–Roy–Vitaver relates proper colourings to longest directed paths in orientations. +Its path predicate is bridged to Lean Pool's `Digraph.IsSimplePath` API. Wilf's and Hoffman's bounds compare the chromatic and independence numbers with adjacency eigenvalues. Two interface corollaries below transfer the spectral colouring bounds to directed path statements. diff --git a/LeanPool/ClassicalGraphColouring/Orientations/GallaiRoy.lean b/LeanPool/ClassicalGraphColouring/Orientations/GallaiRoy.lean index 48f5b9a1a..e32f37b72 100644 --- a/LeanPool/ClassicalGraphColouring/Orientations/GallaiRoy.lean +++ b/LeanPool/ClassicalGraphColouring/Orientations/GallaiRoy.lean @@ -6,6 +6,7 @@ Authors: Juan Pablo Traverso Gianini module public import Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex +public import LeanPool.CircuitComplexity.Digraph.Defs public import Mathlib.Tactic /-! @@ -20,7 +21,7 @@ for all consecutive indices. Vitaver (1962).** If some orientation of `G` has no directed path with more than `k` vertices, then `G` is `k`-colourable. * `GallaiRoy.exists_orientation_of_colorable`: conversely, a `k`-colourable graph has an - (acyclic) orientation without directed paths on more than `k` vertices. Together: the + orientation without directed paths on more than `k` vertices. Together: the chromatic number is the minimum, over orientations, of the number of vertices of a longest directed path. -/ @@ -42,6 +43,15 @@ def IsOrientation (G : SimpleGraph V) (o : V → V → Prop) : Prop := def IsDirectedPath (o : V → V → Prop) {m : ℕ} (f : Fin m → V) : Prop := Function.Injective f ∧ ∀ (i : ℕ) (h : i + 1 < m), o (f ⟨i, by omega⟩) (f ⟨i + 1, h⟩) +/-- The relation-based path predicate agrees with Lean Pool's digraph simple-path API. -/ +theorem isDirectedPath_iff_isSimplePath (D : Digraph V) {m : ℕ} (f : Fin m → V) : + IsDirectedPath D.Adj f ↔ D.IsSimplePath f := by + constructor + · rintro ⟨hinj, hstep⟩ + exact ⟨fun i hi => hstep i.val hi, hinj⟩ + · rintro ⟨hstep, hinj⟩ + exact ⟨hinj, fun i hi => hstep ⟨i, by omega⟩ hi⟩ + private lemma transGen_of_mem_isChain {D : V → V → Prop} : ∀ {a : V} {l : List V}, List.IsChain D (a :: l) → ∀ w ∈ l, Relation.TransGen D a w | a, [], _, w, hw => by simp at hw diff --git a/LeanPool/projects/classical-graph-colouring.yaml b/LeanPool/projects/classical-graph-colouring.yaml index 6be519245..d8c193af8 100644 --- a/LeanPool/projects/classical-graph-colouring.yaml +++ b/LeanPool/projects/classical-graph-colouring.yaml @@ -7,7 +7,8 @@ summary: >- lists supplies kernels for Galvin's orientation of the line graph. This gives list edge colouring from lists of size at least the maximum degree and the Dinitz array theorem. Gallai–Hasse–Roy–Vitaver relates graph colourings to - directed paths, while Wilf's and Hoffman's eigenvalue bounds control the + directed paths (with a bridge to Lean Pool's digraph simple-path API), while + Wilf's and Hoffman's eigenvalue bounds control the chromatic and independence numbers. Two interface corollaries turn the spectral colouring bounds into directed-path bounds. Existing Vizing, matching-cover, poset and equitable-colouring results are reused or left @@ -93,8 +94,8 @@ main_results: source_ref: Hoffman (1970); PALOMAR-2026-10-18-000016. - declaration: SpectralBounds.hoffman_ratio informal: >- - Every independent set in a finite regular graph satisfies Hoffman's - adjacency-eigenvalue ratio bound. + Every independent set in a finite regular graph of positive degree + satisfies Hoffman's adjacency-eigenvalue ratio bound. source_ref: Hoffman (1970); PALOMAR-2026-10-18-000016. - declaration: ClassicalGraphColouring.hoffman_le_directed_path_bound informal: >- From cc25bccb916257b3494debf51bd5212255bc4173 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Mon, 19 Oct 2026 16:11:10 +0300 Subject: [PATCH 3/6] fix: remove unused nonempty assumption from Wilf corollary The unused-argument linter identified this instance as unused. Keep the theorem conclusion and proof unchanged while permitting the empty vertex type. --- LeanPool/ClassicalGraphColouring.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LeanPool/ClassicalGraphColouring.lean b/LeanPool/ClassicalGraphColouring.lean index d5b69f236..bd66ef808 100644 --- a/LeanPool/ClassicalGraphColouring.lean +++ b/LeanPool/ClassicalGraphColouring.lean @@ -53,7 +53,7 @@ theorem hoffman_le_directed_path_bound {V : Type*} [Fintype V] [DecidableEq V] [ (GallaiRoy.colorable_of_orientation G o ho k hk) /-- Wilf's spectral colouring bound gives an orientation with the same bound on directed paths. -/ -theorem exists_orientation_of_wilf_bound {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V] +theorem exists_orientation_of_wilf_bound {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hA : (G.adjMatrix ℝ).IsHermitian) : ∃ o : V → V → Prop, GallaiRoy.IsOrientation G o ∧ ∀ (m : ℕ) (f : Fin m → V), GallaiRoy.IsDirectedPath o f → From dd5a81836cbe5757471fdab67eb4f087b73974c4 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Mon, 19 Oct 2026 18:11:46 +0300 Subject: [PATCH 4/6] Regenerate ClassicalGraphColouring project card Generate the entry card from the existing project YAML and preserve the mathematical overview separately. --- LeanPool/ClassicalGraphColouring.lean | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/LeanPool/ClassicalGraphColouring.lean b/LeanPool/ClassicalGraphColouring.lean index bd66ef808..30f450f62 100644 --- a/LeanPool/ClassicalGraphColouring.lean +++ b/LeanPool/ClassicalGraphColouring.lean @@ -11,7 +11,18 @@ public import LeanPool.ClassicalGraphColouring.Orientations.GallaiRoy public import LeanPool.ClassicalGraphColouring.Spectrum.Bounds /-! -# Classical graph colouring by degree, orientations, lists and eigenvalues +# Classical graph colouring through lists, orientations and spectra + +Source: doi:10.1006/jctb.1995.1011, url:https://github.com/jtraverso/galvin-dinitz/tree/0aa98fc17e1e96ec408f7bad3198ce37a08d26fc +Authors: Juan Pablo Traverso Gianini +Status: verified +Main declarations: `Konig.lineGraph_colorable_of_colorable_two`, `Galvin.galvin`, `GallaiRoy.colorable_of_orientation`, `SpectralBounds.hoffman_chromatic` +Tags: graph-theory, bipartite-graphs, edge-colouring, list-colouring, stable-matchings, orientations, spectral-graph-theory +MSC: 05C15, 05C70, 91B68, 05C50 +-/ + +/-! +## Mathematical overview Kőnig's edge-colouring theorem supplies a proper colouring of a finite bipartite graph with `Δ(G)` colours. Galvin's orientation and kernel argument upgrades this to a colouring from @@ -26,15 +37,6 @@ path statements. The proof of Kőnig's theorem reuses `LeanPool.Vizing` directly. The matching-cover and finite poset results from the registered Kőnig source are already available in `LeanPool.ClassicalMatchingFactors` and are not duplicated here. - -Source: doi:10.1006/jctb.1995.1011, -url:https://github.com/jtraverso/galvin-dinitz/tree/0aa98fc17e1e96ec408f7bad3198ce37a08d26fc -Authors: Juan Pablo Traverso Gianini -Status: verified -Main declarations: `Konig.lineGraph_colorable_of_colorable_two`, `Galvin.galvin`, - `GallaiRoy.colorable_of_orientation`, `SpectralBounds.hoffman_chromatic` -Tags: graph-theory, graph-colouring, edge-colouring, orientations, spectral-graph-theory -MSC: 05C15, 05C20, 05C50, 91B68 -/ @[expose] public section From baed8b105bd5fe72c50bb5f0962ade93a7d8a58b Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Mon, 19 Oct 2026 20:16:20 +0300 Subject: [PATCH 5/6] Keep generated graph-colouring card metadata within line limits Use a compact representative declaration/tag list for the generated card. Preserve all fourteen detailed main results, the complete mathematical overview, and every theorem, proof, import and gate. --- LeanPool/ClassicalGraphColouring.lean | 4 ++-- LeanPool/projects/classical-graph-colouring.yaml | 4 ---- 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/LeanPool/ClassicalGraphColouring.lean b/LeanPool/ClassicalGraphColouring.lean index 30f450f62..fbba7812e 100644 --- a/LeanPool/ClassicalGraphColouring.lean +++ b/LeanPool/ClassicalGraphColouring.lean @@ -16,8 +16,8 @@ public import LeanPool.ClassicalGraphColouring.Spectrum.Bounds Source: doi:10.1006/jctb.1995.1011, url:https://github.com/jtraverso/galvin-dinitz/tree/0aa98fc17e1e96ec408f7bad3198ce37a08d26fc Authors: Juan Pablo Traverso Gianini Status: verified -Main declarations: `Konig.lineGraph_colorable_of_colorable_two`, `Galvin.galvin`, `GallaiRoy.colorable_of_orientation`, `SpectralBounds.hoffman_chromatic` -Tags: graph-theory, bipartite-graphs, edge-colouring, list-colouring, stable-matchings, orientations, spectral-graph-theory +Main declarations: `Galvin.galvin`, `SpectralBounds.hoffman_chromatic` +Tags: graph-theory, edge-colouring, list-colouring, orientations, spectral-graph-theory MSC: 05C15, 05C70, 91B68, 05C50 -/ diff --git a/LeanPool/projects/classical-graph-colouring.yaml b/LeanPool/projects/classical-graph-colouring.yaml index d8c193af8..ddeb4d811 100644 --- a/LeanPool/projects/classical-graph-colouring.yaml +++ b/LeanPool/projects/classical-graph-colouring.yaml @@ -40,9 +40,7 @@ license: Apache-2.0 status: verified provenance: AI main_declarations: -- Konig.lineGraph_colorable_of_colorable_two - Galvin.galvin -- GallaiRoy.colorable_of_orientation - SpectralBounds.hoffman_chromatic main_results: - declaration: Konig.lineGraph_colorable_of_colorable_two @@ -109,10 +107,8 @@ main_results: source_ref: Interface corollary of the proved Wilf and Gallai–Roy theorems. tags: - graph-theory -- bipartite-graphs - edge-colouring - list-colouring -- stable-matchings - orientations - spectral-graph-theory msc: From 9866b02d9e00445c9ea4816f92fa8a289a90fef9 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Mon, 19 Oct 2026 23:11:56 +0300 Subject: [PATCH 6/6] Cite Haemers for Hoffman's independent-set ratio bound Point the independent-set ratio result to Haemers2021 Theorem1. Keep Hoffman's1970 reference for the chromatic bound and preserve all theorem statements, proofs and other project metadata. --- LeanPool/projects/classical-graph-colouring.yaml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/LeanPool/projects/classical-graph-colouring.yaml b/LeanPool/projects/classical-graph-colouring.yaml index ddeb4d811..74ed35c2b 100644 --- a/LeanPool/projects/classical-graph-colouring.yaml +++ b/LeanPool/projects/classical-graph-colouring.yaml @@ -94,7 +94,9 @@ main_results: informal: >- Every independent set in a finite regular graph of positive degree satisfies Hoffman's adjacency-eigenvalue ratio bound. - source_ref: Hoffman (1970); PALOMAR-2026-10-18-000016. + source_ref: >- + Hoffman's ratio bound, stated in Haemers (2021), Theorem 1, + https://arxiv.org/abs/2102.05529v2; PALOMAR-2026-10-18-000016. - declaration: ClassicalGraphColouring.hoffman_le_directed_path_bound informal: >- Hoffman's spectral lower bound for chromatic number bounds the maximum