diff --git a/LeanPool/ClassicalGraphColouring.lean b/LeanPool/ClassicalGraphColouring.lean
new file mode 100644
index 000000000..fbba7812e
--- /dev/null
+++ b/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
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..e32f37b72
--- /dev/null
+++ b/LeanPool/ClassicalGraphColouring/Orientations/GallaiRoy.lean
@@ -0,0 +1,180 @@
+/-
+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 LeanPool.CircuitComplexity.Digraph.Defs
+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
+  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⟩)
+
+/-- 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
+  | 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..74ed35c2b
--- /dev/null
+++ b/LeanPool/projects/classical-graph-colouring.yaml
@@ -0,0 +1,120 @@
+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 (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
+  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:
+- Galvin.galvin
+- 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 of positive degree
+    satisfies Hoffman's adjacency-eigenvalue ratio bound.
+  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
+    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
+- edge-colouring
+- list-colouring
+- orientations
+- spectral-graph-theory
+msc:
+- 05C15
+- 05C70
+- 91B68
+- 05C50