Auxiliary terminals

The standard reduction of flow and cut problems between two vertex sets A and B to problems between two single vertices adds a fresh source σ with an arrow to every vertex of A, and a fresh sink τ with an arrow from every vertex of B. Here the new vertices live on the sum type V ⊕ Bool: Sum.inl v is the original vertex v, Sum.inr false is σ and Sum.inr true is τ. Every original arrow is retained with its identity, and the capacities of the new arrows are arbitrary parameters. The sets A and B are arbitrary, and may be empty or overlap.

A σ–τ cut S is determined by its original vertices S.toLeft, and its capacity is the capacity of the new arrows it crosses plus the original capacity leaving S.toLeft. A minimum σ–τ cut need not contain all of A, so S.toLeft need not be a cut between A and B. When A and B are disjoint, the vertex set (S.toLeft ∪ A) \ B contains A and avoids B; if the original capacities are nonnegative, each arrow σ → a has capacity at least the total capacity leaving a, and each arrow b → τ at least the total capacity entering b, then this normalization of S has original cut capacity at most the capacity of S.

A walk from a vertex of A to a vertex of B lifts to a walk from σ to τ through the same original vertices, and every walk from σ to τ contains a walk along original arrows from a vertex of A to a vertex of B, so deleting a set of original vertices separates σ from τ exactly when it separates A from B.

Main definitions

• TauCeti.AuxTerminalHom Q A B: the arrow family of Q with the auxiliary terminals added.
• TauCeti.AuxTerminalHom.original, TauCeti.AuxTerminalHom.source and TauCeti.AuxTerminalHom.sink: its three kinds of arrows.
• TauCeti.AuxTerminalHom.originalEquiv: the arrows between original vertices are exactly the original arrows.
• TauCeti.auxTerminalCapacity cap cσ cτ: the capacities cap on original arrows, cσ a on σ → a and cτ b on b → τ.
• TauCeti.auxTerminalRestrict g: the restriction of an assignment to the original arrows.
• TauCeti.setFlowCapacity cap A B: the auxiliary capacities whose new arrows carry the total capacity leaving each a ∈ A and entering each b ∈ B.

Main results

• TauCeti.AuxTerminalHom.forall_iff: a property of all arrows with auxiliary terminals reduces to the original arrows, the arrows from σ and the arrows to τ.
• TauCeti.arrowSum_auxTerminalCapacity: the capacity of a σ–τ cut.
• TauCeti.TerminalCut.IsAdmissible.arrowSum_auxTerminalCapacity: a vertex set containing A and avoiding B, together with σ, has the same cut capacity as in the original network.
• TauCeti.arrowSum_union_sdiff_le_arrowSum_auxTerminalCapacity: the normalization lemma.
• TauCeti.TerminalCut.IsMinimum.isMinimum_union_sdiff and TauCeti.TerminalCut.IsMinimum.arrowSum_union_sdiff: normalizing a minimum σ–τ cut gives a minimum cut between A and B of the same capacity.
• TauCeti.AuxTerminalHom.exists_arrowWalk_vertices_eq and TauCeti.AuxTerminalHom.exists_arrowWalk_map_vertices_subset: lifting walks between A and B to walks between the auxiliary terminals, and projecting them back.
• TauCeti.reachableAvoiding_auxTerminalHom_iff: reachability between the auxiliary terminals after deleting vertices is reachability from A to B.
• TauCeti.AuxTerminalHom.excessAt_inl and TauCeti.AuxTerminalHom.excessAt_inr_true: the excess of an assignment at an original vertex and at the fresh sink.

References

• L. R. Ford, D. R. Fulkerson, Flows in Networks, Princeton University Press, 1962.
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003.

def TauCeti.AuxTerminalHom {V : Type u} (Q : V → V → Type v) (A B : Finset V) : V ⊕ Bool → V ⊕ Bool → Type v

The arrow family of Q with auxiliary terminals for the vertex sets A and B, on the vertex type V ⊕ Bool. The arrows between original vertices Sum.inl v and Sum.inl w are those of Q v w; the fresh source σ = Sum.inr false has one arrow to each Sum.inl a with a ∈ A; the fresh sink τ = Sum.inr true has one arrow from each Sum.inl b with b ∈ B; and there are no other arrows.

@[instance_reducible]

instance TauCeti.AuxTerminalHom.instFintype {V : Type u} (Q : V → V → Type v) (A B : Finset V) [DecidableEq V] [(v w : V) → Fintype (Q v w)] (x y : V ⊕ Bool) : Fintype (AuxTerminalHom Q A B x y)

def TauCeti.AuxTerminalHom.original {V : Type u} {Q : V → V → Type v} {A B : Finset V} {v w : V} (e : Q v w) : AuxTerminalHom Q A B (Sum.inl v) (Sum.inl w)

An original arrow e : Q v w, as an arrow from Sum.inl v to Sum.inl w.

def TauCeti.AuxTerminalHom.source {V : Type u} {Q : V → V → Type v} {A B : Finset V} {a : V} (ha : a ∈ A) : AuxTerminalHom Q A B (Sum.inr false) (Sum.inl a)

The arrow from the fresh source Sum.inr false to a vertex Sum.inl a with a ∈ A.

def TauCeti.AuxTerminalHom.sink {V : Type u} {Q : V → V → Type v} {A B : Finset V} {b : V} (hb : b ∈ B) : AuxTerminalHom Q A B (Sum.inl b) (Sum.inr true)

The arrow from a vertex Sum.inl b with b ∈ B to the fresh sink Sum.inr true.

def TauCeti.AuxTerminalHom.originalEquiv {V : Type u} {Q : V → V → Type v} {A B : Finset V} {v w : V} : Q v w ≃ AuxTerminalHom Q A B (Sum.inl v) (Sum.inl w)

The arrows from Sum.inl v to Sum.inl w are exactly the original arrows Q v w.

@[simp]

theorem TauCeti.AuxTerminalHom.originalEquiv_apply {V : Type u} {Q : V → V → Type v} {A B : Finset V} {v w : V} (e : Q v w) : originalEquiv e = original e

@[simp]

theorem TauCeti.AuxTerminalHom.originalEquiv_symm_original {V : Type u} {Q : V → V → Type v} {A B : Finset V} {v w : V} (e : Q v w) : originalEquiv.symm (original e) = e

@[simp]

theorem TauCeti.AuxTerminalHom.original_originalEquiv_symm {V : Type u} {Q : V → V → Type v} {A B : Finset V} {v w : V} (e : AuxTerminalHom Q A B (Sum.inl v) (Sum.inl w)) : original (originalEquiv.symm e) = e

theorem TauCeti.AuxTerminalHom.original_injective {V : Type u} {Q : V → V → Type v} {A B : Finset V} {v w : V} : Function.Injective original

@[simp]

theorem TauCeti.AuxTerminalHom.original_inj {V : Type u} {Q : V → V → Type v} {A B : Finset V} {v w : V} {e e' : Q v w} : original e = original e' ↔ e = e'

theorem TauCeti.AuxTerminalHom.mem_of_source {V : Type u} {Q : V → V → Type v} {A B : Finset V} {a : V} (e : AuxTerminalHom Q A B (Sum.inr false) (Sum.inl a)) : a ∈ A

The fresh source has an arrow to Sum.inl a only when a ∈ A.

theorem TauCeti.AuxTerminalHom.mem_of_sink {V : Type u} {Q : V → V → Type v} {A B : Finset V} {b : V} (e : AuxTerminalHom Q A B (Sum.inl b) (Sum.inr true)) : b ∈ B

The fresh sink has an arrow from Sum.inl b only when b ∈ B.

theorem TauCeti.AuxTerminalHom.eq_source {V : Type u} {Q : V → V → Type v} {A B : Finset V} {a : V} (e : AuxTerminalHom Q A B (Sum.inr false) (Sum.inl a)) : e = source ⋯

Every arrow from the fresh source to Sum.inl a is source.

theorem TauCeti.AuxTerminalHom.eq_sink {V : Type u} {Q : V → V → Type v} {A B : Finset V} {b : V} (e : AuxTerminalHom Q A B (Sum.inl b) (Sum.inr true)) : e = sink ⋯

Every arrow from Sum.inl b to the fresh sink is sink.

theorem TauCeti.AuxTerminalHom.forall_iff {V : Type u} {Q : V → V → Type v} {A B : Finset V} {P : ⦃x y : V ⊕ Bool⦄ → AuxTerminalHom Q A B x y → Prop} : (∀ ⦃x y : V ⊕ Bool⦄ (e : AuxTerminalHom Q A B x y), P e) ↔ (∀ ⦃v w : V⦄ (e : Q v w), P (original e)) ∧ (∀ ⦃a : V⦄ (ha : a ∈ A), P (source ha)) ∧ ∀ ⦃b : V⦄ (hb : b ∈ B), P (sink hb)

A property holds for every arrow with auxiliary terminals exactly when it holds for every original arrow, every arrow from the fresh source and every arrow to the fresh sink.

instance TauCeti.AuxTerminalHom.instSubsingletonSource {V : Type u} {Q : V → V → Type v} {A B : Finset V} (a : V) : Subsingleton (AuxTerminalHom Q A B (Sum.inr false) (Sum.inl a))

instance TauCeti.AuxTerminalHom.instSubsingletonSink {V : Type u} {Q : V → V → Type v} {A B : Finset V} (b : V) : Subsingleton (AuxTerminalHom Q A B (Sum.inl b) (Sum.inr true))

instance TauCeti.AuxTerminalHom.instIsEmptyToSource {V : Type u} {Q : V → V → Type v} {A B : Finset V} (x : V ⊕ Bool) : IsEmpty (AuxTerminalHom Q A B x (Sum.inr false))

No arrow enters the fresh source.

instance TauCeti.AuxTerminalHom.instIsEmptyFromSink {V : Type u} {Q : V → V → Type v} {A B : Finset V} (y : V ⊕ Bool) : IsEmpty (AuxTerminalHom Q A B (Sum.inr true) y)

No arrow leaves the fresh sink.

instance TauCeti.AuxTerminalHom.instIsEmptySourceSink {V : Type u} {Q : V → V → Type v} {A B : Finset V} : IsEmpty (AuxTerminalHom Q A B (Sum.inr false) (Sum.inr true))

No arrow goes directly from the fresh source to the fresh sink.

def TauCeti.auxTerminalCapacity {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} (cap : Assignment Q K) (cσ cτ : V → K) : Assignment (AuxTerminalHom Q A B) K

The capacities on the arrow family with auxiliary terminals: cap e on an original arrow e, cσ a on the arrow from the fresh source to a, and cτ b on the arrow from b to the fresh sink.

def TauCeti.auxTerminalRestrict {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} (g : Assignment (AuxTerminalHom Q A B) K) : Assignment Q K

The restriction of an assignment with auxiliary terminals to the original arrows.

@[simp]

theorem TauCeti.auxTerminalRestrict_apply {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} (g : Assignment (AuxTerminalHom Q A B) K) {v w : V} (e : Q v w) : auxTerminalRestrict g e = g (AuxTerminalHom.original e)

@[simp]

theorem TauCeti.auxTerminalRestrict_auxTerminalCapacity {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} (cap : Assignment Q K) (cσ cτ : V → K) : auxTerminalRestrict (auxTerminalCapacity cap cσ cτ) = cap

@[simp]

theorem TauCeti.auxTerminalCapacity_original {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} (cap : Assignment Q K) (cσ cτ : V → K) {v w : V} (e : Q v w) : auxTerminalCapacity cap cσ cτ (AuxTerminalHom.original e) = cap e

@[simp]

theorem TauCeti.auxTerminalCapacity_source {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} (cap : Assignment Q K) (cσ cτ : V → K) {a : V} (ha : a ∈ A) : auxTerminalCapacity cap cσ cτ (AuxTerminalHom.source ha) = cσ a

@[simp]

theorem TauCeti.auxTerminalCapacity_sink {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} (cap : Assignment Q K) (cσ cτ : V → K) {b : V} (hb : b ∈ B) : auxTerminalCapacity cap cσ cτ (AuxTerminalHom.sink hb) = cτ b

theorem TauCeti.auxTerminalCapacity_nonneg {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} [Zero K] [Preorder K] {cap : Assignment Q K} {cσ cτ : V → K} (hcap : 0 ≤ cap) (hσ : ∀ a ∈ A, 0 ≤ cσ a) (hτ : ∀ b ∈ B, 0 ≤ cτ b) : 0 ≤ auxTerminalCapacity cap cσ cτ

The capacities with auxiliary terminals are nonnegative when the original capacities and the capacities of the new arrows are.

theorem TauCeti.AuxTerminalHom.sum_inl_inl {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} [AddCommMonoid K] [DecidableEq V] [(v w : V) → Fintype (Q v w)] {x y : V} (g : AuxTerminalHom Q A B (Sum.inl x) (Sum.inl y) → K) : ∑ e : AuxTerminalHom Q A B (Sum.inl x) (Sum.inl y), g e = ∑ e : Q x y, g (original e)

A sum over the arrows between two original vertices is a sum over the original arrows.

theorem TauCeti.AuxTerminalHom.sum_source {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} [AddCommMonoid K] [DecidableEq V] [(v w : V) → Fintype (Q v w)] {a : V} (ha : a ∈ A) (g : AuxTerminalHom Q A B (Sum.inr false) (Sum.inl a) → K) : ∑ e : AuxTerminalHom Q A B (Sum.inr false) (Sum.inl a), g e = g (source ha)

A sum over the arrows from the fresh source to Sum.inl a, for a ∈ A, is the value on source.

theorem TauCeti.AuxTerminalHom.sum_source_of_notMem {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} [AddCommMonoid K] [DecidableEq V] [(v w : V) → Fintype (Q v w)] {a : V} (ha : a ∉ A) (g : AuxTerminalHom Q A B (Sum.inr false) (Sum.inl a) → K) : ∑ e : AuxTerminalHom Q A B (Sum.inr false) (Sum.inl a), g e = 0

There is no arrow from the fresh source to Sum.inl a for a ∉ A.

theorem TauCeti.AuxTerminalHom.sum_sink {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} [AddCommMonoid K] [DecidableEq V] [(v w : V) → Fintype (Q v w)] {b : V} (hb : b ∈ B) (g : AuxTerminalHom Q A B (Sum.inl b) (Sum.inr true) → K) : ∑ e : AuxTerminalHom Q A B (Sum.inl b) (Sum.inr true), g e = g (sink hb)

A sum over the arrows from Sum.inl b to the fresh sink, for b ∈ B, is the value on sink.

theorem TauCeti.AuxTerminalHom.sum_sink_of_notMem {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} [AddCommMonoid K] [DecidableEq V] [(v w : V) → Fintype (Q v w)] {b : V} (hb : b ∉ B) (g : AuxTerminalHom Q A B (Sum.inl b) (Sum.inr true) → K) : ∑ e : AuxTerminalHom Q A B (Sum.inl b) (Sum.inr true), g e = 0

There is no arrow from Sum.inl b to the fresh sink for b ∉ B.

theorem TauCeti.sum_auxTerminalCapacity_source {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} [AddCommMonoid K] [DecidableEq V] [(v w : V) → Fintype (Q v w)] (cap : Assignment Q K) (cσ cτ : V → K) (a : V) : ∑ e : AuxTerminalHom Q A B (Sum.inr false) (Sum.inl a), auxTerminalCapacity cap cσ cτ e = if a ∈ A then cσ a else 0

The total capacity of the arrows from the fresh source to Sum.inl a is cσ a for a ∈ A, and zero otherwise.

theorem TauCeti.sum_auxTerminalCapacity_sink {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} [AddCommMonoid K] [DecidableEq V] [(v w : V) → Fintype (Q v w)] (cap : Assignment Q K) (cσ cτ : V → K) (b : V) : ∑ e : AuxTerminalHom Q A B (Sum.inl b) (Sum.inr true), auxTerminalCapacity cap cσ cτ e = if b ∈ B then cτ b else 0

The total capacity of the arrows from Sum.inl b to the fresh sink is cτ b for b ∈ B, and zero otherwise.

theorem TauCeti.sum_auxTerminalCapacity_inl_inl {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} [AddCommMonoid K] [DecidableEq V] [(v w : V) → Fintype (Q v w)] (cap : Assignment Q K) (cσ cτ : V → K) (x y : V) : ∑ e : AuxTerminalHom Q A B (Sum.inl x) (Sum.inl y), auxTerminalCapacity cap cσ cτ e = ∑ e : Q x y, cap e

The total capacity with auxiliary terminals of the arrows between two original vertices is their original total capacity.

theorem TauCeti.arrowSum_auxTerminalCapacity {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} [AddCommMonoid K] [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] (cap : Assignment Q K) (cσ cτ : V → K) {S : Finset (V ⊕ Bool)} (hσ : Sum.inr false ∈ S) (hτ : Sum.inr true ∉ S) : arrowSum (auxTerminalCapacity cap cσ cτ) S Sᶜ = ∑ a ∈ A \ S.toLeft, cσ a + ∑ b ∈ B ∩ S.toLeft, cτ b + arrowSum cap S.toLeft S.toLeftᶜ

The capacity of a cut S separating the fresh source from the fresh sink is the capacity cσ a of each a ∈ A outside S, plus the capacity cτ b of each b ∈ B inside S, plus the original capacity of the arrows leaving the original vertices of S.

theorem TauCeti.TerminalCut.IsAdmissible.arrowSum_auxTerminalCapacity {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} [AddCommMonoid K] [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] {R : Finset V} (hR : IsAdmissible A B R) (cap : Assignment Q K) (cσ cτ : V → K) : arrowSum (auxTerminalCapacity cap cσ cτ) (R.disjSum {false}) (R.disjSum {false})ᶜ = arrowSum cap R Rᶜ

A vertex set R containing A and avoiding B, together with the fresh source, is a cut with the same capacity as R in the original network.

theorem TauCeti.arrowSum_union_sdiff_le_arrowSum_auxTerminalCapacity {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} [AddCommMonoid K] [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [PartialOrder K] [IsOrderedAddMonoid K] (hAB : Disjoint A B) {cap : Assignment Q K} (hcap : 0 ≤ cap) {cσ cτ : V → K} (hcσ : ∀ a ∈ A, ∑ w : V, ∑ e : Q a w, cap e ≤ cσ a) (hcτ : ∀ b ∈ B, ∑ v : V, ∑ e : Q v b, cap e ≤ cτ b) {S : Finset (V ⊕ Bool)} (hσ : Sum.inr false ∈ S) (hτ : Sum.inr true ∉ S) : arrowSum cap ((S.toLeft ∪ A) \ B) ((S.toLeft ∪ A) \ B)ᶜ ≤ arrowSum (auxTerminalCapacity cap cσ cτ) S Sᶜ

Normalization of auxiliary cuts. Let A and B be disjoint and the original capacities nonnegative, and suppose that the arrow from the fresh source to each a ∈ A has capacity at least the total capacity leaving a, and the arrow from each b ∈ B to the fresh sink has capacity at least the total capacity entering b. Then for every cut S separating the fresh source from the fresh sink, the vertex set (S.toLeft ∪ A) \ B, which is admissible by TerminalCut.isAdmissible_union_sdiff, has original cut capacity at most the capacity of S.

theorem TauCeti.TerminalCut.IsMinimum.arrowSum_union_sdiff {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} [AddCommMonoid K] [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [PartialOrder K] [IsOrderedAddMonoid K] (hAB : Disjoint A B) {cap : Assignment Q K} (hcap : 0 ≤ cap) {cσ cτ : V → K} (hcσ : ∀ a ∈ A, ∑ w : V, ∑ e : Q a w, cap e ≤ cσ a) (hcτ : ∀ b ∈ B, ∑ v : V, ∑ e : Q v b, cap e ≤ cτ b) {S : Finset (V ⊕ Bool)} (hS : IsMinimum (fun (S : Finset (V ⊕ Bool)) => arrowSum (auxTerminalCapacity cap cσ cτ) S Sᶜ) {Sum.inr false} {Sum.inr true} S) : arrowSum cap ((S.toLeft ∪ A) \ B) ((S.toLeft ∪ A) \ B)ᶜ = arrowSum (auxTerminalCapacity cap cσ cτ) S Sᶜ

Normalization of minimum auxiliary cuts. Under the hypotheses of the normalization lemma TauCeti.arrowSum_union_sdiff_le_arrowSum_auxTerminalCapacity, normalizing a minimum cut S between the fresh terminals to the vertex set (S.toLeft ∪ A) \ B preserves its capacity.

theorem TauCeti.TerminalCut.IsMinimum.isMinimum_union_sdiff {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} [AddCommMonoid K] [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [PartialOrder K] [IsOrderedAddMonoid K] (hAB : Disjoint A B) {cap : Assignment Q K} (hcap : 0 ≤ cap) {cσ cτ : V → K} (hcσ : ∀ a ∈ A, ∑ w : V, ∑ e : Q a w, cap e ≤ cσ a) (hcτ : ∀ b ∈ B, ∑ v : V, ∑ e : Q v b, cap e ≤ cτ b) {S : Finset (V ⊕ Bool)} (hS : IsMinimum (fun (S : Finset (V ⊕ Bool)) => arrowSum (auxTerminalCapacity cap cσ cτ) S Sᶜ) {Sum.inr false} {Sum.inr true} S) : IsMinimum (fun (R : Finset V) => arrowSum cap R Rᶜ) A B ((S.toLeft ∪ A) \ B)

Under the hypotheses of the normalization lemma TauCeti.arrowSum_union_sdiff_le_arrowSum_auxTerminalCapacity, normalizing a minimum cut S between the fresh terminals gives a minimum cut (S.toLeft ∪ A) \ B between A and B in the original network.

Capacities for flows between vertex sets

def TauCeti.setFlowCapacity {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [Fintype V] [(v w : V) → Fintype (Q v w)] (cap : Assignment Q K) (A B : Finset V) : Assignment (AuxTerminalHom Q A B) K

The capacities of the auxiliary network for flows between the vertex sets A and B: cap on the original arrows, the total capacity leaving a on the arrow from the fresh source to a ∈ A, and the total capacity entering b on the arrow from b ∈ B to the fresh sink. These satisfy the hypotheses of the normalization lemmas with equality.

theorem TauCeti.setFlowCapacity_def {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} [AddCommMonoid K] [Fintype V] [(v w : V) → Fintype (Q v w)] (cap : Assignment Q K) : setFlowCapacity cap A B = auxTerminalCapacity cap (fun (a : V) => ∑ w : V, ∑ e : Q a w, cap e) fun (b : V) => ∑ v : V, ∑ e : Q v b, cap e

The capacities setFlowCapacity cap A B are the auxiliary capacities auxTerminalCapacity with the total capacity leaving a and entering b on the new arrows.

@[simp]

theorem TauCeti.auxTerminalRestrict_setFlowCapacity {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} [AddCommMonoid K] [Fintype V] [(v w : V) → Fintype (Q v w)] (cap : Assignment Q K) : auxTerminalRestrict (setFlowCapacity cap A B) = cap

@[simp]

theorem TauCeti.setFlowCapacity_original {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} [AddCommMonoid K] [Fintype V] [(v w : V) → Fintype (Q v w)] (cap : Assignment Q K) {v w : V} (e : Q v w) : setFlowCapacity cap A B (AuxTerminalHom.original e) = cap e

@[simp]

theorem TauCeti.setFlowCapacity_source {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} [AddCommMonoid K] [Fintype V] [(v w : V) → Fintype (Q v w)] (cap : Assignment Q K) {a : V} (ha : a ∈ A) : setFlowCapacity cap A B (AuxTerminalHom.source ha) = ∑ w : V, ∑ e : Q a w, cap e

@[simp]

theorem TauCeti.setFlowCapacity_sink {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} [AddCommMonoid K] [Fintype V] [(v w : V) → Fintype (Q v w)] (cap : Assignment Q K) {b : V} (hb : b ∈ B) : setFlowCapacity cap A B (AuxTerminalHom.sink hb) = ∑ v : V, ∑ e : Q v b, cap e

theorem TauCeti.setFlowCapacity_nonneg {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} [AddCommMonoid K] [Fintype V] [(v w : V) → Fintype (Q v w)] {cap : Assignment Q K} [PartialOrder K] [IsOrderedAddMonoid K] (hcap : 0 ≤ cap) : 0 ≤ setFlowCapacity cap A B

The auxiliary capacities are nonnegative when the original capacities are.

theorem TauCeti.setFlowCapacity_mem {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} [AddCommMonoid K] [Fintype V] [(v w : V) → Fintype (Q v w)] {cap : Assignment Q K} {M : Type u_1} [SetLike M K] [AddSubmonoidClass M K] {H : M} (hcap : ∀ ⦃v w : V⦄ (e : Q v w), cap e ∈ H) ⦃x y : V ⊕ Bool⦄ (e : AuxTerminalHom Q A B x y) : setFlowCapacity cap A B e ∈ H

The auxiliary capacities lie in an additive submonoid containing the original capacities.

theorem TauCeti.AuxTerminalHom.exists_arrowWalk_vertices_eq {V : Type u} {Q : V → V → Type v} {A B : Finset V} {a b : V} (ha : a ∈ A) (hb : b ∈ B) (q : ArrowWalk Q a b) : ∃ (p : ArrowWalk (AuxTerminalHom Q A B) (Sum.inr false) (Sum.inr true)), p.vertices = Sum.inr false :: List.map Sum.inl q.vertices ++ [Sum.inr true]

Lifting a walk to auxiliary terminals. A walk from a ∈ A to b ∈ B gives a walk from the fresh source to the fresh sink through the same original vertices.

theorem TauCeti.AuxTerminalHom.exists_arrowWalk_map_vertices_subset {V : Type u} {Q : V → V → Type v} {A B : Finset V} (p : ArrowWalk (AuxTerminalHom Q A B) (Sum.inr false) (Sum.inr true)) : ∃ a ∈ A, ∃ b ∈ B, ∃ (q : ArrowWalk Q a b), List.map Sum.inl q.vertices ⊆ p.vertices

Projecting a walk from auxiliary terminals. A walk from the fresh source to the fresh sink contains a walk along original arrows from a vertex of A to a vertex of B.

theorem TauCeti.reachableAvoiding_auxTerminalHom_iff {V : Type u} {Q : V → V → Type v} {A B : Finset V} {X : Set (V ⊕ Bool)} (hσ : Sum.inr false ∉ X) (hτ : Sum.inr true ∉ X) : ReachableAvoiding (AuxTerminalHom Q A B) X (Sum.inr false) (Sum.inr true) ↔ ∃ a ∈ A, ∃ b ∈ B, ReachableAvoiding Q (Sum.inl ⁻¹' X) a b

The fresh sink is reachable from the fresh source avoiding a set X of vertices not containing either, exactly when some vertex of B is reachable from some vertex of A avoiding the original vertices in X.

theorem TauCeti.AuxTerminalHom.excessAt_inl {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} [AddCommGroup K] [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] (g : Assignment (AuxTerminalHom Q A B) K) (v : V) : excessAt g (Sum.inl v) = excessAt (auxTerminalRestrict g) v + ∑ e : AuxTerminalHom Q A B (Sum.inr false) (Sum.inl v), g e - ∑ e : AuxTerminalHom Q A B (Sum.inl v) (Sum.inr true), g e

The excess at an original vertex Sum.inl v of an assignment with auxiliary terminals is the excess at v of its restriction to the original arrows, plus the value arriving from the fresh source, minus the value sent to the fresh sink.

theorem TauCeti.AuxTerminalHom.excessAt_inr_true {V : Type u} {Q : V → V → Type v} {A B : Finset V} {K : Type w} [AddCommGroup K] [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] (g : Assignment (AuxTerminalHom Q A B) K) : excessAt g (Sum.inr true) = ∑ b : V, ∑ e : AuxTerminalHom Q A B (Sum.inl b) (Sum.inr true), g e

The excess at the fresh sink of an assignment with auxiliary terminals is the total value on the arrows entering it.