Menger's theorem for arrow-disjoint directed paths

Let Q be an arrow family on a vertex type V, and let s ≠ t. A family of directed s–t paths is arrow-disjoint when no arrow identity is traversed by two of its members; parallel arrows are distinct arrows. A set F of arrows separates t from s when every walk from s to t traverses an arrow of F, that is, when t is not reachable from s without the arrows of F.

This file proves the local edge form of Menger's theorem for directed networks with finitely many vertices and arrows: the largest number of arrow-disjoint s–t paths equals the least number of arrows separating t from s. Weak duality, that every arrow-disjoint family of s–t walks has at most as many members as every separating set of arrows, needs no finiteness at all: each member traverses an arrow of the separating set, and different members traverse different arrows.

It also proves the set-to-set form for disjoint vertex sets A and B. An A–B path runs from a vertex of A to a vertex of B and has no other vertex in A or B; arrow-disjoint A–B paths may share their endpoints. A set of arrows separates B from A when after deleting it no vertex of B is reachable from a vertex of A. The largest number of arrow-disjoint A–B paths equals the least number of arrows separating B from A; weak duality again needs neither finiteness nor disjointness.

Attainment is reduced to the max-flow/min-cut theorem over ℤ with capacity one on every arrow, between the terminals s and t or between the vertex sets A and B (TauCeti.SetFlow.exists_val_eq_arrowSum). A maximum flow has the value of a cut S, which is the number of arrows leaving S; those arrows separate the sink side from the source side. A path–cycle decomposition of the flow has paths from supply to demand vertices whose weights add up to the value. Every arrow carries at most one unit, so every path has weight one and no two paths share an arrow (TauCeti.PathCycleDecomposition.pairwise_disjoint_arrows). In the set-to-set case each path is finally trimmed to an A–B path, which traverses only arrows of the original path (TauCeti.ArrowWalk.exists_isPath_interior_notMem).

Main results

• TauCeti.natCard_sub_one_le_card_of_completeCut: a finite set of arrows containing every arrow across a nontrivial complete directed cut has at least one fewer member than the number of vertices.
• TauCeti.card_le_card_of_not_reachableWithout: weak duality, an arrow-disjoint family of s–t walks has at most as many members as any set of arrows separating t from s.
• TauCeti.exists_paths_arrowSeparator_card_eq: Menger's theorem for arrow-disjoint directed paths, in witness form: there are a family of arrow-disjoint s–t paths and a set of arrows separating t from s of the same size.
• TauCeti.forall_reachableWithout_iff_exists_paths: the predicate form, t stays reachable from s after deleting any fewer than k arrows exactly when there are k arrow-disjoint s–t paths.
• TauCeti.SetFlow.exists_paths_card_eq_val: an integer A–B flow carrying at most one unit on every arrow carries as many arrow-disjoint paths from A to B as its value.
• TauCeti.card_le_card_of_forall_not_reachableWithout: weak duality for arrow-disjoint walks from A to B and sets of arrows separating B from A.
• TauCeti.exists_paths_setArrowSeparator_card_eq: Menger's theorem for arrow-disjoint directed paths between disjoint vertex sets, in witness form.
• TauCeti.forall_exists_reachableWithout_iff_exists_paths: its predicate form.

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, Section 9.1.

theorem TauCeti.natCard_sub_one_le_card_of_completeCut {V : Type u} {Q : V → V → Type v} {s t : V} [Finite V] {C : Set V} (hs : s ∈ C) (ht : t ∉ C) (hC : ∀ u ∈ C, ∀ w ∉ C, Nonempty (Q u w)) {F : Finset ((x : V) × (y : V) × Q x y)} (hF : ∀ ⦃v w : V⦄ (e : Q v w), v ∈ C → w ∉ C → ⟨v, ⟨w, e⟩⟩ ∈ F) : Nat.card V - 1 ≤ F.card

If every vertex of C has an arrow to every vertex outside C, then any finite set containing all arrows leaving C has at least Nat.card V - 1 members, provided C and its complement are nonempty.

theorem TauCeti.card_le_card_of_forall_not_reachableWithout {V : Type u} {Q : V → V → Type v} {A B : Set V} {ι : Type u_1} [Fintype ι] {a b : ι → V} {P : (i : ι) → ArrowWalk Q (a i) (b i)} (ha : ∀ (i : ι), a i ∈ A) (hb : ∀ (i : ι), b i ∈ B) (hP : Pairwise fun (i j : ι) => (P i).arrows.Disjoint (P j).arrows) {F : Finset ((x : V) × (y : V) × Q x y)} (hF : ∀ a ∈ A, ∀ b ∈ B, ¬ReachableWithout (↑F) a b) : Fintype.card ι ≤ F.card

Weak duality for arrow-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 arrow, has at most as many members as any set of arrows whose deletion leaves no vertex of B reachable from a vertex of A.

theorem TauCeti.card_le_card_of_not_reachableWithout {V : Type u} {Q : V → V → Type v} {s t : V} {ι : Type u_1} [Fintype ι] {P : ι → ArrowWalk Q s t} (hP : Pairwise fun (i j : ι) => (P i).arrows.Disjoint (P j).arrows) {F : Finset ((x : V) × (y : V) × Q x y)} (hF : ¬ReachableWithout (↑F) s t) : Fintype.card ι ≤ F.card

Weak duality for arrow-disjoint walks. A family of s–t walks of which no two traverse a common arrow has at most as many members as any set of arrows whose deletion leaves t unreachable from s.

theorem TauCeti.TerminalCut.IsAdmissible.not_reachableWithout_of_cut_subset {V : Type u} {Q : V → V → Type v} {A B S : Finset V} (hS : IsAdmissible A B S) {F : Set ((x : V) × (y : V) × Q x y)} (hF : ∀ ⦃v w : V⦄ (e : Q v w), v ∈ S → w ∉ S → ⟨v, ⟨w, e⟩⟩ ∈ F) (a : V) (ha : a ∈ A) (b : V) (hb : b ∈ B) : ¬ReachableWithout F a b

Any arrow set containing all arrows leaving an admissible terminal cut separates its sink terminals from its source terminals.

theorem TauCeti.exists_paths_arrowSeparator_card_eq {V : Type u} {Q : V → V → Type v} {s t : V} [Finite V] [∀ (x y : V), Finite (Q x y)] (hst : s ≠ t) : ∃ (k : ℕ) (P : Fin k → ArrowWalk Q s t) (F : Finset ((x : V) × (y : V) × Q x y)), (∀ (i : Fin k), (P i).IsPath) ∧ (Pairwise fun (i j : Fin k) => (P i).arrows.Disjoint (P j).arrows) ∧ ¬ReachableWithout (↑F) s t ∧ F.card = k

Menger's theorem for arrow-disjoint directed paths. For distinct vertices s and t of a finite arrow family, some family of directed s–t paths, no two of which traverse a common arrow, has as many members as some set of arrows whose deletion leaves t unreachable from s. By TauCeti.card_le_card_of_not_reachableWithout, the family is then largest and the set of arrows smallest.

theorem TauCeti.forall_reachableWithout_iff_exists_paths {V : Type u} {Q : V → V → Type v} {s t : V} [Finite V] [∀ (x y : V), Finite (Q x y)] (k : ℕ) : (∀ (F : Finset ((x : V) × (y : V) × Q x y)), F.card < k → ReachableWithout (↑F) s t) ↔ ∃ (P : Fin k → ArrowWalk Q s t), (∀ (i : Fin k), (P i).IsPath) ∧ Pairwise fun (i j : Fin k) => (P i).arrows.Disjoint (P j).arrows

Menger's theorem for arrow-disjoint directed paths, predicate form. For vertices s and t of a finite arrow family, t stays reachable from s after deleting any fewer than k arrows exactly when there are k directed s–t paths, no two of which traverse a common arrow.

Arrow-disjoint paths between vertex sets

theorem TauCeti.SetFlow.exists_paths_card_eq_val {V : Type u} {Q : V → V → Type v} [Fintype V] [(x y : V) → Fintype (Q x y)] {cap : Assignment Q ℤ} {A B : Finset V} (f : SetFlow cap A B) (hf : ∀ ⦃x y : V⦄ (e : Q x y), f.toFun e ≤ 1) : ∃ (k : ℕ) (a : Fin k → V) (b : Fin k → V) (P : (i : Fin k) → ArrowWalk Q (a i) (b i)), ↑k = f.val ∧ (∀ (i : Fin k), a i ∈ A) ∧ (∀ (i : Fin k), b i ∈ B) ∧ (∀ (i : Fin k), (P i).IsPath) ∧ (∀ (i : Fin k), ∀ v ∈ (P i).vertices, v ≠ a i → v ≠ b i → v ∉ A ∧ v ∉ B) ∧ (∀ (i : Fin k), ∀ e ∈ (P i).arrows, f.toFun e.snd.snd = 1) ∧ Pairwise fun (i j : Fin k) => (P i).arrows.Disjoint (P j).arrows

An integer A–B flow carrying at most one unit on every arrow carries as many directed paths as its value, each from a vertex of A to a vertex of B, with no internal vertex in either terminal set and no arrow shared by two paths. Every arrow of an extracted path carries exactly one unit of the flow.

theorem TauCeti.exists_paths_setArrowSeparator_card_eq {V : Type u} {Q : V → V → Type v} [Finite V] [∀ (x y : V), Finite (Q x y)] {A B : Finset V} (hAB : Disjoint A B) : ∃ (k : ℕ) (a : Fin k → V) (b : Fin k → V) (P : (i : Fin k) → ArrowWalk Q (a i) (b i)) (F : Finset ((x : V) × (y : V) × Q x y)), (∀ (i : Fin k), a i ∈ A) ∧ (∀ (i : Fin k), b i ∈ B) ∧ (∀ (i : Fin k), (P i).IsPath) ∧ (∀ (i : Fin k), ∀ v ∈ (P i).vertices, v ≠ a i → v ≠ b i → v ∉ A ∧ v ∉ B) ∧ (Pairwise fun (i j : Fin k) => (P i).arrows.Disjoint (P j).arrows) ∧ (∀ a ∈ A, ∀ b ∈ B, ¬ReachableWithout (↑F) a b) ∧ F.card = k

Menger's theorem for arrow-disjoint directed paths between vertex sets. Let A and B be disjoint sets of vertices of a finite arrow family. Some family of k directed paths, the i-th from a i ∈ A to b i ∈ B with its other vertices in neither A nor B, no two of which traverse a common arrow, and some set of k arrows whose deletion leaves no vertex of B reachable from a vertex of A exist. By TauCeti.card_le_card_of_forall_not_reachableWithout, the family is then largest and the set of arrows smallest.

theorem TauCeti.forall_exists_reachableWithout_iff_exists_paths {V : Type u} {Q : V → V → Type v} [Finite V] [∀ (x y : V), Finite (Q x y)] {A B : Finset V} (k : ℕ) : (∀ (F : Finset ((x : V) × (y : V) × Q x y)), F.card < k → ∃ a ∈ A, ∃ b ∈ B, ReachableWithout (↑F) a b) ↔ ∃ (a : Fin k → V) (b : Fin k → V) (P : (i : Fin k) → ArrowWalk Q (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).vertices, v ≠ a i → v ≠ b i → v ∉ A ∧ v ∉ B) ∧ Pairwise fun (i j : Fin k) => (P i).arrows.Disjoint (P j).arrows

Menger's theorem for arrow-disjoint directed paths between vertex sets, predicate form. Let A and B be sets of vertices of a finite arrow family. After deleting any fewer than k arrows, some vertex of B stays reachable from some vertex of A exactly when there are k directed paths, each from a vertex of A to a vertex of B with its other vertices in neither A nor B, no two of which traverse a common arrow.