Flow-equivalent trees and cut trees

Let f be a set function on a finite vertex type, with minimum cut values λ(s, t) = pairMinimumValue f s t. A tree T on the same vertex type with edge weights w is flow-equivalent for f when, for any two distinct vertices, λ(s, t) is the minimum weight on the tree path from s to t. It is a cut tree (a Gomory–Hu tree) when moreover, for every tree edge s(u, v), the side of u left by deleting that edge is a minimum u–v cut.

This file develops what these properties give, independently of how such a tree is constructed:

• IsFlowEquivalentTree.reachable_deleteEdges_iff: the threshold partition. Deleting the tree edges of weight below k leaves s and t connected exactly when s = t or k ≤ λ(s, t).
• IsCutTree.isMinimum_edgeSide_of_mem_edges: the query theorem. A minimum-weight edge on the tree path from s to t yields a minimum s–t cut by deleting that edge.
• IsCutTree.apply_edgeSide_le: deleting a tree edge of minimum weight gives a side that minimizes f among all sets separating two vertices, with value that minimum weight.
• IsFlowEquivalentTree.card_image_pairMinimumValue_le: the minimum cut values between distinct vertices take at most |V| - 1 distinct values, since each is a tree-edge weight.
• IsCutTree.of_isMinimum_edgeSide: a tree whose edges all leave minimum cuts between their ends is a cut tree for the weights given by those minimum cut values.

Neither property assumes symmetry or submodularity of f. The results here take the tree as given; for symmetric submodular f, a cut tree always exists by the Gomory–Hu theorem TauCeti.TerminalCut.exists_isCutTree.

References

• R. E. Gomory and T. C. Hu, Multi-terminal network flows, J. SIAM 9 (1961), 551–570.
• D. Gusfield, Very Simple Methods for All Pairs Network Flow Analysis, SIAM J. Comput. 19 (1990), 143–155.
• B. Korte and J. Vygen, Combinatorial Optimization: Theory and Algorithms, Section 8.6.

structure TauCeti.TerminalCut.IsFlowEquivalentTree {V : Type u_1} {K : Type u_2} [Finite V] [Zero K] [LinearOrder K] (f : Finset V → K) (T : SimpleGraph V) (w : Sym2 V → K) : Prop

A tree T on the vertex type with edge weights w is flow-equivalent for f when the minimum cut value between any two distinct vertices is the minimum weight on the tree path between them. Only the weights of tree edges matter.

• isTree : T.IsTree

  The graph is a tree.

• le_weight ⦃s t : V⦄ ⦃p : T.Walk s t⦄ (hp : p.IsPath) ⦃e : Sym2 V⦄ (he : e ∈ p.edges) : pairMinimumValue f s t ≤ w e

  Every edge on a tree path weighs at least the minimum cut value between its ends.

• exists_weight_eq ⦃s t : V⦄ (hst : s ≠ t) ⦃p : T.Walk s t⦄ (hp : p.IsPath) : ∃ e ∈ p.edges, w e = pairMinimumValue f s t

  Some edge on a tree path between distinct vertices attains the minimum cut value.

theorem TauCeti.TerminalCut.IsFlowEquivalentTree.weight_eq {V : Type u_1} {K : Type u_2} [Finite V] [Zero K] [LinearOrder K] {f : Finset V → K} {T : SimpleGraph V} {w : Sym2 V → K} (hT : IsFlowEquivalentTree f T w) {u v : V} (huv : T.Adj u v) : w s(u, v) = pairMinimumValue f u v

The weight of a tree edge is the minimum cut value between its ends.

theorem TauCeti.TerminalCut.IsFlowEquivalentTree.reachable_deleteEdges_iff {V : Type u_1} {K : Type u_2} [Finite V] [Zero K] [LinearOrder K] {f : Finset V → K} {T : SimpleGraph V} {w : Sym2 V → K} (hT : IsFlowEquivalentTree f T w) (k : K) {s t : V} : (T.deleteEdges {e : Sym2 V | w e < k}).Reachable s t ↔ s = t ∨ k ≤ pairMinimumValue f s t

Threshold partition. Deleting the tree edges of weight below k leaves two vertices connected exactly when they are equal or their minimum cut value is at least k.

theorem TauCeti.TerminalCut.IsFlowEquivalentTree.exists_weight_le {V : Type u_1} {K : Type u_2} [Finite V] [Zero K] [LinearOrder K] {f : Finset V → K} {T : SimpleGraph V} {w : Sym2 V → K} (hT : IsFlowEquivalentTree f T w) {S : Finset V} {s t : V} (hs : s ∈ S) (ht : t ∉ S) : ∃ e ∈ T.edgeSet, w e ≤ f S

Any set separating two vertices has value at least the weight of some tree edge.

theorem TauCeti.TerminalCut.IsFlowEquivalentTree.card_image_pairMinimumValue_le {V : Type u_1} {K : Type u_2} [Finite V] [Zero K] [LinearOrder K] {f : Finset V → K} {T : SimpleGraph V} {w : Sym2 V → K} [Fintype V] [DecidableEq V] [DecidableEq K] (hT : IsFlowEquivalentTree f T w) : (Finset.image (fun (p : V × V) => pairMinimumValue f p.1 p.2) {p : V × V | p.1 ≠ p.2}).card ≤ Fintype.card V - 1

The minimum cut values between distinct vertices take at most |V| - 1 distinct values, since each is the weight of a tree edge.

structure TauCeti.TerminalCut.IsCutTree {V : Type u_1} {K : Type u_2} [Fintype V] [Zero K] [LinearOrder K] (f : Finset V → K) (T : SimpleGraph V) (w : Sym2 V → K) extends TauCeti.TerminalCut.IsFlowEquivalentTree f T w : Prop

A cut tree, or Gomory–Hu tree, for f: a flow-equivalent tree in which, for every tree edge s(u, v), the side of u left by deleting that edge is a minimum u–v cut.

• isTree : T.IsTree
• le_weight ⦃s t : V⦄ ⦃p : T.Walk s t⦄ (hp : p.IsPath) ⦃e : Sym2 V⦄ (he : e ∈ p.edges) : pairMinimumValue f s t ≤ w e
• exists_weight_eq ⦃s t : V⦄ (hst : s ≠ t) ⦃p : T.Walk s t⦄ (hp : p.IsPath) : ∃ e ∈ p.edges, w e = pairMinimumValue f s t
• isMinimum_edgeSide ⦃u v : V⦄ (huv : T.Adj u v) : IsMinimum f {u} {v} (T.edgeSide u v)

  Deleting a tree edge leaves a minimum cut between its ends.

theorem TauCeti.TerminalCut.IsCutTree.of_isMinimum_edgeSide {V : Type u_1} {K : Type u_2} [Fintype V] [Zero K] [LinearOrder K] {f : Finset V → K} {T : SimpleGraph V} {w : Sym2 V → K} (hT : T.IsTree) (hmin : ∀ ⦃u v : V⦄, T.Adj u v → IsMinimum f {u} {v} (T.edgeSide u v)) (hw : ∀ ⦃u v : V⦄, T.Adj u v → w s(u, v) = pairMinimumValue f u v) : IsCutTree f T w

A tree is a cut tree as soon as deleting any of its edges leaves a minimum cut between the ends of that edge, with the edge weighted by their minimum cut value: flow-equivalence then follows from the ultrametric inequality along tree paths.

theorem TauCeti.TerminalCut.IsCutTree.apply_edgeSide {V : Type u_1} {K : Type u_2} [Fintype V] [Zero K] [LinearOrder K] {f : Finset V → K} {T : SimpleGraph V} {w : Sym2 V → K} (hT : IsCutTree f T w) {u v : V} (huv : T.Adj u v) : f (T.edgeSide u v) = w s(u, v)

The side left by deleting a tree edge has value equal to the weight of that edge.

theorem TauCeti.TerminalCut.IsCutTree.isMinimum_edgeSide_of_mem_edges {V : Type u_1} {K : Type u_2} [Fintype V] [Zero K] [LinearOrder K] {f : Finset V → K} {T : SimpleGraph V} {w : Sym2 V → K} (hT : IsCutTree f T w) {s t u v : V} {p : T.Walk s t} (hp : p.IsPath) (huv : s(u, v) ∈ p.edges) (hmin : ∀ e ∈ p.edges, w s(u, v) ≤ w e) (hs : s ∈ T.edgeSide u v) : IsMinimum f {s} {t} (T.edgeSide u v)

Query theorem. If s(u, v) has minimum weight on the tree path from s to t, and s lies on the side of u, then that side is a minimum s–t cut. Since the two sides of a tree edge cover the vertices, one of the orientations (u, v) and (v, u) applies.

theorem TauCeti.TerminalCut.IsCutTree.apply_edgeSide_le {V : Type u_1} {K : Type u_2} [Fintype V] [Zero K] [LinearOrder K] {f : Finset V → K} {T : SimpleGraph V} {w : Sym2 V → K} (hT : IsCutTree f T w) {u v : V} (huv : T.Adj u v) (hmin : ∀ e ∈ T.edgeSet, w s(u, v) ≤ w e) {S : Finset V} {s t : V} (hs : s ∈ S) (ht : t ∉ S) : f (T.edgeSide u v) ≤ f S

Global minimum cut. Deleting a tree edge of minimum weight gives a side whose value is at most that of every set separating two vertices.

theorem TauCeti.TerminalCut.IsCutTree.exists_edgeSide_apply_le {V : Type u_1} {K : Type u_2} [Fintype V] [Zero K] [LinearOrder K] {f : Finset V → K} {T : SimpleGraph V} {w : Sym2 V → K} (hT : IsCutTree f T w) [Nontrivial V] : ∃ (u : V) (v : V), T.Adj u v ∧ ∀ (S : Finset V), S.Nonempty → S ≠ Finset.univ → f (T.edgeSide u v) ≤ f S

A minimum-weight edge of a cut tree leaves a side minimizing the set function among all nonempty proper vertex sets.