Menger's theorem for edge-disjoint paths in multigraphs

Let G : Graph α β be a multigraph and let s ≠ t. Two walks of G are edge-disjoint when no edge identity is traversed by both; distinct parallel edges are different edges, while a single edge cannot be shared even if the two walks traverse it in opposite directions. A set F of edges separates s from t when s and t are not reachable in G.deleteEdges F.

This file proves the local edge form of Menger's theorem for multigraphs with finitely many actual vertices and edges: the largest number of pairwise edge-disjoint s–t paths equals the least number of edges separating s from t. Weak duality, that every family of pairwise edge-disjoint s–t walks has at most as many members as every separating set of edges, needs no finiteness: each member traverses an edge of the separating set, and different members traverse different edges. The predicate form identifies k-edge-reachability (Graph.IsEdgeReachable) with the existence of k pairwise edge-disjoint s–t paths. Through Graph.ofSimpleGraph, the same statements hold for simple graphs, with Mathlib's SimpleGraph.IsEdgeReachable.

The set-to-set form allows disjoint terminal sets A and B. Its paths may share endpoints, but their internal vertices avoid both terminal sets. The largest number of pairwise edge-disjoint A–B paths equals the least number of edges whose deletion separates every vertex of B from every vertex of A. Set-to-set weak duality also needs no finiteness. Empty terminal sets are allowed.

Main results

• Graph.card_le_encard_of_not_reachable_deleteEdges: weak duality, a family of pairwise edge-disjoint s–t walks has at most as many members as any set of edges separating s from t.
• Graph.exists_paths_edgeSeparator_card_eq: Menger's theorem for edge-disjoint paths in a multigraph, in witness form: there are a family of pairwise edge-disjoint s–t paths and a set of actual edges separating s from t of the same size.
• Graph.isEdgeReachable_iff_exists_paths: the predicate form, s and t are k-edge-reachable exactly when there are k pairwise edge-disjoint s–t paths.
• Graph.card_le_encard_of_forall_not_reachable_deleteEdges: set-to-set weak duality.
• Graph.exists_paths_setEdgeSeparator_card_eq: the corresponding witness theorem between disjoint vertex sets.
• Graph.forall_exists_reachable_deleteEdges_iff_exists_paths: its predicate form.
• SimpleGraph.card_le_encard_of_not_reachable_deleteEdges, SimpleGraph.exists_paths_edgeSeparator_card_eq, SimpleGraph.isEdgeReachable_iff_exists_paths: the same statements for simple graphs.
• SimpleGraph.card_le_encard_of_forall_not_reachable_deleteEdges, SimpleGraph.exists_paths_setEdgeSeparator_card_eq, SimpleGraph.forall_exists_reachable_deleteEdges_iff_exists_paths: the set-to-set theorems for simple graphs.

Implementation notes

Attainment starts from TauCeti.SetFlow.exists_val_eq_arrowSum over ℤ on the bidirected arrow family Graph.BidirectedHom G, with capacity one on every arrow. A maximum set-to-set flow has the value of a cut S, the number of arrows leaving S. It is replaced by an acyclic flow of the same value using TauCeti.SetFlow.exists_isAcyclic, decomposed into arrow-disjoint unit paths, and trimmed so the path interiors avoid A ∪ B. Acyclicity prevents two paths from using opposite orientations of one edge. Each cut edge supplies exactly one arrow leaving S, so the cut arrows have distinct underlying edges; deleting those edges separates B from A. The local theorem is the singleton-terminal corollary.

References

• K. Menger, Zur allgemeinen Kurventheorie, Fund. Math. 10 (1927).
• L. R. Ford, D. R. Fulkerson, Maximal flow through a network, Canad. J. Math. 8 (1956).
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003, Sections 9.1 and 9.2.

Edge-disjoint paths between vertex sets

theorem Graph.card_le_encard_of_forall_not_reachable_deleteEdges {α : Type u} {β : Type v} {G : Graph α β} {A B : Set α} {ι : Type u_1} {a b : ι → α} {P : (i : ι) → G.Walk (a i) (b i)} (ha : ∀ (i : ι), a i ∈ A) (hb : ∀ (i : ι), b i ∈ B) (hstart : ∀ (i : ι), a i ∈ G.vertexSet) (hP : Pairwise fun (i j : ι) => (P i).edges.Disjoint (P j).edges) {F : Set β} (hF : ∀ a ∈ A, ∀ b ∈ B, ¬(G.deleteEdges F).Reachable a b) : ENat.card ι ≤ F.encard

Weak duality for edge-disjoint set-to-set walks. A family of walks, each from a vertex of A to a vertex of B, of which no two traverse a common edge has at most as many members as any set of edges whose deletion leaves no vertex of B reachable from a vertex of A. No finiteness assumption is needed, but every walk must start at an actual vertex.

theorem Graph.exists_paths_setEdgeSeparator_card_eq {α : Type u} {β : Type v} {G : Graph α β} [Finite ↑G.vertexSet] [Finite ↑G.edgeSet] {A B : Finset α} (hAB : Disjoint A B) : ∃ (k : ℕ) (a : Fin k → α) (b : Fin k → α) (P : (i : Fin k) → G.Walk (a i) (b i)) (F : Finset β), (∀ (i : Fin k), a i ∈ A) ∧ (∀ (i : Fin k), b i ∈ B) ∧ (∀ (i : Fin k), (P i).IsPath) ∧ (∀ (i : Fin k), ∀ v ∈ (P i).support, v ≠ a i → v ≠ b i → v ∉ A ∧ v ∉ B) ∧ (Pairwise fun (i j : Fin k) => (P i).edges.Disjoint (P j).edges) ∧ ↑F ⊆ G.edgeSet ∧ (∀ a ∈ A, ∀ b ∈ B, ¬(G.deleteEdges ↑F).Reachable a b) ∧ F.card = k

Menger's theorem for edge-disjoint paths between vertex sets in a multigraph. Let A and B be disjoint finite vertex sets of a multigraph with finitely many actual vertices and edges. Some family of pairwise edge-disjoint paths from A to B, with no internal vertex in either terminal set, has as many members as some set of actual edges whose deletion separates B from A. Shared endpoints are allowed.

Edge-disjoint paths between two vertices

theorem Graph.card_le_encard_of_not_reachable_deleteEdges {α : Type u} {β : Type v} {G : Graph α β} {s t : α} {ι : Type u_1} {P : ι → G.Walk s t} (hP : Pairwise fun (i j : ι) => (P i).edges.Disjoint (P j).edges) (hs : s ∈ G.vertexSet) {F : Set β} (hF : ¬(G.deleteEdges F).Reachable s t) : ENat.card ι ≤ F.encard

Weak duality for edge-disjoint walks. A family of s–t walks, from an actual vertex s, of which no two traverse a common edge has at most as many members as any set of edges whose deletion leaves s and t unreachable.

theorem Graph.exists_paths_edgeSeparator_card_eq {α : Type u} {β : Type v} {G : Graph α β} {s t : α} [Finite ↑G.vertexSet] [Finite ↑G.edgeSet] (hst : s ≠ t) : ∃ (k : ℕ) (P : Fin k → G.Walk s t) (F : Finset β), (∀ (i : Fin k), (P i).IsPath) ∧ (Pairwise fun (i j : Fin k) => (P i).edges.Disjoint (P j).edges) ∧ ↑F ⊆ G.edgeSet ∧ ¬(G.deleteEdges ↑F).Reachable s t ∧ F.card = k

Menger's theorem for edge-disjoint paths in a multigraph. For distinct points s and t of a multigraph with finitely many actual vertices and edges, some family of s–t paths, no two of which traverse a common edge, has as many members as some set of actual edges whose deletion leaves s and t unreachable. By Graph.card_le_encard_of_not_reachable_deleteEdges, the family is then largest and the set of edges smallest.

theorem Graph.isEdgeReachable_iff_exists_paths {α : Type u} {β : Type v} {G : Graph α β} {s t : α} [Finite ↑G.vertexSet] [Finite ↑G.edgeSet] (hs : s ∈ G.vertexSet) (k : ℕ) : G.IsEdgeReachable k s t ↔ ∃ (P : Fin k → G.Walk s t), (∀ (i : Fin k), (P i).IsPath) ∧ Pairwise fun (i j : Fin k) => (P i).edges.Disjoint (P j).edges

Menger's theorem for edge-disjoint paths in a multigraph, predicate form. For an actual vertex s of a multigraph with finitely many actual vertices and edges, s and t stay reachable after deleting any fewer than k edges exactly when there are k s–t paths, no two of which traverse a common edge.

theorem Graph.forall_exists_reachable_deleteEdges_iff_exists_paths {α : Type u} {β : Type v} {G : Graph α β} [Finite ↑G.vertexSet] [Finite ↑G.edgeSet] {A B : Finset α} (hAB : Disjoint A B) (k : ℕ) : (∀ (F : Finset β), F.card < k → ∃ a ∈ A, ∃ b ∈ B, (G.deleteEdges ↑F).Reachable a b) ↔ ∃ (a : Fin k → α) (b : Fin k → α) (P : (i : Fin k) → G.Walk (a i) (b i)), (∀ (i : Fin k), a i ∈ A) ∧ (∀ (i : Fin k), b i ∈ B) ∧ (∀ (i : Fin k), (P i).IsPath) ∧ (∀ (i : Fin k), ∀ v ∈ (P i).support, v ≠ a i → v ≠ b i → v ∉ A ∧ v ∉ B) ∧ Pairwise fun (i j : Fin k) => (P i).edges.Disjoint (P j).edges

Menger's theorem for edge-disjoint paths between vertex sets in a multigraph, predicate form. For disjoint finite sets A and B in a finite multigraph, deleting fewer than k edges always leaves some vertex of B reachable from some vertex of A exactly when there are k pairwise edge-disjoint A–B paths with no internal terminal vertex.

Simple graphs

theorem SimpleGraph.exists_paths_edgeSeparator_card_eq {α : Type u} {G : SimpleGraph α} {s t : α} [Finite α] (hst : s ≠ t) : ∃ (k : ℕ) (P : Fin k → G.Walk s t) (F : Finset (Sym2 α)), (∀ (i : Fin k), (P i).IsPath) ∧ (Pairwise fun (i j : Fin k) => (P i).edges.Disjoint (P j).edges) ∧ ↑F ⊆ G.edgeSet ∧ ¬(G.deleteEdges ↑F).Reachable s t ∧ F.card = k

Menger's theorem for edge-disjoint paths in a simple graph. For distinct vertices s and t of a finite simple graph, some family of s–t paths, no two of which traverse a common edge, has as many members as some set of edges of G whose deletion leaves s and t unreachable. By SimpleGraph.card_le_encard_of_not_reachable_deleteEdges, the family is then largest and the set of edges smallest.

theorem SimpleGraph.isEdgeReachable_iff_exists_paths {α : Type u} {G : SimpleGraph α} {s t : α} [Finite α] (k : ℕ) : G.IsEdgeReachable (↑k) s t ↔ ∃ (P : Fin k → G.Walk s t), (∀ (i : Fin k), (P i).IsPath) ∧ Pairwise fun (i j : Fin k) => (P i).edges.Disjoint (P j).edges

Menger's theorem for edge-disjoint paths in a simple graph, predicate form. In a finite simple graph, s and t stay reachable after deleting any fewer than k edges exactly when there are k s–t paths, no two of which traverse a common edge.

Edge-disjoint paths between vertex sets

theorem SimpleGraph.card_le_encard_of_forall_not_reachable_deleteEdges {α : Type u} {G : SimpleGraph α} {A B : Set α} {ι : Type u_1} {a b : ι → α} {P : (i : ι) → G.Walk (a i) (b i)} (ha : ∀ (i : ι), a i ∈ A) (hb : ∀ (i : ι), b i ∈ B) (hP : Pairwise fun (i j : ι) => (P i).edges.Disjoint (P j).edges) {F : Set (Sym2 α)} (hF : ∀ a ∈ A, ∀ b ∈ B, ¬(G.deleteEdges F).Reachable a b) : ENat.card ι ≤ F.encard

Weak duality for edge-disjoint set-to-set walks in a simple graph. A family of walks from A to B, of which no two traverse a common edge, has at most as many members as any set of edges whose deletion leaves no vertex of B reachable from a vertex of A.

theorem SimpleGraph.card_le_encard_of_not_reachable_deleteEdges {α : Type u} {G : SimpleGraph α} {s t : α} {ι : Type u_1} {P : ι → G.Walk s t} (hP : Pairwise fun (i j : ι) => (P i).edges.Disjoint (P j).edges) {F : Set (Sym2 α)} (hF : ¬(G.deleteEdges F).Reachable s t) : ENat.card ι ≤ F.encard

Weak duality for edge-disjoint walks in a simple graph. A family of s–t walks of which no two traverse a common edge has at most as many members as any set of edges whose deletion leaves s and t unreachable.

theorem SimpleGraph.exists_paths_setEdgeSeparator_card_eq {α : Type u} {G : SimpleGraph α} [Finite α] {A B : Finset α} (hAB : Disjoint A B) : ∃ (k : ℕ) (a : Fin k → α) (b : Fin k → α) (P : (i : Fin k) → G.Walk (a i) (b i)) (F : Finset (Sym2 α)), (∀ (i : Fin k), a i ∈ A) ∧ (∀ (i : Fin k), b i ∈ B) ∧ (∀ (i : Fin k), (P i).IsPath) ∧ (∀ (i : Fin k), ∀ v ∈ (P i).support, v ≠ a i → v ≠ b i → v ∉ A ∧ v ∉ B) ∧ (Pairwise fun (i j : Fin k) => (P i).edges.Disjoint (P j).edges) ∧ ↑F ⊆ G.edgeSet ∧ (∀ a ∈ A, ∀ b ∈ B, ¬(G.deleteEdges ↑F).Reachable a b) ∧ F.card = k

Menger's theorem for edge-disjoint paths between vertex sets in a simple graph. For disjoint finite vertex sets A and B in a finite simple graph, some family of pairwise edge-disjoint A–B paths with no internal terminal vertex and some separating edge set have the same cardinality. Shared endpoints are allowed.

theorem SimpleGraph.forall_exists_reachable_deleteEdges_iff_exists_paths {α : Type u} {G : SimpleGraph α} [Finite α] {A B : Finset α} (hAB : Disjoint A B) (k : ℕ) : (∀ (F : Finset (Sym2 α)), F.card < k → ∃ a ∈ A, ∃ b ∈ B, (G.deleteEdges ↑F).Reachable a b) ↔ ∃ (a : Fin k → α) (b : Fin k → α) (P : (i : Fin k) → G.Walk (a i) (b i)), (∀ (i : Fin k), a i ∈ A) ∧ (∀ (i : Fin k), b i ∈ B) ∧ (∀ (i : Fin k), (P i).IsPath) ∧ (∀ (i : Fin k), ∀ v ∈ (P i).support, v ≠ a i → v ≠ b i → v ∉ A ∧ v ∉ B) ∧ Pairwise fun (i j : Fin k) => (P i).edges.Disjoint (P j).edges

Menger's theorem for edge-disjoint paths between vertex sets in a simple graph, predicate form. For disjoint finite vertex sets A and B in a finite simple graph, deleting fewer than k edges always leaves an A–B connection exactly when there are k pairwise edge-disjoint A–B paths with no internal terminal vertex.