Terminal-set minimum cuts

A terminal cut is a finite vertex set containing all source terminals and no sink terminals. For a set function with linearly ordered values on a finite vertex type, disjoint terminal sets guarantee attainment of a minimum. For a submodular function, the minimizing sides form a distributive sublattice under inclusion; on a finite vertex type with linearly ordered values, it is finite, with a smallest and a largest side. These extremal sides describe which vertices occur in every minimum cut and which occur in at least one.

For two vertices, pairMinimumValue f s t is the minimum cut value λ(s, t), with λ(s, s) = 0. It satisfies the ultrametric inequality min (λ(s, v)) (λ(v, t)) ≤ λ(s, t) for distinct s, t.

The theory is independent of a graph representation and does not require symmetry of the set function. Either terminal set may be empty.

def TauCeti.TerminalCut.IsAdmissible {V : Type u_1} (A B S : Finset V) : Prop

An admissible source side contains A and avoids B.

theorem TauCeti.TerminalCut.isAdmissible_iff {V : Type u_1} {A B S : Finset V} : IsAdmissible A B S ↔ A ⊆ S ∧ Disjoint S B

The characteristic conditions for a terminal cut.

theorem TauCeti.TerminalCut.IsAdmissible.subset {V : Type u_1} {A B S : Finset V} (hS : IsAdmissible A B S) : A ⊆ S

Every source terminal belongs to an admissible side.

theorem TauCeti.TerminalCut.IsAdmissible.disjoint {V : Type u_1} {A B S : Finset V} (hS : IsAdmissible A B S) : Disjoint S B

An admissible side contains no sink terminal.

theorem TauCeti.TerminalCut.isAdmissible_iff_mem_Icc {V : Type u_1} [DecidableEq V] [Fintype V] {A B S : Finset V} : IsAdmissible A B S ↔ S ∈ Set.Icc A Bᶜ

With a finite vertex type, admissible sides form the interval from A to Bᶜ.

@[simp]

theorem TauCeti.TerminalCut.isAdmissible_compl_iff {V : Type u_1} [Fintype V] [DecidableEq V] {A B S : Finset V} : IsAdmissible B A Sᶜ ↔ IsAdmissible A B S

Complementing a source side exchanges the source and sink terminal sets.

theorem TauCeti.TerminalCut.IsAdmissible.compl {V : Type u_1} [Fintype V] [DecidableEq V] {A B S : Finset V} (hS : IsAdmissible A B S) : IsAdmissible B A Sᶜ

The complement of an admissible side is admissible for the exchanged terminal sets.

theorem TauCeti.TerminalCut.isAdmissible_self {V : Type u_1} {A B : Finset V} (hAB : Disjoint A B) : IsAdmissible A B A

Disjoint terminal sets admit the source terminal set itself as a cut.

theorem TauCeti.TerminalCut.IsAdmissible.union {V : Type u_1} [DecidableEq V] {A B S T : Finset V} (hS : IsAdmissible A B S) (hT : IsAdmissible A B T) : IsAdmissible A B (S ∪ T)

Admissibility is closed under union.

theorem TauCeti.TerminalCut.IsAdmissible.inter {V : Type u_1} [DecidableEq V] {A B S T : Finset V} (hS : IsAdmissible A B S) (hT : IsAdmissible A B T) : IsAdmissible A B (S ∩ T)

Admissibility is closed under intersection.

theorem TauCeti.TerminalCut.isAdmissible_union_sdiff {V : Type u_1} [DecidableEq V] {A B : Finset V} (hAB : Disjoint A B) (S : Finset V) : IsAdmissible A B ((S ∪ A) \ B)

For disjoint terminal sets, adding A to any vertex set and removing B gives an admissible side.

def TauCeti.TerminalCut.IsMinimum {V : Type u_1} {K : Type u_3} [Preorder K] (f : Finset V → K) (A B S : Finset V) : Prop

A minimum terminal cut is an admissible side minimizing f over all admissible sides.

theorem TauCeti.TerminalCut.isMinimum_iff {V : Type u_1} {K : Type u_3} [Preorder K] {f : Finset V → K} {A B S : Finset V} : IsMinimum f A B S ↔ IsAdmissible A B S ∧ ∀ (T : Finset V), IsAdmissible A B T → f S ≤ f T

Membership and optimality characterize a minimum terminal cut.

theorem TauCeti.TerminalCut.IsMinimum.admissible {V : Type u_1} {K : Type u_3} [Preorder K] {f : Finset V → K} {A B S : Finset V} (hS : IsMinimum f A B S) : IsAdmissible A B S

Every minimum side is an admissible cut.

theorem TauCeti.TerminalCut.IsMinimum.le {V : Type u_1} {K : Type u_3} [Preorder K] {f : Finset V → K} {A B S T : Finset V} (hS : IsMinimum f A B S) (hT : IsAdmissible A B T) : f S ≤ f T

The value at a minimum side bounds the value at any admissible cut.

theorem TauCeti.TerminalCut.IsMinimum.value_eq {V : Type u_1} {K : Type u_3} [PartialOrder K] {f : Finset V → K} {A B S T : Finset V} (hS : IsMinimum f A B S) (hT : IsMinimum f A B T) : f S = f T

All minimum cuts have the same value.

theorem TauCeti.TerminalCut.exists_minimum {V : Type u_1} {K : Type u_3} [Finite V] [LinearOrder K] (f : Finset V → K) {A B : Finset V} (hAB : Disjoint A B) : ∃ (S : Finset V), IsMinimum f A B S

On a finite vertex type, disjoint terminal sets have an attaining minimum cut.

noncomputable def TauCeti.TerminalCut.minimumValue {V : Type u_1} {K : Type u_3} [Finite V] [LinearOrder K] (f : Finset V → K) {A B : Finset V} (hAB : Disjoint A B) : K

The attained minimum value among cuts separating the disjoint terminal sets.

theorem TauCeti.TerminalCut.minimumValue_le {V : Type u_1} {K : Type u_3} [Finite V] [LinearOrder K] (f : Finset V → K) {A B : Finset V} (hAB : Disjoint A B) {S : Finset V} (hS : IsAdmissible A B S) : minimumValue f hAB ≤ f S

The minimum value is no larger than the value of any admissible cut.

theorem TauCeti.TerminalCut.isMinimum_iff_value_eq {V : Type u_1} {K : Type u_3} [Finite V] [LinearOrder K] (f : Finset V → K) {A B : Finset V} (hAB : Disjoint A B) {S : Finset V} : IsMinimum f A B S ↔ IsAdmissible A B S ∧ f S = minimumValue f hAB

An admissible side is minimum exactly when its value is the minimum value.

theorem TauCeti.TerminalCut.eq_of_le_of_min_le_of_lt {V : Type u_1} {K : Type u_3} [LinearOrder K] {f g : Finset V → K} {b : K} (hgf : ∀ (S : Finset V), g S ≤ f S) (hfg : ∀ (S : Finset V), min (f S) b ≤ g S) {T : Finset V} (hT : f T < b) : g T = f T

Suppose that g ≤ f and that g is at least min f b everywhere. Then f and g agree on every set whose f-value is below b.

theorem TauCeti.TerminalCut.IsMinimum.eq_of_le_of_min_le {V : Type u_1} {K : Type u_3} [LinearOrder K] {f g : Finset V → K} {A B S₀ : Finset V} {b : K} (hgf : ∀ (S : Finset V), g S ≤ f S) (hfg : ∀ (S : Finset V), min (f S) b ≤ g S) (hS₀ : IsAdmissible A B S₀) (hb : f S₀ < b) {S : Finset V} (hS : IsMinimum f A B S) : g S = f S

Suppose that g ≤ f, that g is at least min f b everywhere, and that some admissible side has f-value below b. Then f and g agree on every minimum side of f.

theorem TauCeti.TerminalCut.isMinimum_iff_of_le_of_min_le {V : Type u_1} {K : Type u_3} [LinearOrder K] {f g : Finset V → K} {A B S₀ : Finset V} {b : K} (hgf : ∀ (S : Finset V), g S ≤ f S) (hfg : ∀ (S : Finset V), min (f S) b ≤ g S) (hS₀ : IsAdmissible A B S₀) (hb : f S₀ < b) {S : Finset V} : IsMinimum g A B S ↔ IsMinimum f A B S

Suppose that g ≤ f, that g is at least min f b everywhere, and that some admissible side has f-value below b. Then f and g have the same minimum sides. This is the effect on minimum cuts of truncating all values above b.

theorem TauCeti.TerminalCut.minimumValue_eq_of_le_of_min_le {V : Type u_1} {K : Type u_3} [LinearOrder K] {f g : Finset V → K} {A B S₀ : Finset V} {b : K} [Finite V] (hAB : Disjoint A B) (hgf : ∀ (S : Finset V), g S ≤ f S) (hfg : ∀ (S : Finset V), min (f S) b ≤ g S) (hS₀ : IsAdmissible A B S₀) (hb : f S₀ < b) : minimumValue g hAB = minimumValue f hAB

Under the hypotheses of TauCeti.TerminalCut.isMinimum_iff_of_le_of_min_le, the set functions f and g have the same minimum value.

@[simp]

theorem TauCeti.TerminalCut.isAdmissible_map_iff {V : Type u_1} {W : Type u_2} (e : V ↪ W) {A B S : Finset V} : IsAdmissible (Finset.map e A) (Finset.map e B) (Finset.map e S) ↔ IsAdmissible A B S

An injective relabeling preserves the conditions on terminal cuts.

theorem TauCeti.TerminalCut.isMinimum_map_iff {V : Type u_1} {W : Type u_2} {K : Type u_3} [Preorder K] (e : V ≃ W) {f : Finset V → K} {g : Finset W → K} (hfg : ∀ (S : Finset V), g (Finset.map e.toEmbedding S) = f S) {A B S : Finset V} : IsMinimum g (Finset.map e.toEmbedding A) (Finset.map e.toEmbedding B) (Finset.map e.toEmbedding S) ↔ IsMinimum f A B S

Relabeling all vertices preserves minimum cuts whenever it preserves the set function.

theorem TauCeti.TerminalCut.minimumValue_map {V : Type u_1} {W : Type u_2} {K : Type u_3} [Finite V] [Finite W] [LinearOrder K] (e : V ≃ W) {f : Finset V → K} {g : Finset W → K} (hfg : ∀ (S : Finset V), g (Finset.map e.toEmbedding S) = f S) {A B : Finset V} (hAB : Disjoint A B) : minimumValue g ⋯ = minimumValue f hAB

Relabeling vertices does not change the minimum cut value.

def TauCeti.TerminalCut.minimizers {V : Type u_1} {K : Type u_3} [DecidableEq V] [AddCommMonoid K] [PartialOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) (A B : Finset V) : Sublattice (Finset V)

The minimum terminal cuts, as a sublattice of finite vertex sets. Its induced lattice is distributive, and is finite when the vertex type is finite.

@[simp]

theorem TauCeti.TerminalCut.mem_minimizers {V : Type u_1} {K : Type u_3} [DecidableEq V] [AddCommMonoid K] [PartialOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) (A B : Finset V) {S : Finset V} : S ∈ minimizers hf A B ↔ IsMinimum f A B S

Membership in the cut lattice is precisely minimum-cut optimality.

theorem TauCeti.TerminalCut.IsMinimum.union {V : Type u_1} {K : Type u_3} [DecidableEq V] [AddCommMonoid K] [PartialOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) {A B S T : Finset V} (hS : IsMinimum f A B S) (hT : IsMinimum f A B T) : IsMinimum f A B (S ∪ T)

The union of minimum cuts is minimum.

theorem TauCeti.TerminalCut.IsMinimum.inter {V : Type u_1} {K : Type u_3} [DecidableEq V] [AddCommMonoid K] [PartialOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) {A B S T : Finset V} (hS : IsMinimum f A B S) (hT : IsMinimum f A B T) : IsMinimum f A B (S ∩ T)

The intersection of minimum cuts is minimum.

def TauCeti.TerminalCut.minimizersOrderIso {V : Type u_1} {W : Type u_2} {K : Type u_3} [DecidableEq V] [AddCommMonoid K] [PartialOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) (A B : Finset V) [DecidableEq W] (e : V ≃ W) {g : Finset W → K} (hg : IsSubmodular g) (hfg : ∀ (S : Finset V), g (Finset.map e.toEmbedding S) = f S) : ↥(minimizers hf A B) ≃o ↥(minimizers hg (Finset.map e.toEmbedding A) (Finset.map e.toEmbedding B))

A value-preserving vertex equivalence identifies the lattices of minimum cuts.

@[simp]

theorem TauCeti.TerminalCut.minimizersOrderIso_apply {V : Type u_1} {W : Type u_2} {K : Type u_3} [DecidableEq V] [AddCommMonoid K] [PartialOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) (A B : Finset V) [DecidableEq W] (e : V ≃ W) {g : Finset W → K} (hg : IsSubmodular g) (hfg : ∀ (S : Finset V), g (Finset.map e.toEmbedding S) = f S) (S : ↥(minimizers hf A B)) : ↑((minimizersOrderIso hf A B e hg hfg) S) = Finset.map e.toEmbedding ↑S

The minimum-cut order isomorphism maps each source side by the vertex equivalence.

@[simp]

theorem TauCeti.TerminalCut.minimizersOrderIso_symm_apply {V : Type u_1} {W : Type u_2} {K : Type u_3} [DecidableEq V] [AddCommMonoid K] [PartialOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) (A B : Finset V) [DecidableEq W] (e : V ≃ W) {g : Finset W → K} (hg : IsSubmodular g) (hfg : ∀ (S : Finset V), g (Finset.map e.toEmbedding S) = f S) (S : ↥(minimizers hg (Finset.map e.toEmbedding A) (Finset.map e.toEmbedding B))) : ↑((minimizersOrderIso hf A B e hg hfg).symm S) = Finset.map e.symm.toEmbedding ↑S

The inverse minimum-cut isomorphism relabels by the inverse vertex equivalence.

@[reducible, inline]

noncomputable abbrev TauCeti.TerminalCut.minimizersBoundedOrder {V : Type u_1} {K : Type u_3} [DecidableEq V] [Finite V] [AddCommMonoid K] [LinearOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) {A B : Finset V} (hAB : Disjoint A B) : BoundedOrder ↥(minimizers hf A B)

The finite nonempty lattice of minimum cuts has bottom and top elements.

theorem TauCeti.TerminalCut.exists_isLeast {V : Type u_1} {K : Type u_3} [DecidableEq V] [Finite V] [AddCommMonoid K] [LinearOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) {A B : Finset V} (hAB : Disjoint A B) : ∃ (S : Finset V), IsLeast {T : Finset V | IsMinimum f A B T} S

Minimum terminal cuts have a least side under inclusion.

theorem TauCeti.TerminalCut.exists_isGreatest {V : Type u_1} {K : Type u_3} [DecidableEq V] [Finite V] [AddCommMonoid K] [LinearOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) {A B : Finset V} (hAB : Disjoint A B) : ∃ (S : Finset V), IsGreatest {T : Finset V | IsMinimum f A B T} S

Minimum terminal cuts have a greatest side under inclusion.

noncomputable def TauCeti.TerminalCut.smallest {V : Type u_1} {K : Type u_3} [DecidableEq V] [Finite V] [AddCommMonoid K] [LinearOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) {A B : Finset V} (hAB : Disjoint A B) : Finset V

The smallest minimum source side.

noncomputable def TauCeti.TerminalCut.largest {V : Type u_1} {K : Type u_3} [DecidableEq V] [Finite V] [AddCommMonoid K] [LinearOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) {A B : Finset V} (hAB : Disjoint A B) : Finset V

The largest minimum source side.

theorem TauCeti.TerminalCut.isLeast_smallest {V : Type u_1} {K : Type u_3} [DecidableEq V] [Finite V] [AddCommMonoid K] [LinearOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) {A B : Finset V} (hAB : Disjoint A B) : IsLeast {T : Finset V | IsMinimum f A B T} (smallest hf hAB)

The smallest side is minimum and contained in every minimum side.

theorem TauCeti.TerminalCut.isGreatest_largest {V : Type u_1} {K : Type u_3} [DecidableEq V] [Finite V] [AddCommMonoid K] [LinearOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) {A B : Finset V} (hAB : Disjoint A B) : IsGreatest {T : Finset V | IsMinimum f A B T} (largest hf hAB)

The largest side is minimum and contains every minimum side.

theorem TauCeti.TerminalCut.smallest_mem_minimizers {V : Type u_1} {K : Type u_3} [DecidableEq V] [Finite V] [AddCommMonoid K] [LinearOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) {A B : Finset V} (hAB : Disjoint A B) : smallest hf hAB ∈ minimizers hf A B

The smallest minimum side belongs to the minimizer lattice.

theorem TauCeti.TerminalCut.largest_mem_minimizers {V : Type u_1} {K : Type u_3} [DecidableEq V] [Finite V] [AddCommMonoid K] [LinearOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) {A B : Finset V} (hAB : Disjoint A B) : largest hf hAB ∈ minimizers hf A B

The largest minimum side belongs to the minimizer lattice.

theorem TauCeti.TerminalCut.smallest_eq_iff {V : Type u_1} {K : Type u_3} [DecidableEq V] [Finite V] [AddCommMonoid K] [LinearOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) {A B : Finset V} (hAB : Disjoint A B) {S : Finset V} : smallest hf hAB = S ↔ IsLeast {T : Finset V | IsMinimum f A B T} S

The least property characterizes the smallest side uniquely.

theorem TauCeti.TerminalCut.largest_eq_iff {V : Type u_1} {K : Type u_3} [DecidableEq V] [Finite V] [AddCommMonoid K] [LinearOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) {A B : Finset V} (hAB : Disjoint A B) {S : Finset V} : largest hf hAB = S ↔ IsGreatest {T : Finset V | IsMinimum f A B T} S

The greatest property characterizes the largest side uniquely.

@[simp]

theorem TauCeti.TerminalCut.coe_bot_minimizers {V : Type u_1} {K : Type u_3} [DecidableEq V] [Finite V] [AddCommMonoid K] [LinearOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) {A B : Finset V} (hAB : Disjoint A B) : ↑⊥ = smallest hf hAB

The bottom of the bounded minimizer lattice is the smallest minimum source side.

@[simp]

theorem TauCeti.TerminalCut.coe_top_minimizers {V : Type u_1} {K : Type u_3} [DecidableEq V] [Finite V] [AddCommMonoid K] [LinearOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) {A B : Finset V} (hAB : Disjoint A B) : ↑⊤ = largest hf hAB

The top of the bounded minimizer lattice is the largest minimum source side.

theorem TauCeti.TerminalCut.smallest_map {V : Type u_1} {W : Type u_2} {K : Type u_3} [DecidableEq V] [Finite V] [AddCommMonoid K] [LinearOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) {A B : Finset V} [DecidableEq W] [Finite W] (e : V ≃ W) {g : Finset W → K} (hg : IsSubmodular g) (hfg : ∀ (S : Finset V), g (Finset.map e.toEmbedding S) = f S) (hAB : Disjoint A B) : smallest hg ⋯ = Finset.map e.toEmbedding (smallest hf hAB)

Relabeling vertices transports the smallest minimum source side.

theorem TauCeti.TerminalCut.largest_map {V : Type u_1} {W : Type u_2} {K : Type u_3} [DecidableEq V] [Finite V] [AddCommMonoid K] [LinearOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) {A B : Finset V} [DecidableEq W] [Finite W] (e : V ≃ W) {g : Finset W → K} (hg : IsSubmodular g) (hfg : ∀ (S : Finset V), g (Finset.map e.toEmbedding S) = f S) (hAB : Disjoint A B) : largest hg ⋯ = Finset.map e.toEmbedding (largest hf hAB)

Relabeling vertices transports the largest minimum source side.

@[simp]

theorem TauCeti.TerminalCut.mem_smallest_iff {V : Type u_1} {K : Type u_3} [DecidableEq V] [Finite V] [AddCommMonoid K] [LinearOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) {A B : Finset V} (hAB : Disjoint A B) {v : V} : v ∈ smallest hf hAB ↔ ∀ (S : Finset V), IsMinimum f A B S → v ∈ S

A vertex belongs to the smallest cut exactly when it belongs to every minimum cut.

@[simp]

theorem TauCeti.TerminalCut.mem_largest_iff {V : Type u_1} {K : Type u_3} [DecidableEq V] [Finite V] [AddCommMonoid K] [LinearOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) {A B : Finset V} (hAB : Disjoint A B) {v : V} : v ∈ largest hf hAB ↔ ∃ (S : Finset V), IsMinimum f A B S ∧ v ∈ S

A vertex belongs to the largest cut exactly when it belongs to some minimum cut.

theorem TauCeti.TerminalCut.existsUnique_minimum_iff {V : Type u_1} {K : Type u_3} [DecidableEq V] [Finite V] [AddCommMonoid K] [LinearOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) {A B : Finset V} (hAB : Disjoint A B) : (∃! S : Finset V, IsMinimum f A B S) ↔ smallest hf hAB = largest hf hAB

There is a unique minimum cut exactly when the smallest and largest sides agree.

@[simp]

theorem TauCeti.TerminalCut.isAdmissible_singleton {V : Type u_1} {s t : V} {S : Finset V} : IsAdmissible {s} {t} S ↔ s ∈ S ∧ t ∉ S

Singleton terminal sets recover the usual source-membership and sink-exclusion conditions.

theorem TauCeti.TerminalCut.IsAdmissible.ne {V : Type u_1} {s t : V} {S : Finset V} (hS : IsAdmissible {s} {t} S) : s ≠ t

A side admissible for a pair of singleton terminal sets separates distinct terminals.

theorem TauCeti.TerminalCut.isMinimum_singleton_iff {V : Type u_1} {K : Type u_3} [Preorder K] {f : Finset V → K} {s t : V} {S : Finset V} : IsMinimum f {s} {t} S ↔ s ∈ S ∧ t ∉ S ∧ ∀ (T : Finset V), s ∈ T → t ∉ T → f S ≤ f T

A minimum cut for a pair of singleton terminal sets has the usual source-membership, sink-exclusion, and optimality characterization.

noncomputable def TauCeti.TerminalCut.pairMinimumValue {V : Type u_1} {K : Type u_3} [Finite V] [Zero K] [LinearOrder K] (f : Finset V → K) (s t : V) : K

The minimum cut value λ(s, t) between two vertices: the minimum value of a cut containing s and not t when s ≠ t, and zero on the diagonal.

@[simp]

theorem TauCeti.TerminalCut.pairMinimumValue_self {V : Type u_1} {K : Type u_3} [Finite V] [Zero K] [LinearOrder K] (f : Finset V → K) (s : V) : pairMinimumValue f s s = 0

The minimum cut value between a vertex and itself is zero by convention.

theorem TauCeti.TerminalCut.pairMinimumValue_of_ne {V : Type u_1} {K : Type u_3} [Finite V] [Zero K] [LinearOrder K] (f : Finset V → K) {s t : V} (hst : s ≠ t) : pairMinimumValue f s t = minimumValue f ⋯

Between distinct vertices, the minimum cut value is that of the singleton terminal sets.

theorem TauCeti.TerminalCut.pairMinimumValue_le {V : Type u_1} {K : Type u_3} [Finite V] [Zero K] [LinearOrder K] (f : Finset V → K) {s t : V} {S : Finset V} (hs : s ∈ S) (ht : t ∉ S) : pairMinimumValue f s t ≤ f S

The minimum cut value between two vertices is no larger than the value of any cut separating them.

theorem TauCeti.TerminalCut.IsMinimum.pairMinimumValue_eq {V : Type u_1} {K : Type u_3} [Finite V] [Zero K] [LinearOrder K] {f : Finset V → K} {s t : V} {S : Finset V} (hS : IsMinimum f {s} {t} S) : pairMinimumValue f s t = f S

A minimum cut between two vertices attains their minimum cut value.

theorem TauCeti.TerminalCut.isMinimum_singleton_iff_pairMinimumValue_eq {V : Type u_1} {K : Type u_3} [Finite V] [Zero K] [LinearOrder K] (f : Finset V → K) {s t : V} {S : Finset V} : IsMinimum f {s} {t} S ↔ s ∈ S ∧ t ∉ S ∧ f S = pairMinimumValue f s t

A cut separating two vertices is minimum exactly when it attains their minimum cut value.

theorem TauCeti.TerminalCut.min_pairMinimumValue_le {V : Type u_1} {K : Type u_3} [Finite V] [Zero K] [LinearOrder K] (f : Finset V → K) {s t : V} (hst : s ≠ t) (v : V) : min (pairMinimumValue f s v) (pairMinimumValue f v t) ≤ pairMinimumValue f s t

Ultrametric inequality for minimum cut values: every cut separating s from t separates s from v or v from t. The intermediate vertex v is arbitrary.

Examples

On six vertices, charge one unit for including vertex 4, and nothing for the other vertices. With sources 0, 1 and sinks 2, 3, the two minimum source sides are {0, 1} and {0, 1, 5}. This nonconstant modular function also illustrates that empty terminal sets cause no exception to attainment or to the smallest and largest cut formulas.