Import the Goldberg–Seymour edge-coloring theorem

LeanPool/GoldbergSeymour.lean

@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2026 Wesley Pegden. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wesley Pegden
+-/
+
+module
+
+public import LeanPool.GoldbergSeymour.MathlibGraph
+
+/-!
+# The Goldberg–Seymour edge-coloring theorem
+
+Source: arxiv:1901.10316v2, url:https://github.com/wpegden/goldberg_seymour/tree/88d98c1d1a59d1f1bf7c4eb58e73f3945f6daf12
+Authors: Wesley Pegden
+Status: verified
+Main declarations: `GoldbergSeymour.goldbergSeymour`, `GoldbergSeymour.GeneralHighIndexElementary`
+Tags: graph-theory, edge-coloring, multigraphs, tashkinov-trees
+MSC: 05C15
+-/
+
+/-!
+Formalized by Trellis, operated by Wesley Pegden, following the mathematical
+theorem of Guantao Chen, Guangming Jing and Wenan Zang, arXiv:1901.10316v2.
+Adapted from wpegden/goldberg_seymour at
+88d98c1d1a59d1f1bf7c4eb58e73f3945f6daf12.
+-/
+
+@[expose] public section
+
+namespace GoldbergSeymour
+
+/-- The Goldberg–Seymour bound for the chromatic index of a finite loopless multigraph. -/
+theorem goldbergSeymour {V E : Type*} [Fintype V] [Fintype E]
+    (G : LooplessMultigraph V E) :
+    ChromaticIndex G ≤ max (MaximumDegree G + 1) (DensityCeil G) := by
+  classical
+  exact ThmGS G
+
+end GoldbergSeymour
+
+end

LeanPool/GoldbergSeymour/AbsorbingVertex.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2026 Wesley Pegden. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wesley Pegden
+-/
+module
+
+public import LeanPool.GoldbergSeymour.TreeFreeColors
+public import LeanPool.GoldbergSeymour.TwoColorComponent
+
+/-!
+# Absorbing Vertex
+
+Part of the dependency closure of the Goldberg–Seymour edge-colouring theorem.
+Adapted from Wesley Pegden’s Trellis formalization at
+88d98c1d1a59d1f1bf7c4eb58e73f3945f6daf12; module paths and namespace changed.
+-/
+
+@[expose] public section
+
+namespace GoldbergSeymour
+
+/--
+An outside vertex whose two-color components select unique missing-color witnesses in the tree. -/
+def AbsorbingVertex {V E : Type*} [Fintype E] {G : LooplessMultigraph V E} {k : ℕ}
+  {e0 : E} (T : TreeSequence G e0) (phi : PartialEdgeColoring E k) (v : V) : Prop :=
+ v ∉ TreeSequenceVertexSet T ∧
+  ∀ delta ∈ MissingColors G phi v,
+   ∀ gamma ∈ TreeFreeColors phi T,
+    gamma ≠ delta →
+     ∃ u : V,
+      u ∈ TreeSequenceVertexSet T ∧
+       gamma ∈ MissingColors G phi u ∧
+        Sum.inl u ∈ TwoColorComponent G phi gamma delta (Sum.inl v) ∧
+         ∀ w ∈ TreeSequenceVertexSet T, gamma ∈ MissingColors G phi w → w = u
+
+end GoldbergSeymour
+
+end

LeanPool/GoldbergSeymour/AbsorbingVertices.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2026 Wesley Pegden. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wesley Pegden
+-/
+module
+
+public import LeanPool.GoldbergSeymour.AbsorbingVertex
+
+/-!
+# Absorbing Vertices
+
+Part of the dependency closure of the Goldberg–Seymour edge-colouring theorem.
+Adapted from Wesley Pegden’s Trellis formalization at
+88d98c1d1a59d1f1bf7c4eb58e73f3945f6daf12; module paths and namespace changed.
+-/
+
+@[expose] public section
+
+namespace GoldbergSeymour
+
+/-- Outside vertices satisfying the absorbing-vertex condition for the given coloring and tree. -/
+noncomputable def AbsorbingVertices {V E : Type*} [Fintype V] [Fintype E]
+    {G : LooplessMultigraph V E} {k : ℕ} {e0 : E} (T : TreeSequence G e0)
+    (phi : PartialEdgeColoring E k) : Finset V := by
+  classical
+  exact Finset.univ.filter fun v => AbsorbingVertex T phi v
+
+end GoldbergSeymour
+
+end

LeanPool/GoldbergSeymour/AdjacentEdges.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2026 Wesley Pegden. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wesley Pegden
+-/
+module
+
+public import LeanPool.GoldbergSeymour.Incident
+
+/-!
+# Adjacent Edges
+
+Part of the dependency closure of the Goldberg–Seymour edge-colouring theorem.
+Adapted from Wesley Pegden’s Trellis formalization at
+88d98c1d1a59d1f1bf7c4eb58e73f3945f6daf12; module paths and namespace changed.
+-/
+
+@[expose] public section
+
+namespace GoldbergSeymour
+
+/-- Two edges are adjacent when they have a common incident vertex. -/
+def AdjacentEdges {V E : Type*} (G : LooplessMultigraph V E) (e f : E) : Prop :=
+ ∃ v, Incident G v e ∧ Incident G v f
+
+end GoldbergSeymour
+
+end