Symmetric terminal cuts

For a symmetric set function, complementing a cut exchanges its source and sink terminal sets without changing its value. Consequently the two terminal orders have the same minimum value, and complementation exchanges their smallest and largest minimum source sides.

This interface makes terminal exchange explicit for later uncrossing arguments. Those arguments can choose either side of an undirected cut while the underlying minimum-cut lattice remains oriented by inclusion of the source side.

theorem TauCeti.TerminalCut.IsMinimum.compl {V : Type u_1} {K : Type u_2} [Fintype V] [DecidableEq V] [Preorder K] {f : Finset V → K} (hf : ∀ (S : Finset V), f Sᶜ = f S) {A B S : Finset V} (hS : IsMinimum f A B S) : IsMinimum f B A Sᶜ

Complementing a minimum cut exchanges its source and sink terminal sets.

@[simp]

theorem TauCeti.TerminalCut.isMinimum_compl_iff {V : Type u_1} {K : Type u_2} [Fintype V] [DecidableEq V] [Preorder K] {f : Finset V → K} (hf : ∀ (S : Finset V), f Sᶜ = f S) {A B S : Finset V} : IsMinimum f B A Sᶜ ↔ IsMinimum f A B S

Complementing a minimum cut exchanges its source and sink terminal sets.

theorem TauCeti.TerminalCut.minimumValue_comm {V : Type u_1} {K : Type u_2} [Fintype V] [DecidableEq V] [LinearOrder K] {f : Finset V → K} (hf : ∀ (S : Finset V), f Sᶜ = f S) {A B : Finset V} (hAB : Disjoint A B) : minimumValue f hAB = minimumValue f ⋯

For a symmetric set function, exchanging the terminal sets does not change the minimum cut value.

theorem TauCeti.TerminalCut.pairMinimumValue_comm {V : Type u_1} {K : Type u_2} [Fintype V] [DecidableEq V] [Zero K] [LinearOrder K] {f : Finset V → K} (hf : ∀ (S : Finset V), f Sᶜ = f S) (s t : V) : pairMinimumValue f s t = pairMinimumValue f t s

For a symmetric set function, the minimum cut value between two vertices is symmetric.

theorem TauCeti.TerminalCut.IsMinimum.reattach {V : Type u_1} {K : Type u_2} [Fintype V] [DecidableEq V] [Zero K] [LinearOrder K] {f : Finset V → K} (hf : ∀ (S : Finset V), f Sᶜ = f S) {S X : Finset V} {r x y : V} (hS : IsMinimum f {y} {r} S) (hX : IsMinimum f {r} {x} X) (hyX : y ∉ X) (hxS : x ∉ S) : IsMinimum f {y} {x} S

If S is a minimum y–r cut avoiding x, and some minimum r–x cut avoids y, then S is also a minimum y–x cut for a symmetric set function.

theorem TauCeti.IsSymmSubmodular.smallest_symm_eq_compl_largest {V : Type u_1} {K : Type u_2} [Fintype V] [DecidableEq V] [AddCommMonoid K] [LinearOrder K] {f : Finset V → K} [IsOrderedCancelAddMonoid K] (hf : IsSymmSubmodular f) {A B : Finset V} (hAB : Disjoint A B) : TerminalCut.smallest ⋯ ⋯ = (TerminalCut.largest ⋯ hAB)ᶜ

Exchanging terminal sets sends the smallest minimum source side to the complement of the largest one.

theorem TauCeti.IsSymmSubmodular.largest_symm_eq_compl_smallest {V : Type u_1} {K : Type u_2} [Fintype V] [DecidableEq V] [AddCommMonoid K] [LinearOrder K] {f : Finset V → K} [IsOrderedCancelAddMonoid K] (hf : IsSymmSubmodular f) {A B : Finset V} (hAB : Disjoint A B) : TerminalCut.largest ⋯ ⋯ = (TerminalCut.smallest ⋯ hAB)ᶜ

Exchanging terminal sets sends the largest minimum source side to the complement of the smallest one.