Classical graph colouring: lists, orientations and spectra

LeanPool/ClassicalGraphColouring.lean

@@ -0,0 +1,65 @@
+/-
+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 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: `Galvin.galvin`, `SpectralBounds.hoffman_chromatic`
+Tags: graph-theory, edge-colouring, list-colouring, 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
+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.
+
+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.
+-/
+
+@[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]
+    (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

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

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