From 1ca35544a4b1fbd32bf377493df8e11ca3e2417a Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sat, 17 Oct 2026 09:27:32 +0000 Subject: [PATCH 1/4] =?UTF-8?q?Import=20Nash-Williams=E2=80=93Tutte=20tree?= =?UTF-8?q?=20packing=20and=20arboricity?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanPool/NashWilliamsTutte.lean | 35 ++ LeanPool/NashWilliamsTutte/Auxiliary.lean | 427 +++++++++++++++++++++ LeanPool/NashWilliamsTutte/Imports.lean | 11 + LeanPool/NashWilliamsTutte/Theorems.lean | 237 ++++++++++++ LeanPool/projects/nash-williams-tutte.yaml | 50 +++ 5 files changed, 760 insertions(+) create mode 100644 LeanPool/NashWilliamsTutte.lean create mode 100644 LeanPool/NashWilliamsTutte/Auxiliary.lean create mode 100644 LeanPool/NashWilliamsTutte/Imports.lean create mode 100644 LeanPool/NashWilliamsTutte/Theorems.lean create mode 100644 LeanPool/projects/nash-williams-tutte.yaml diff --git a/LeanPool/NashWilliamsTutte.lean b/LeanPool/NashWilliamsTutte.lean new file mode 100644 index 000000000..cf23abe40 --- /dev/null +++ b/LeanPool/NashWilliamsTutte.lean @@ -0,0 +1,35 @@ +/- +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.NashWilliamsTutte.Theorems + + +/-! +# Nash-Williams–Tutte tree packing and arboricity + +Source: doi:10.1112/jlms/s1-36.1.445, url:https://github.com/jtraverso/nash-williams-trees/tree/101e48847a929dd8102521f57723e2137989ce2e +Authors: Juan Pablo Traverso Gianini +Status: verified +Main declarations: `NashWilliamsTutte.tree_packing`, `NashWilliamsTutte.arboricity` +Tags: graph-theory, tree-packing, arboricity, edge-connectivity +MSC: 05C05, 05C70, 05C40 +-/ + +/-! +# Nash-Williams–Tutte tree packing and arboricity + +Adapted from jtraverso/nash-williams-trees at +101e48847a929dd8102521f57723e2137989ce2e. +The proofs were generated by Harmonic's Aristotle from statements and a proof plan +prepared by Juan Pablo Traverso Gianini with Claude Code. + +These are the finite simple-graph versions of the tree-packing theorem of +Nash-Williams (1961), doi:10.1112/jlms/s1-36.1.445, and Tutte (1961), +doi:10.1112/jlms/s1-36.1.221, and the arboricity theorem of Nash-Williams (1964), +doi:10.1112/jlms/s1-39.1.12. The upstream proof plan follows Diestel, +*Graph Theory*, fifth edition, Section 2.4, doi:10.1007/978-3-662-53622-3. +-/ diff --git a/LeanPool/NashWilliamsTutte/Auxiliary.lean b/LeanPool/NashWilliamsTutte/Auxiliary.lean new file mode 100644 index 000000000..6a67d632a --- /dev/null +++ b/LeanPool/NashWilliamsTutte/Auxiliary.lean @@ -0,0 +1,427 @@ +/- +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.Acyclic +public import Mathlib.Data.Set.Card.Arithmetic +public import Mathlib.Data.Set.Finite.Lemmas + +/-! +# Auxiliary lemmas for the Nash-Williams–Tutte theorems + +General counting lemmas for forests and connected graphs, and the core exchange lemma: for any +finite graph `G` there are `k` edge-disjoint forests `F i ≤ G` and a subgraph `H ≤ G` such that +each `F i ⊓ H` has the same connected components as `H`, and every edge of `G` outside `H` is +covered by some `F i`. +-/ + +public section + +open Finset Fintype SimpleGraph Function + +namespace NashWilliamsTutte + +variable {V : Type*} + +/-- Reachability transfers along a map that sends adjacent vertices to reachable ones. -/ +theorem reachable_map_of_adj {W : Type*} {A : SimpleGraph V} {B : SimpleGraph W} (g : V → W) + (h : ∀ a b, A.Adj a b → B.Reachable (g a) (g b)) {a b : V} (hab : A.Reachable a b) : + B.Reachable (g a) (g b) := by + obtain ⟨p⟩ := hab + induction p with + | nil => rfl + | cons hadj _ ih => exact (h _ _ hadj).trans ih + +/-- A predicate closed under adjacency is closed under reachability. -/ +theorem reachable_closed {A : SimpleGraph V} (P : V → Prop) (h : ∀ a b, A.Adj a b → P a → P b) + {a b : V} (hab : A.Reachable a b) (ha : P a) : P b := by + obtain ⟨p⟩ := hab + induction p with + | nil => exact ha + | cons hadj _ ih => exact ih (h _ _ hadj ha) + +/-- Disjointness of simple graphs in terms of adjacency. -/ +theorem disjoint_iff_adj {A B : SimpleGraph V} : + Disjoint A B ↔ ∀ a b, A.Adj a b → ¬ B.Adj a b := by + rw [← disjoint_edgeSet, Set.disjoint_left] + constructor + · intro h a b ha hb + exact h (show s(a, b) ∈ A.edgeSet from ha) hb + · intro h e + induction e using Sym2.ind with + | _ a b => exact fun ha hb ↦ h a b ha hb + +/-- The sum of the sizes of pairwise disjoint subsets of a finite set is at most its size. -/ +theorem sum_ncard_le_of_pairwise_disjoint {ι α : Type*} [Fintype ι] [Finite α] (A : ι → Set α) + (B : Set α) (hAB : ∀ i, A i ⊆ B) (hd : Pairwise (Disjoint on A)) : + ∑ i, (A i).ncard ≤ B.ncard := by + have h := Set.ncard_iUnion_of_finite (s := A) (fun i ↦ Set.toFinite _) hd + rw [finsum_eq_sum_of_fintype] at h + rw [← h] + exact Set.ncard_le_ncard (Set.iUnion_subset hAB) + +/-- A forest on a finite nonempty vertex type has at most `|V| - 1` edges, and exactly `|V| - 1` +only if it is a tree. -/ +theorem IsAcyclic.ncard_edgeSet_add_one_le [Finite V] [Nonempty V] {F : SimpleGraph V} + (hF : F.IsAcyclic) : + F.edgeSet.ncard + 1 ≤ Nat.card V ∧ (Nat.card V ≤ F.edgeSet.ncard + 1 → F.IsTree) := by + obtain ⟨T, hFT, hT⟩ := exists_maximal_isAcyclic_of_le_isAcyclic (le_top : F ≤ ⊤) hF + have hT' : T.IsTree := by + rw [← maximal_isAcyclic_iff_isTree] + exact ⟨hT.1.2, fun H hH hle ↦ hT.2 ⟨le_top, hH⟩ hle⟩ + have hcard := (isTree_iff_connected_and_card.1 hT').2 + rw [Nat.card_coe_set_eq] at hcard + have hsub : F.edgeSet ⊆ T.edgeSet := edgeSet_mono hFT + have hle : F.edgeSet.ncard ≤ T.edgeSet.ncard := Set.ncard_le_ncard hsub + refine ⟨by omega, fun h ↦ ?_⟩ + have heq : F.edgeSet = T.edgeSet := Set.eq_of_subset_of_ncard_le hsub (by omega) + rwa [edgeSet_inj.1 heq] + +/-- If every vertex `v` is reachable in `K` from `f v`, then `K` has at least +`|V| - #(image f)` edges. -/ +theorem card_le_ncard_edgeSet_add_card_image [Fintype V] [DecidableEq V] [Nonempty V] + (K : SimpleGraph V) (f : V → V) (hf : ∀ v, K.Reachable v (f v)) : + Nat.card V ≤ K.edgeSet.ncard + #(univ.image f) := by + set r₀ := f (Classical.arbitrary V) + have hr₀ : r₀ ∈ univ.image f := mem_image_of_mem _ (mem_univ _) + set St : Set (Sym2 V) := (fun r ↦ s(r₀, r)) '' ↑((univ.image f).erase r₀) + set L := K ⊔ fromEdgeSet St + have hreach : ∀ a, L.Reachable a r₀ := by + intro a + refine ((hf a).mono le_sup_left).trans ?_ + by_cases ha : f a = r₀ + · rw [ha] + · refine Adj.reachable (Or.inr ?_) + refine ⟨⟨f a, ?_, ?_⟩, ha⟩ + · simp [ha] + · exact Sym2.eq_swap + have hL : L.Connected := by + have : Nonempty V := inferInstance + exact Connected.mk fun a b ↦ (hreach a).trans (hreach b).symm + have h1 := hL.card_vert_le_card_edgeSet_add_one + rw [Nat.card_coe_set_eq] at h1 + have h2 : L.edgeSet.ncard ≤ K.edgeSet.ncard + St.ncard := by + refine (Set.ncard_le_ncard (t := K.edgeSet ∪ St) ?_).trans (Set.ncard_union_le _ _) + rw [edgeSet_sup, edgeSet_fromEdgeSet] + exact Set.union_subset_union_right _ Set.sdiff_subset + have h3 : St.ncard ≤ #(univ.image f) - 1 := by + refine (Set.ncard_image_le (Set.toFinite _)).trans ?_ + rw [Set.ncard_coe_finset, card_erase_of_mem hr₀] + have h4 : 1 ≤ #(univ.image f) := card_pos.2 ⟨_, hr₀⟩ + omega + +/-- A connected graph has at least `m - 1` edges joining different fibres of `f`, where `m` is the +number of nonempty fibres. -/ +theorem card_image_le_ncard_crossing_add_one [Fintype V] [DecidableEq V] {T : SimpleGraph V} + (hT : T.Connected) (f : V → V) : + #(univ.image f) ≤ (T.edgeSet ∩ ((⊤ : SimpleGraph V).comap f).edgeSet).ncard + 1 := by + set W := ↥(univ.image f) + let g : V → W := fun a ↦ ⟨f a, mem_image_of_mem _ (mem_univ a)⟩ + let Q : SimpleGraph W := SimpleGraph.fromRel fun p q ↦ ∃ a b, T.Adj a b ∧ g a = p ∧ g b = q + have hg : ∀ p : W, ∃ a, g a = p := by + rintro ⟨p, hp⟩ + obtain ⟨a, -, rfl⟩ := mem_image.1 hp + exact ⟨a, rfl⟩ + have hQ : Q.Connected := by + have : Nonempty V := hT.nonempty + have : Nonempty W := ⟨g (Classical.arbitrary V)⟩ + refine Connected.mk fun p q ↦ ?_ + obtain ⟨a, rfl⟩ := hg p + obtain ⟨b, rfl⟩ := hg q + refine reachable_map_of_adj g (fun x y hxy ↦ ?_) (hT.preconnected a b) + by_cases hxy' : g x = g y + · rw [hxy'] + · exact Adj.reachable ((fromRel_adj _ _ _).2 ⟨hxy', Or.inl ⟨x, y, hxy, rfl, rfl⟩⟩) + have h1 := hQ.card_vert_le_card_edgeSet_add_one + rw [Nat.card_coe_set_eq, Nat.card_eq_fintype_card, Fintype.card_coe] at h1 + have h2 : Q.edgeSet ⊆ Sym2.map g '' (T.edgeSet ∩ ((⊤ : SimpleGraph V).comap f).edgeSet) := by + intro e he + induction e using Sym2.ind with + | _ p q => + have he' : Q.Adj p q := he + obtain ⟨hpq, h | h⟩ := (fromRel_adj _ _ _).1 he' + · obtain ⟨a, b, hab, rfl, rfl⟩ := h + refine ⟨s(a, b), ⟨hab, ?_⟩, rfl⟩ + exact fun h' ↦ hpq (Subtype.ext h') + · obtain ⟨a, b, hab, rfl, rfl⟩ := h + refine ⟨s(a, b), ⟨hab, ?_⟩, Sym2.eq_swap⟩ + exact fun h' ↦ hpq (Subtype.ext h'.symm) + have h3 := (Set.ncard_le_ncard h2 (Set.toFinite _)).trans (Set.ncard_image_le (Set.toFinite _)) + omega + +/-- Deleting an edge of the unique path between `u` and `v` in a forest disconnects `u` from +`v`. -/ +theorem not_reachable_deleteEdges_of_mem_edges {F : SimpleGraph V} (hF : F.IsAcyclic) {u v x y : V} + (p : F.Walk u v) (hp : p.IsPath) (he : s(x, y) ∈ p.edges) : + ¬ (F.deleteEdges {s(x, y)}).Reachable u v := by + classical + rintro ⟨q⟩ + have hq : (q.bypass.mapLe (deleteEdges_le _)).IsPath := (Walk.isPath_mapLe _).2 q.bypass_isPath + have := (hF.subsingleton_path u v).elim ⟨p, hp⟩ ⟨_, hq⟩ + simp only [Subtype.mk.injEq] at this + rw [this, Walk.edges_mapLe_eq_edges] at he + have := q.bypass.edges_subset_edgeSet he + simp [edgeSet_deleteEdges] at this + +section Exchange + +variable (G : SimpleGraph V) {k : ℕ} + +/-- `k` pairwise edge-disjoint forests in `G`. -/ +def ValidForests (F : Fin k → SimpleGraph V) : Prop := + (∀ i, F i ≤ G ∧ (F i).IsAcyclic) ∧ Pairwise fun i j ↦ Disjoint (F i) (F j) + +/-- The totalEdges number of edges of a family of graphs. -/ +noncomputable def totalEdges (F : Fin k → SimpleGraph V) : ℕ := ∑ i, (F i).edgeSet.ncard + +/-- `uv` is an edge of `G` not covered by the family `F`. -/ +def Uncovered (F : Fin k → SimpleGraph V) (u v : V) : Prop := G.Adj u v ∧ ∀ j, ¬ (F j).Adj u v + +/-- One exchange step: an uncovered edge `uv` replaces an edge `xy` of some `F i`, keeping it +acyclic. -/ +def ExchangeStep (F F' : Fin k → SimpleGraph V) : Prop := + ∃ i u v x y, Uncovered G F u v ∧ (F i).Adj x y ∧ + ((F i).deleteEdges {s(x, y)} ⊔ edge u v).IsAcyclic ∧ + F' = update F i ((F i).deleteEdges {s(x, y)} ⊔ edge u v) + +variable {G} + +theorem total_update (F : Fin k → SimpleGraph V) (i : Fin k) (X : SimpleGraph V) : + totalEdges (update F i X) + (F i).edgeSet.ncard = totalEdges F + X.edgeSet.ncard := by + simp only [totalEdges] + rw [show (fun j ↦ (update F i X j).edgeSet.ncard) = + update (fun j ↦ (F j).edgeSet.ncard) i X.edgeSet.ncard from + funext fun j ↦ apply_update (fun _ (H : SimpleGraph V) ↦ H.edgeSet.ncard) F i X j] + rw [Finset.sum_update_of_mem (mem_univ i), Finset.sdiff_singleton_eq_erase] + have := Finset.add_sum_erase univ (fun j ↦ (F j).edgeSet.ncard) (mem_univ i) + omega + +theorem Uncovered.adj_iff {F : Fin k → SimpleGraph V} {u v : V} (h : Uncovered G F u v) {j : Fin k} + {a b : V} (hab : s(a, b) = s(u, v)) : ¬ (F j).Adj a b := by + rcases Sym2.eq_iff.1 hab with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ + · exact h.2 j + · exact fun h' ↦ h.2 j h'.symm + +theorem adj_new {F : SimpleGraph V} {x y u v a b : V} + (h : (F.deleteEdges {s(x, y)} ⊔ edge u v).Adj a b) : + (F.Adj a b ∧ s(a, b) ≠ s(x, y)) ∨ s(a, b) = s(u, v) := by + rcases h with h | h + · rw [deleteEdges_adj] at h + exact Or.inl ⟨h.1, h.2⟩ + · rw [edge_adj] at h + right + rcases h.1 with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ + · rfl + · exact Sym2.eq_swap + +/-- Replacing `F i` by a graph `X ≤ G` whose edges are edges of `F i` or uncovered edges keeps +the family valid, provided `X` is acyclic. -/ +theorem ValidForests.update {F : Fin k → SimpleGraph V} (hF : ValidForests G F) + (i : Fin k) {X : SimpleGraph V} + (hXG : X ≤ G) (hX : X.IsAcyclic) + (hXadj : ∀ a b, X.Adj a b → (F i).Adj a b ∨ ∀ j, ¬ (F j).Adj a b) : + ValidForests G (update F i X) := by + refine ⟨fun j ↦ ?_, fun j₁ j₂ hj ↦ ?_⟩ + · by_cases hj : j = i + · subst hj; simpa using ⟨hXG, hX⟩ + · simpa [hj] using hF.1 j + · have key : ∀ j, j ≠ i → Disjoint X (F j) := by + intro j hji + rw [disjoint_iff_adj] + intro a b hab + rcases hXadj a b hab with h | h + · exact (disjoint_iff_adj.1 (hF.2 (Ne.symm hji))) a b h + · exact h j + by_cases h₁ : j₁ = i + · subst h₁ + simpa [Ne.symm hj] using key j₂ (Ne.symm hj) + · by_cases h₂ : j₂ = i + · subst h₂ + simpa [h₁] using (key j₁ h₁).symm + · simpa [h₁, h₂] using hF.2 hj + +theorem ExchangeStep.valid {F F' : Fin k → SimpleGraph V} (hF : ValidForests G F) + (h : ExchangeStep G F F') : + ValidForests G F' := by + obtain ⟨i, u, v, x, y, huv, hxy, hac, rfl⟩ := h + refine hF.update i (sup_le ((deleteEdges_le _).trans (hF.1 i).1) + ((edge_le_iff _).2 (Or.inr huv.1))) hac fun a b hab ↦ ?_ + rcases adj_new hab with h | h + · exact Or.inl h.1 + · exact Or.inr fun j ↦ huv.adj_iff h + +theorem ExchangeStep.total_eq [Finite V] {F F' : Fin k → SimpleGraph V} (h : ExchangeStep G F F') : + totalEdges F' = totalEdges F := by + obtain ⟨i, u, v, x, y, huv, hxy, hac, rfl⟩ := h + have h1 := total_update F i ((F i).deleteEdges {s(x, y)} ⊔ edge u v) + have hne : u ≠ v := huv.1.ne + have h2 : ((F i).deleteEdges {s(x, y)} ⊔ edge u v).edgeSet.ncard = (F i).edgeSet.ncard := by + rw [edgeSet_sup, edgeSet_deleteEdges, edgeSet_edge_of_ne hne, + Set.ncard_union_eq (Set.disjoint_singleton_right.2 fun h ↦ huv.2 i h.1) (Set.toFinite _) + (Set.toFinite _), Set.ncard_singleton] + exact Set.ncard_sdiff_singleton_add_one (show s(x, y) ∈ (F i).edgeSet from hxy) + (Set.toFinite _) + omega + +/-- In a family with the maximum totalEdges number of edges, the endpoints of an uncovered edge are +joined in every forest. -/ +theorem reachable_of_uncovered [Finite V] {F : Fin k → SimpleGraph V} (hF : ValidForests G F) + (hmax : ∀ F' : Fin k → SimpleGraph V, ValidForests G F' → totalEdges F' ≤ totalEdges F) + {u v : V} + (huv : Uncovered G F u v) (i : Fin k) : + (F i).Reachable u v := by + by_contra h + have hval : ValidForests G (update F i (F i ⊔ edge u v)) := by + refine hF.update i (sup_le (hF.1 i).1 ((edge_le_iff _).2 (Or.inr huv.1))) + ((hF.1 i).2.sup_edge_of_not_reachable h) fun a b hab ↦ ?_ + rcases hab with hab | hab + · exact Or.inl hab + · right + intro j + apply huv.adj_iff + rw [edge_adj] at hab + rcases hab.1 with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ + · rfl + · exact Sym2.eq_swap + have h1 := total_update F i (F i ⊔ edge u v) + have h2 : (F i ⊔ edge u v).edgeSet.ncard = (F i).edgeSet.ncard + 1 := by + rw [edgeSet_sup, edgeSet_edge_of_ne huv.1.ne, + Set.ncard_union_eq + (Set.disjoint_singleton_right.2 (show s(u, v) ∉ (F i).edgeSet from huv.2 i)) + (Set.toFinite _) + (Set.toFinite _), Set.ncard_singleton] + have h3 := hmax _ hval + omega + +theorem ExchangeStep.uncovered {F : Fin k → SimpleGraph V} (hF : ValidForests G F) + {i : Fin k} {u v x y : V} + (huv : Uncovered G F u v) (hxy : (F i).Adj x y) : + Uncovered G (update F i ((F i).deleteEdges {s(x, y)} ⊔ edge u v)) x y := by + refine ⟨(hF.1 i).1 hxy, fun j ↦ ?_⟩ + by_cases hj : j = i + · subst hj + simp only [update_self] + intro h + rcases adj_new h with h | h + · exact h.2 rfl + · exact huv.adj_iff h hxy + · simp only [update_of_ne hj] + exact disjoint_iff_adj.1 (hF.2 (Ne.symm hj)) x y hxy + +end Exchange + +section Core + +variable {G : SimpleGraph V} {k : ℕ} + +/-- The graph of all edges of `G` that are uncovered in some family obtained from `F₀` by a +sequence of exchange steps. -/ +def exchangeGraph (G : SimpleGraph V) (F₀ : Fin k → SimpleGraph V) : SimpleGraph V where + Adj a b := ∃ F, Relation.ReflTransGen (ExchangeStep G) F₀ F ∧ Uncovered G F a b + symm := ⟨fun _ _ ⟨F, h, hu⟩ ↦ ⟨F, h, hu.1.symm, fun j h' ↦ hu.2 j h'.symm⟩⟩ + loopless := ⟨fun _ ⟨_, _, hu⟩ ↦ hu.1.ne rfl⟩ + +theorem exchangeGraph_adj {F₀ : Fin k → SimpleGraph V} {a b : V} : + (exchangeGraph G F₀).Adj a b ↔ + ∃ F, Relation.ReflTransGen (ExchangeStep G) F₀ F ∧ Uncovered G F a b := + Iff.rfl + +variable [Finite V] {F₀ : Fin k → SimpleGraph V} (hF₀ : ValidForests G F₀) + (hmax : ∀ F : Fin k → SimpleGraph V, ValidForests G F → totalEdges F ≤ totalEdges F₀) +include hF₀ hmax + +omit hmax in +theorem reach_valid {F : Fin k → SimpleGraph V} (hF : Relation.ReflTransGen (ExchangeStep G) F₀ F) : + ValidForests G F ∧ totalEdges F = totalEdges F₀ := by + induction hF with + | refl => exact ⟨hF₀, rfl⟩ + | tail _ hstep ih => exact ⟨hstep.valid ih.1, hstep.total_eq.trans ih.2⟩ + +theorem reach_uncovered_reachable {F : Fin k → SimpleGraph V} + (hF : Relation.ReflTransGen (ExchangeStep G) F₀ F) {u v : V} + (huv : Uncovered G F u v) (i : Fin k) : + (F i ⊓ exchangeGraph G F₀).Reachable u v := by + classical + obtain ⟨hval, htot⟩ := reach_valid hF₀ hF + have hr := reachable_of_uncovered hval (fun F' hF' ↦ htot ▸ hmax F' hF') huv i + obtain ⟨w⟩ := hr + set p := w.bypass + have hp : p.IsPath := w.bypass_isPath + refine ⟨p.transfer _ fun e he ↦ ?_⟩ + induction e using Sym2.ind with + | _ x y => + have hxy : (F i).Adj x y := p.edges_subset_edgeSet he + refine ⟨hxy, exchangeGraph_adj.2 + ⟨update F i ((F i).deleteEdges {s(x, y)} ⊔ edge u v), ?_, + ExchangeStep.uncovered hval huv hxy⟩⟩ + refine hF.tail ⟨i, u, v, x, y, huv, hxy, ?_, rfl⟩ + exact ((hval.1 i).2.anti (deleteEdges_le _)).sup_edge_of_not_reachable + (not_reachable_deleteEdges_of_mem_edges (hval.1 i).2 p hp he) + +theorem step_reachable_iff {F F' : Fin k → SimpleGraph V} + (hF : Relation.ReflTransGen (ExchangeStep G) F₀ F) (hstep : ExchangeStep G F F') + (j : Fin k) (a b : V) : + (F j ⊓ exchangeGraph G F₀).Reachable a b ↔ (F' j ⊓ exchangeGraph G F₀).Reachable a b := by + classical + have hF' : Relation.ReflTransGen (ExchangeStep G) F₀ F' := hF.tail hstep + have hval := (reach_valid hF₀ hF).1 + obtain ⟨i, u, v, x, y, huv, hxy, hac, rfl⟩ := hstep + by_cases hj : j = i + swap + · simp only [update_of_ne hj] + subst hj + simp only [update_self] + constructor + · refine reachable_map_of_adj id fun c d hcd ↦ ?_ + by_cases hc : s(c, d) = s(x, y) + · have h := reach_uncovered_reachable hF₀ hmax hF' (ExchangeStep.uncovered hval huv hxy) j + simp only [update_self] at h + rcases Sym2.eq_iff.1 hc with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ + · exact h + · exact h.symm + · exact Adj.reachable + ⟨Or.inl (deleteEdges_adj.2 ⟨hcd.1, fun h ↦ hc (Set.mem_singleton_iff.1 h)⟩), hcd.2⟩ + · refine reachable_map_of_adj id fun c d hcd ↦ ?_ + rcases adj_new hcd.1 with h | h + · exact Adj.reachable ⟨h.1, hcd.2⟩ + · have h' := reach_uncovered_reachable hF₀ hmax hF huv j + rcases Sym2.eq_iff.1 h with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ + · exact h' + · exact h'.symm + +theorem reach_reachable_iff {F : Fin k → SimpleGraph V} + (hF : Relation.ReflTransGen (ExchangeStep G) F₀ F) (j : Fin k) (a b : V) : + (F j ⊓ exchangeGraph G F₀).Reachable a b ↔ (F₀ j ⊓ exchangeGraph G F₀).Reachable a b := by + induction hF with + | refl => rfl + | tail h hstep ih => exact (step_reachable_iff hF₀ hmax h hstep j a b).symm.trans ih + +end Core + +/-- **Core exchange lemma.** For every finite graph `G` there are `k` pairwise edge-disjoint +forests `F i ≤ G` and a subgraph `H ≤ G` such that each `F i ⊓ H` has the same connected +components as `H`, and every edge of `G` outside `H` belongs to some `F i`. -/ +theorem exists_forests_core [Finite V] (G : SimpleGraph V) (k : ℕ) : + ∃ (F : Fin k → SimpleGraph V) (H : SimpleGraph V), (∀ i, F i ≤ G ∧ (F i).IsAcyclic) ∧ + (Pairwise fun i j ↦ Disjoint (F i) (F j)) ∧ H ≤ G ∧ + (∀ i a b, H.Reachable a b → (F i ⊓ H).Reachable a b) ∧ + (∀ a b, G.Adj a b → ¬ H.Adj a b → ∃ i, (F i).Adj a b) := by + have : Finite (SimpleGraph V) := Finite.of_injective _ fun _ _ h ↦ SimpleGraph.ext h + have hval0 : ValidForests G (fun _ : Fin k ↦ (⊥ : SimpleGraph V)) := + ⟨fun _ ↦ ⟨bot_le, isAcyclic_bot⟩, fun _ _ _ ↦ disjoint_bot_left⟩ + obtain ⟨F₀, hF₀, hmax⟩ := Set.exists_max_image + {F : Fin k → SimpleGraph V | ValidForests G F} totalEdges (Set.toFinite _) ⟨_, hval0⟩ + refine ⟨F₀, exchangeGraph G F₀, hF₀.1, hF₀.2, fun a b h ↦ ?_, fun i a b hab ↦ ?_, + fun a b hab hH ↦ ?_⟩ + · obtain ⟨_, _, hu⟩ := exchangeGraph_adj.1 h + exact hu.1 + · refine reachable_map_of_adj id (fun c d h ↦ ?_) hab + obtain ⟨F, hF, hu⟩ := exchangeGraph_adj.1 h + exact (reach_reachable_iff hF₀ hmax hF i c d).1 (reach_uncovered_reachable hF₀ hmax hF hu i) + · by_contra h + exact hH (exchangeGraph_adj.2 ⟨F₀, .refl, hab, fun j hj ↦ h ⟨j, hj⟩⟩) + +end NashWilliamsTutte diff --git a/LeanPool/NashWilliamsTutte/Imports.lean b/LeanPool/NashWilliamsTutte/Imports.lean new file mode 100644 index 000000000..fe7f48d96 --- /dev/null +++ b/LeanPool/NashWilliamsTutte/Imports.lean @@ -0,0 +1,11 @@ +/- +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.NashWilliamsTutte +public import LeanPool.NashWilliamsTutte.Auxiliary +public import LeanPool.NashWilliamsTutte.Theorems diff --git a/LeanPool/NashWilliamsTutte/Theorems.lean b/LeanPool/NashWilliamsTutte/Theorems.lean new file mode 100644 index 000000000..b382fb893 --- /dev/null +++ b/LeanPool/NashWilliamsTutte/Theorems.lean @@ -0,0 +1,237 @@ +/- +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.Tactic.Push +public import LeanPool.NashWilliamsTutte.Auxiliary + +/-! +# The Nash-Williams–Tutte tree packing theorem and Nash-Williams' arboricity theorem + +For a finite simple graph `G` on `V`: + +* `NashWilliamsTutte.tree_packing`: **Nash-Williams (1961), Tutte (1961).** + `G` has `k` edge-disjoint spanning trees if and only if, for every partition of `V` into `m` + parts, at least `k (m - 1)` + edges of `G` join different parts. A partition is given by a map `f : V → V` (its parts are the + nonempty fibres, `#(univ.image f)` of them), and the edges of `G` joining different parts are + those of `G ⊓ (⊤ : SimpleGraph V).comap f`. +* `NashWilliamsTutte.arboricity`: **Nash-Williams (1964).** The edges of `G` can be covered by `k` + forests if and only if every nonempty vertex set `S` spans at most `k (#S - 1)` edges. +* `NashWilliamsTutte.exists_trees_of_isEdgeConnected`: **corollary.** A `2k`-edge-connected finite + graph (Mathlib's `SimpleGraph.IsEdgeConnected`) has `k` edge-disjoint spanning trees. + +Spanning trees are subgraphs `T ≤ G` on the same vertex type with Mathlib's `SimpleGraph.IsTree`; +forests are subgraphs with `SimpleGraph.IsAcyclic`; edge-disjointness is `Disjoint` in the lattice +of simple graphs. +-/ + +@[expose] public section + +open Finset Fintype SimpleGraph + +namespace NashWilliamsTutte + +/-- **Nash-Williams–Tutte tree packing theorem.** A finite graph on a nonempty vertex type has `k` +pairwise edge-disjoint spanning trees if and only if, for every map `f : V → V`, the number of +edges of `G` whose endpoints have different images under `f` is at least `k` times the number of +nonempty fibres of `f` minus one. -/ +theorem tree_packing {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) + (k : ℕ) : + (∃ T : Fin k → SimpleGraph V, (∀ i, T i ≤ G ∧ (T i).IsTree) ∧ + Pairwise fun i j ↦ Disjoint (T i) (T j)) ↔ + ∀ f : V → V, + k * (#(univ.image f) - 1) ≤ (G ⊓ (⊤ : SimpleGraph V).comap f).edgeSet.ncard := by + constructor + · rintro ⟨T, hT, hdisj⟩ f + have h1 : ∀ i, #(univ.image f) - 1 ≤ + ((T i).edgeSet ∩ ((⊤ : SimpleGraph V).comap f).edgeSet).ncard := fun i ↦ by + have := card_image_le_ncard_crossing_add_one (hT i).2.connected f + omega + have h2 := sum_ncard_le_of_pairwise_disjoint + (fun i ↦ (T i).edgeSet ∩ ((⊤ : SimpleGraph V).comap f).edgeSet) + (G ⊓ (⊤ : SimpleGraph V).comap f).edgeSet + (fun i ↦ by rw [edgeSet_inf]; exact Set.inter_subset_inter_left _ (edgeSet_mono (hT i).1)) + (fun i j hij ↦ (disjoint_edgeSet.2 (hdisj hij)).mono Set.inter_subset_left + Set.inter_subset_left) + calc k * (#(univ.image f) - 1) = ∑ _i : Fin k, (#(univ.image f) - 1) := by simp + _ ≤ ∑ i, ((T i).edgeSet ∩ ((⊤ : SimpleGraph V).comap f).edgeSet).ncard := + sum_le_sum fun i _ ↦ h1 i + _ ≤ _ := h2 + · intro hcond + obtain ⟨F, H, hF, hdisj, -, hreach, hcov⟩ := exists_forests_core G k + refine ⟨F, fun i ↦ ⟨(hF i).1, ?_⟩, hdisj⟩ + let f : V → V := fun v ↦ Quot.out (H.connectedComponentMk v) + have hfr : ∀ v, H.Reachable v (f v) := fun v ↦ + (ConnectedComponent.exact (Quot.out_eq (H.connectedComponentMk v))).symm + have hfeq : ∀ a b, H.Adj a b → f a = f b := fun a b hab ↦ by + simp only [f, ConnectedComponent.sound hab.reachable] + have hcf := hcond f + set m := #(univ.image f) + set C := (G ⊓ (⊤ : SimpleGraph V).comap f).edgeSet + have hC : C ⊆ ⋃ j, (F j).edgeSet ∩ C := by + intro e he + induction e using Sym2.ind with + | _ a b => + have he' : G.Adj a b ∧ f a ≠ f b := by simpa [C] using he + obtain ⟨j, hj⟩ := hcov a b he'.1 fun h ↦ he'.2 (hfeq a b h) + exact Set.mem_iUnion.2 ⟨j, hj, he⟩ + have hsum : C.ncard ≤ ∑ j, ((F j).edgeSet ∩ C).ncard := + (Set.ncard_le_ncard hC (Set.toFinite _)).trans (Set.ncard_iUnion_le_of_fintype _) + have hbound : ∀ j, ((F j).edgeSet ∩ C).ncard + Nat.card V ≤ + (F j).edgeSet.ncard + m := by + intro j + have hLB := card_le_ncard_edgeSet_add_card_image (F j ⊓ H) f + fun v ↦ hreach j _ _ (hfr v) + have hdj : Disjoint ((F j).edgeSet ∩ C) (F j ⊓ H).edgeSet := by + rw [Set.disjoint_left] + intro e he he' + induction e using Sym2.ind with + | _ a b => + have h1 : G.Adj a b ∧ f a ≠ f b := by simpa [C] using he.2 + exact h1.2 (hfeq a b he'.2) + have hsub : (F j).edgeSet ∩ C ∪ (F j ⊓ H).edgeSet ⊆ (F j).edgeSet := + Set.union_subset Set.inter_subset_left (edgeSet_mono inf_le_left) + have := Set.ncard_le_ncard hsub (Set.toFinite _) + rw [Set.ncard_union_eq hdj (Set.toFinite _) (Set.toFinite _)] at this + omega + by_contra hnt + have hlt : ∑ j, ((F j).edgeSet ∩ C).ncard < ∑ _j : Fin k, (m - 1) := by + refine Finset.sum_lt_sum (fun j _ ↦ ?_) ⟨i, mem_univ i, ?_⟩ + · have := (IsAcyclic.ncard_edgeSet_add_one_le (hF j).2).1 + have := hbound j + omega + · have h1 := IsAcyclic.ncard_edgeSet_add_one_le (hF i).2 + have h2 : ¬ Nat.card V ≤ (F i).edgeSet.ncard + 1 := fun h ↦ hnt (h1.2 h) + have := hbound i + omega + simp only [sum_const, card_univ, Fintype.card_fin, smul_eq_mul] at hlt + omega + +/-- **Nash-Williams' arboricity theorem.** The edges of a finite graph can be covered by `k` +forests if and only if every nonempty set `S` of vertices spans at most `k (#S - 1)` edges. -/ +theorem arboricity {V : Type*} [Finite V] (G : SimpleGraph V) (k : ℕ) : + (∃ F : Fin k → SimpleGraph V, (∀ i, F i ≤ G ∧ (F i).IsAcyclic) ∧ G = ⨆ i, F i) ↔ + ∀ S : Finset V, S.Nonempty → (G.induce (S : Set V)).edgeSet.ncard ≤ k * (#S - 1) := by + constructor + · rintro ⟨F, hF, hG⟩ S hS + have : Nonempty (S : Set V) := ⟨⟨hS.choose, hS.choose_spec⟩⟩ + have hcardS : Nat.card (S : Set V) = #S := by + rw [Nat.card_coe_set_eq, Set.ncard_coe_finset] + have hsub : (G.induce (S : Set V)).edgeSet ⊆ ⋃ i, ((F i).induce (S : Set V)).edgeSet := by + intro e he + induction e using Sym2.ind with + | _ a b => + have hab : G.Adj a b := he + rw [hG, iSup_adj] at hab + obtain ⟨i, hi⟩ := hab + exact Set.mem_iUnion.2 ⟨i, hi⟩ + calc (G.induce (S : Set V)).edgeSet.ncard + ≤ ∑ i, ((F i).induce (S : Set V)).edgeSet.ncard := + (Set.ncard_le_ncard hsub (Set.toFinite _)).trans (Set.ncard_iUnion_le_of_fintype _) + _ ≤ ∑ _i : Fin k, (#S - 1) := sum_le_sum fun i _ ↦ by + have := (IsAcyclic.ncard_edgeSet_add_one_le ((hF i).2.induce (S : Set V))).1 + omega + _ = k * (#S - 1) := by simp + · intro hcond + have := Fintype.ofFinite V + classical + obtain ⟨F, H, hF, hdisj, -, hreach, hcov⟩ := exists_forests_core G k + refine ⟨F, hF, le_antisymm (fun u v huv ↦ ?_) (iSup_le fun i ↦ (hF i).1)⟩ + rw [iSup_adj] + by_contra hnot + have hH : H.Adj u v := by + by_contra h + exact hnot (hcov u v huv h) + let S : Finset V := univ.filter fun w ↦ H.Reachable u w + have hu : u ∈ S := by simp [S] + have hv : v ∈ S := by simpa [S] using hH.reachable + have hcardS : Nat.card (S : Set V) = #S := by + rw [Nat.card_coe_set_eq, Set.ncard_coe_finset] + have hconn : ∀ i, ((F i ⊓ H).induce (S : Set V)).Connected := by + intro i + have hS : (S : Set V) = ((F i ⊓ H).connectedComponentMk u).supp := by + ext w + simp only [S, coe_filter, mem_univ, true_and, Set.mem_ofPred_eq, + ConnectedComponent.mem_supp_iff, ConnectedComponent.eq] + exact ⟨fun h ↦ (hreach i u w h).symm, fun h ↦ (h.mono inf_le_right).symm⟩ + rw [hS] + exact ((F i ⊓ H).connectedComponentMk u).connected_toSimpleGraph + let e : Sym2 (S : Set V) := s(⟨u, hu⟩, ⟨v, hv⟩) + have he : e ∈ (G.induce (S : Set V)).edgeSet := huv + have h1 := sum_ncard_le_of_pairwise_disjoint + (fun i ↦ ((F i ⊓ H).induce (S : Set V)).edgeSet) ((G.induce (S : Set V)).edgeSet \ {e}) + (fun i x hx ↦ by + induction x using Sym2.ind with + | _ a b => + have hab : (F i ⊓ H).Adj a b := hx + refine ⟨(hF i).1 hab.1, fun h ↦ ?_⟩ + rcases Sym2.eq_iff.1 (Set.mem_singleton_iff.1 h) with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ + · exact hnot ⟨i, hab.1⟩ + · exact hnot ⟨i, hab.1.symm⟩) + (fun i j hij ↦ by + rw [Function.onFun, disjoint_edgeSet, disjoint_iff_adj] + intro a b hi hj + exact disjoint_iff_adj.1 (hdisj hij) a b hi.1 hj.1) + have h2 := Set.ncard_sdiff_singleton_add_one he (Set.toFinite _) + have h3 := hcond S ⟨u, hu⟩ + have h4 : ∑ _i : Fin k, (#S - 1) ≤ ∑ i, ((F i ⊓ H).induce (S : Set V)).edgeSet.ncard := + sum_le_sum fun i _ ↦ by + have := (hconn i).card_vert_le_card_edgeSet_add_one + rw [Nat.card_coe_set_eq (((F i ⊓ H).induce (S : Set V)).edgeSet), hcardS] at this + omega + simp only [sum_const, card_univ, Fintype.card_fin, smul_eq_mul] at h4 + omega + +/-- **Corollary.** A finite `2k`-edge-connected graph on a nonempty vertex type has `k` pairwise +edge-disjoint spanning trees. -/ +theorem exists_trees_of_isEdgeConnected {V : Type*} [Finite V] [Nonempty V] + (G : SimpleGraph V) (k : ℕ) (hG : G.IsEdgeConnected (2 * k)) : + ∃ T : Fin k → SimpleGraph V, (∀ i, T i ≤ G ∧ (T i).IsTree) ∧ + Pairwise fun i j ↦ Disjoint (T i) (T j) := by + have := Fintype.ofFinite V + classical + refine (tree_packing G k).2 fun f ↦ ?_ + by_cases hm : #(univ.image f) ≤ 1 + · simp [Nat.sub_eq_zero_of_le hm] + push Not at hm + set K := G ⊓ (⊤ : SimpleGraph V).comap f + have hfib : ∀ r ∈ univ.image f, 2 * k ≤ #(univ.filter fun d : K.Dart ↦ f d.fst = r) := by + intro r hr + obtain ⟨x, -, hx⟩ := mem_image.1 hr + obtain ⟨r', hr', hr'r⟩ := exists_mem_ne hm r + obtain ⟨y, -, hy⟩ := mem_image.1 hr' + by_contra hlt + push Not at hlt + set s : Set (Sym2 V) := + ↑((univ.filter fun d : K.Dart ↦ f d.fst = r).image Dart.edge) + have hs : s.encard < (2 * k : ℕ) := by + rw [Set.encard_coe_eq_coe_finsetCard] + exact_mod_cast card_image_le.trans_lt hlt + have hreach := hG x y hs + have : f y = r := reachable_closed (fun w ↦ f w = r) (fun a b hab ha ↦ by + by_contra hb + rw [deleteEdges_adj] at hab + refine hab.2 ?_ + have hK : K.Adj a b := ⟨hab.1, by simp [ha, Ne.symm hb]⟩ + exact mem_image.2 ⟨⟨(a, b), hK⟩, by simp [ha], rfl⟩) hreach hx + exact hr'r (hy.symm.trans this) + have hdart : Fintype.card K.Dart = + ∑ r ∈ univ.image f, #(univ.filter fun d : K.Dart ↦ f d.fst = r) := + card_eq_sum_card_fiberwise fun d _ ↦ mem_image_of_mem _ (mem_univ _) + have hsum : ∑ _r ∈ univ.image f, 2 * k ≤ + ∑ r ∈ univ.image f, #(univ.filter fun d : K.Dart ↦ f d.fst = r) := + sum_le_sum hfib + have h2 := K.dart_card_eq_twice_card_edges + simp only [edgeFinset_card, Fintype.card_eq_nat_card, Nat.card_coe_set_eq] at h2 hdart + rw [h2] at hdart + rw [sum_const, smul_eq_mul, ← hdart] at hsum + have hcount : k * #(univ.image f) ≤ K.edgeSet.ncard := by + rw [Nat.mul_comm (#(univ.image f)) (2 * k), Nat.mul_assoc] at hsum + omega + exact (Nat.mul_le_mul_left _ (Nat.sub_le _ _)).trans hcount + +end NashWilliamsTutte diff --git a/LeanPool/projects/nash-williams-tutte.yaml b/LeanPool/projects/nash-williams-tutte.yaml new file mode 100644 index 000000000..e0d9498bb --- /dev/null +++ b/LeanPool/projects/nash-williams-tutte.yaml @@ -0,0 +1,50 @@ +slug: nash-williams-tutte +title: Nash-Williams–Tutte tree packing and arboricity +summary: A finite simple graph has k edge-disjoint spanning trees exactly when every + partition into m nonempty parts has at least k(m − 1) crossing edges. The development + also proves the Nash-Williams characterization of covering the edges by k forests, + and that every finite nonempty 2k-edge-connected simple graph has k edge-disjoint + spanning trees. It preserves the general forest exchange lemma and supporting + reachability and edge-counting infrastructure, using Mathlib's graph definitions. +branch: graph theory +entry_module: LeanPool.NashWilliamsTutte +authors: +- Juan Pablo Traverso Gianini +source: + title: Edge-disjoint spanning trees of finite graphs + doi: 10.1112/jlms/s1-36.1.445 + url: https://github.com/jtraverso/nash-williams-trees/tree/101e48847a929dd8102521f57723e2137989ce2e + github_repo: jtraverso/nash-williams-trees + commit: 101e48847a929dd8102521f57723e2137989ce2e + completion_url: https://github.com/jtraverso/nash-williams-trees/commit/5a5153dedcdfdc2eb9dc7e51f71abe0a6778830f + completion_date: '2026-10-17' +license: Apache-2.0 +status: verified +provenance: AI +main_declarations: +- NashWilliamsTutte.tree_packing +- NashWilliamsTutte.arboricity +main_results: +- declaration: NashWilliamsTutte.tree_packing + informal: A finite simple graph on a nonempty vertex type has k pairwise edge-disjoint + spanning trees if and only if every vertex partition into m nonempty parts has at + least k(m − 1) crossing edges. +- declaration: NashWilliamsTutte.arboricity + informal: A finite simple graph is the union of k forests if and only if every nonempty + finite vertex set S induces at most k(|S| − 1) edges. +- declaration: NashWilliamsTutte.exists_trees_of_isEdgeConnected + informal: Every finite simple graph on a nonempty vertex type that remains connected + after deletion of fewer than 2k edges has k pairwise edge-disjoint spanning trees. +- declaration: NashWilliamsTutte.exists_forests_core + informal: Every finite simple graph G contains k pairwise edge-disjoint forests and + a subgraph H such that intersecting each forest with H preserves the connected + components of H, and the forests cover every edge of G outside H. +tags: +- graph-theory +- tree-packing +- arboricity +- edge-connectivity +msc: +- 05C05 +- 05C70 +- 05C40 From 4ed45fab66e90ae3dab00b8a45cf7a59c7dd1e64 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sat, 17 Oct 2026 09:29:21 +0000 Subject: [PATCH 2/4] Polish imported theorem documentation --- LeanPool/NashWilliamsTutte.lean | 1 - LeanPool/NashWilliamsTutte/Auxiliary.lean | 4 ++-- LeanPool/NashWilliamsTutte/Theorems.lean | 4 ++-- 3 files changed, 4 insertions(+), 5 deletions(-) diff --git a/LeanPool/NashWilliamsTutte.lean b/LeanPool/NashWilliamsTutte.lean index cf23abe40..482aaf1d1 100644 --- a/LeanPool/NashWilliamsTutte.lean +++ b/LeanPool/NashWilliamsTutte.lean @@ -7,7 +7,6 @@ module public import LeanPool.NashWilliamsTutte.Theorems - /-! # Nash-Williams–Tutte tree packing and arboricity diff --git a/LeanPool/NashWilliamsTutte/Auxiliary.lean b/LeanPool/NashWilliamsTutte/Auxiliary.lean index 6a67d632a..371748c40 100644 --- a/LeanPool/NashWilliamsTutte/Auxiliary.lean +++ b/LeanPool/NashWilliamsTutte/Auxiliary.lean @@ -174,7 +174,7 @@ variable (G : SimpleGraph V) {k : ℕ} def ValidForests (F : Fin k → SimpleGraph V) : Prop := (∀ i, F i ≤ G ∧ (F i).IsAcyclic) ∧ Pairwise fun i j ↦ Disjoint (F i) (F j) -/-- The totalEdges number of edges of a family of graphs. -/ +/-- The total number of edges of a family of graphs. -/ noncomputable def totalEdges (F : Fin k → SimpleGraph V) : ℕ := ∑ i, (F i).edgeSet.ncard /-- `uv` is an edge of `G` not covered by the family `F`. -/ @@ -266,7 +266,7 @@ theorem ExchangeStep.total_eq [Finite V] {F F' : Fin k → SimpleGraph V} (h : E (Set.toFinite _) omega -/-- In a family with the maximum totalEdges number of edges, the endpoints of an uncovered edge are +/-- In a family with the maximum total number of edges, the endpoints of an uncovered edge are joined in every forest. -/ theorem reachable_of_uncovered [Finite V] {F : Fin k → SimpleGraph V} (hF : ValidForests G F) (hmax : ∀ F' : Fin k → SimpleGraph V, ValidForests G F' → totalEdges F' ≤ totalEdges F) diff --git a/LeanPool/NashWilliamsTutte/Theorems.lean b/LeanPool/NashWilliamsTutte/Theorems.lean index b382fb893..c3e76d897 100644 --- a/LeanPool/NashWilliamsTutte/Theorems.lean +++ b/LeanPool/NashWilliamsTutte/Theorems.lean @@ -15,8 +15,8 @@ For a finite simple graph `G` on `V`: * `NashWilliamsTutte.tree_packing`: **Nash-Williams (1961), Tutte (1961).** `G` has `k` edge-disjoint spanning trees if and only if, for every partition of `V` into `m` - parts, at least `k (m - 1)` - edges of `G` join different parts. A partition is given by a map `f : V → V` (its parts are the + parts, at least `k (m - 1)` edges of `G` join different parts. A partition is given by a map + `f : V → V` (its parts are the nonempty fibres, `#(univ.image f)` of them), and the edges of `G` joining different parts are those of `G ⊓ (⊤ : SimpleGraph V).comap f`. * `NashWilliamsTutte.arboricity`: **Nash-Williams (1964).** The edges of `G` can be covered by `k` From 882dec7b0b583f6e236eafff68918a281528a69a Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sat, 17 Oct 2026 09:30:43 +0000 Subject: [PATCH 3/4] Disclose nonempty vertices in the tree-packing summary --- LeanPool/projects/nash-williams-tutte.yaml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/LeanPool/projects/nash-williams-tutte.yaml b/LeanPool/projects/nash-williams-tutte.yaml index e0d9498bb..f9b95f70d 100644 --- a/LeanPool/projects/nash-williams-tutte.yaml +++ b/LeanPool/projects/nash-williams-tutte.yaml @@ -1,7 +1,8 @@ slug: nash-williams-tutte title: Nash-Williams–Tutte tree packing and arboricity -summary: A finite simple graph has k edge-disjoint spanning trees exactly when every - partition into m nonempty parts has at least k(m − 1) crossing edges. The development +summary: A finite simple graph on a nonempty vertex type has k edge-disjoint spanning + trees exactly when every partition into m nonempty parts has at least k(m − 1) crossing + edges. The development also proves the Nash-Williams characterization of covering the edges by k forests, and that every finite nonempty 2k-edge-connected simple graph has k edge-disjoint spanning trees. It preserves the general forest exchange lemma and supporting From e7a7cdd3f76bb2fa747cdccccdc6bf0219292f4b Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sat, 17 Oct 2026 02:40:45 -0700 Subject: [PATCH 4/4] Clarify Diestel citation as theorem background --- LeanPool/NashWilliamsTutte.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LeanPool/NashWilliamsTutte.lean b/LeanPool/NashWilliamsTutte.lean index 482aaf1d1..640702b43 100644 --- a/LeanPool/NashWilliamsTutte.lean +++ b/LeanPool/NashWilliamsTutte.lean @@ -29,6 +29,6 @@ prepared by Juan Pablo Traverso Gianini with Claude Code. These are the finite simple-graph versions of the tree-packing theorem of Nash-Williams (1961), doi:10.1112/jlms/s1-36.1.445, and Tutte (1961), doi:10.1112/jlms/s1-36.1.221, and the arboricity theorem of Nash-Williams (1964), -doi:10.1112/jlms/s1-39.1.12. The upstream proof plan follows Diestel, +doi:10.1112/jlms/s1-39.1.12. For background on these statements, see Diestel, *Graph Theory*, fifth edition, Section 2.4, doi:10.1007/978-3-662-53622-3. -/