Menger's theorem for vertex-disjoint directed paths between vertex sets

Let Q be an arrow family on a finite vertex type V, let A and B be sets of vertices, and let c v : ℕ be a capacity on every vertex. An A–B path is a directed path from a vertex a ∈ A to a vertex b ∈ B whose vertices other than a and b lie in neither A nor B. A packing of A–B paths is a finite indexed family of them, repetitions allowed, in which every vertex v, endpoints included, lies on at most c v members. A separator is a set X of vertices meeting every walk from a vertex of A to a vertex of B; it may meet A and B, and its weight is ∑ v ∈ X, c v.

This file proves the vertex-capacitated set-to-set form of Menger's theorem: some packing has as many members as some separator has weight, and every packing has at most as many members as every separator has weight. A vertex of A ∩ B is a path of length zero, which may be repeated up to its capacity, and it lies in every separator. The sets A and B may be empty or overlap, and the arrow types need not be finite. For c = 1 the members of a packing are pairwise vertex-disjoint, which gives the set-to-set form of Menger's theorem for vertex-disjoint paths, also in predicate form: after deleting any fewer than k vertices some vertex of B stays reachable from some vertex of A exactly when there are k pairwise vertex-disjoint A–B paths.

Main results

• TauCeti.card_le_sum_of_forall_not_reachableAvoiding: weak duality, a family of walks from vertices of A to vertices of B in which every vertex v lies on at most c v members has at most as many members as the weight of any separator.
• TauCeti.exists_paths_setSeparator_sum_eq: vertex-capacitated set-to-set Menger, a packing of A–B paths and a separator of equal size and weight.
• TauCeti.card_le_card_of_forall_not_reachableAvoiding: weak duality for families of pairwise vertex-disjoint walks.
• TauCeti.exists_paths_setSeparator_card_eq: Menger's theorem for vertex-disjoint directed paths between two vertex sets, in witness form.
• TauCeti.forall_exists_reachableAvoiding_iff_exists_paths: its predicate form.

Implementation notes

Both directions reduce to the vertex-capacitated Menger theorem between two vertices (TauCeti.exists_paths_vertexSeparator_sum_eq and TauCeti.card_le_sum_of_not_reachableAvoiding) for the arrow family TauCeti.AuxTerminalHom Q A B, which adds a fresh source σ with an arrow to every vertex of A and a fresh sink τ with an arrow from every vertex of B; the original vertices keep their capacities. Walks from A to B lift to σ–τ walks through the same original vertices, and every σ–τ walk projects to a walk from A to B (TauCeti.reachableAvoiding_auxTerminalHom_iff). Each σ–τ path of a packing is then trimmed to an A–B path (TauCeti.ArrowWalk.exists_isPath_interior_notMem), which visits no new vertex.

References

• K. Menger, Zur allgemeinen Kurventheorie, Fund. Math. 10 (1927).
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003, Section 9.1.

Vertex-capacitated packings

theorem TauCeti.card_le_sum_of_forall_not_reachableAvoiding {V : Type u} {Q : V → V → Type v} [DecidableEq V] {A B : Finset 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) {c : V → ℕ} (hP : ∀ (v : V), {i : ι | v ∈ (P i).vertices}.card ≤ c v) {X : Finset V} (hX : ∀ a ∈ A, ∀ b ∈ B, ¬ReachableAvoiding Q (↑X) a b) : Fintype.card ι ≤ ∑ v ∈ X, c v

Weak duality for vertex-capacitated set-to-set packings. A family of walks, each from a vertex of A to a vertex of B, in which every vertex v lies on at most c v members, has at most ∑ v ∈ X, c v members, for every set X of vertices meeting every walk from a vertex of A to a vertex of B.

theorem TauCeti.exists_paths_setSeparator_sum_eq {V : Type u} {Q : V → V → Type v} [Finite V] [DecidableEq V] (c : V → ℕ) (A B : Finset V) : ∃ (k : ℕ) (a : Fin k → V) (b : Fin k → V) (P : (i : Fin k) → ArrowWalk Q (a i) (b i)) (X : Finset V), (∀ (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) ∧ (∀ (v : V), {i : Fin k | v ∈ (P i).vertices}.card ≤ c v) ∧ (∀ a ∈ A, ∀ b ∈ B, ¬ReachableAvoiding Q (↑X) a b) ∧ ∑ v ∈ X, c v = k

Vertex-capacitated Menger's theorem for directed paths between vertex sets. Let A and B be sets of vertices of an arrow family on a finite vertex type, and let c v be a capacity on every vertex. 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, in which every vertex v lies on at most c v members, and some set X of vertices meeting every walk from a vertex of A to a vertex of B satisfy ∑ v ∈ X, c v = k. By TauCeti.card_le_sum_of_forall_not_reachableAvoiding, the family is then largest and the separator of least weight.

Vertex-disjoint paths

theorem TauCeti.card_le_card_of_forall_not_reachableAvoiding {V : Type u} {Q : V → V → Type v} {A B : Finset 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).vertices.Disjoint (P j).vertices) {X : Finset V} (hX : ∀ a ∈ A, ∀ b ∈ B, ¬ReachableAvoiding Q (↑X) a b) : Fintype.card ι ≤ X.card

Weak duality for vertex-disjoint set-to-set walks. A family of pairwise vertex-disjoint walks, each from a vertex of A to a vertex of B, has at most #X members, for every set X of vertices meeting every walk from a vertex of A to a vertex of B.

theorem TauCeti.exists_paths_setSeparator_card_eq {V : Type u} {Q : V → V → Type v} [Finite V] (A B : Finset V) : ∃ (k : ℕ) (a : Fin k → V) (b : Fin k → V) (P : (i : Fin k) → ArrowWalk Q (a i) (b i)) (X : Finset V), (∀ (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).vertices.Disjoint (P j).vertices) ∧ (∀ a ∈ A, ∀ b ∈ B, ¬ReachableAvoiding Q (↑X) a b) ∧ X.card = k

Menger's theorem for vertex-disjoint directed paths between vertex sets. Let A and B be sets of vertices of an arrow family on a finite vertex type. Some family of k pairwise vertex-disjoint directed paths, the i-th from a i ∈ A to b i ∈ B with its other vertices in neither A nor B, and some set of k vertices meeting every walk from a vertex of A to a vertex of B exist. By TauCeti.card_le_card_of_forall_not_reachableAvoiding, the family is then largest and the separator smallest.

theorem TauCeti.forall_exists_reachableAvoiding_iff_exists_paths {V : Type u} {Q : V → V → Type v} [Finite V] (A B : Finset V) (k : ℕ) : (∀ (X : Finset V), X.card < k → ∃ a ∈ A, ∃ b ∈ B, ReachableAvoiding Q (↑X) 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).vertices.Disjoint (P j).vertices

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