Menger's theorem for vertex-disjoint directed paths

Let Q be an arrow family on a finite vertex type V, let s ≠ t be vertices with no arrow from s to t, and let c v : ℕ be a capacity on every vertex. A packing of s–t paths is a finite indexed family of directed s–t paths, repetitions allowed, in which every vertex v other than s and t lies on at most c v members. A vertex separator is a set X of vertices, avoiding s and t, whose deletion leaves t unreachable from s; its weight is ∑ v ∈ X, c v.

This file proves the vertex-capacitated form of Menger's theorem: some packing has as many members as some vertex separator has weight, and every packing has at most as many members as every vertex separator has weight. For c = 1 the members of a packing are distinct and internally vertex-disjoint, which gives the local vertex form of Menger's theorem, also in predicate form: t stays reachable from s after deleting any fewer than k vertices other than s and t exactly when there are k internally vertex-disjoint s–t paths; the predicate form needs neither s ≠ t nor the absence of an arrow from s to t. Without the hypothesis that no arrow runs from s to t, no vertex separator exists, and with c = 1 a direct arrow could be repeated arbitrarily often in a packing.

The arrow types need not be finite, since the statements concern only the vertices visited by walks.

Main results

• TauCeti.card_le_sum_of_not_reachableAvoiding: weak duality, a family of s–t walks in which every vertex v other than s and t lies on at most c v members has at most as many members as the weight of any vertex separator.
• TauCeti.exists_paths_vertexSeparator_sum_eq: vertex-capacitated Menger, a packing and a vertex separator of equal size and weight.
• TauCeti.card_le_card_of_not_reachableAvoiding: weak duality for families of walks pairwise sharing no vertex other than s and t.
• TauCeti.exists_paths_vertexSeparator_card_eq: Menger's theorem for internally vertex-disjoint directed paths, in witness form.
• TauCeti.forall_reachableAvoiding_iff_exists_paths: its predicate form.

Implementation notes

Weak duality is counting: each member of a packing visits a vertex of the separator, and the separator vertex v is visited by at most c v members. Attainment is reduced to the max-flow/min-cut theorem for mixed vertex and arrow capacities over ℤ (TauCeti.Flow.exists_respectsVertexCapacity_val_eq), with capacity M = ∑ v, c v + 1 on every arrow. The vertices other than s and t form a separator of weight below M, so a minimum mixed separator contains no arrows and is a vertex separator. A maximum flow carries a packing with as many members as its value (TauCeti.Flow.exists_paths_card_eq_val_card_filter_le). For arrow types that may be infinite, the arrow family is first replaced by the family with one arrow from v to w whenever Q v w is inhabited, which has walks with the same vertex sequences.

References

• K. Menger, Zur allgemeinen Kurventheorie, Fund. Math. 10 (1927).
• L. R. Ford, D. R. Fulkerson, Flows in Networks, Princeton University Press, 1962.
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003, Section 9.1.

Weak duality

theorem TauCeti.card_le_sum_of_not_reachableAvoiding {V : Type u} {Q : V → V → Type v} {s t : V} [DecidableEq V] {ι : Type u_1} [Fintype ι] {P : ι → ArrowWalk Q s t} {c : V → ℕ} (hP : ∀ (v : V), v ≠ s → v ≠ t → {i : ι | v ∈ (P i).vertices}.card ≤ c v) {X : Finset V} (hs : s ∉ X) (ht : t ∉ X) (hX : ¬ReachableAvoiding Q (↑X) s t) : Fintype.card ι ≤ ∑ v ∈ X, c v

Weak duality for vertex-capacitated packings. A family of s–t walks in which every vertex v other than s and t lies on at most c v members has at most ∑ v ∈ X, c v members, for every set X of vertices avoiding s and t whose deletion leaves t unreachable from s.

Vertex-capacitated Menger

theorem TauCeti.exists_paths_vertexSeparator_sum_eq {V : Type u} {Q : V → V → Type v} {s t : V} [Finite V] [DecidableEq V] (c : V → ℕ) (hst : s ≠ t) (hadj : IsEmpty (Q s t)) : ∃ (k : ℕ) (P : Fin k → ArrowWalk Q s t) (X : Finset V), (∀ (i : Fin k), (P i).IsPath) ∧ (∀ (v : V), v ≠ s → v ≠ t → {i : Fin k | v ∈ (P i).vertices}.card ≤ c v) ∧ s ∉ X ∧ t ∉ X ∧ ¬ReachableAvoiding Q (↑X) s t ∧ ∑ v ∈ X, c v = k

Vertex-capacitated Menger's theorem for directed paths. Let s ≠ t be vertices of an arrow family on a finite vertex type, with no arrow from s to t, and let c v be a capacity on every vertex. Some family of k directed s–t paths, in which every vertex v other than s and t lies on at most c v members, and some set X of vertices avoiding s and t, whose deletion leaves t unreachable from s, satisfy ∑ v ∈ X, c v = k. By TauCeti.card_le_sum_of_not_reachableAvoiding, the family is then largest and the separator of least weight.

Internally vertex-disjoint paths

theorem TauCeti.card_le_card_of_not_reachableAvoiding {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).InternallyDisjoint (P j)) {X : Finset V} (hs : s ∉ X) (ht : t ∉ X) (hX : ¬ReachableAvoiding Q (↑X) s t) : Fintype.card ι ≤ X.card

Weak duality for internally vertex-disjoint walks. A family of s–t walks whose members pairwise share no vertex other than s and t has at most #X members, for every set X of vertices avoiding s and t whose deletion leaves t unreachable from s.

theorem TauCeti.exists_paths_vertexSeparator_card_eq {V : Type u} {Q : V → V → Type v} {s t : V} [Finite V] (hst : s ≠ t) (hadj : IsEmpty (Q s t)) : ∃ (k : ℕ) (P : Fin k → ArrowWalk Q s t) (X : Finset V), Function.Injective P ∧ (∀ (i : Fin k), (P i).IsPath) ∧ (Pairwise fun (i j : Fin k) => (P i).InternallyDisjoint (P j)) ∧ s ∉ X ∧ t ∉ X ∧ ¬ReachableAvoiding Q (↑X) s t ∧ X.card = k

Menger's theorem for internally vertex-disjoint directed paths. Let s ≠ t be vertices of an arrow family on a finite vertex type, with no arrow from s to t. Some family of k distinct directed s–t paths, pairwise sharing no vertex other than s and t, and some set of k vertices avoiding s and t, whose deletion leaves t unreachable from s, exist. By TauCeti.card_le_card_of_not_reachableAvoiding, the family is then largest and the separator smallest.

theorem TauCeti.forall_reachableAvoiding_iff_exists_paths {V : Type u} {Q : V → V → Type v} {s t : V} [Finite V] (k : ℕ) : (∀ (X : Finset V), s ∉ X → t ∉ X → X.card < k → ReachableAvoiding Q (↑X) s t) ↔ ∃ (P : Fin k → ArrowWalk Q s t), (∀ (i : Fin k), (P i).IsPath) ∧ Pairwise fun (i j : Fin k) => (P i).InternallyDisjoint (P j)

Menger's theorem for internally vertex-disjoint directed paths, predicate form. Let s and t be vertices of an arrow family on a finite vertex type. Then t stays reachable from s after deleting any fewer than k vertices other than s and t exactly when there are k directed s–t paths pairwise sharing no vertex other than s and t. For s = t, and when there is an arrow from s to t, both sides hold, the paths being the trivial walk or k copies of the one-arrow path.