Path–cycle decomposition of nonnegative arrow assignments

Every nonnegative arrow assignment f on a finite arrow family is a finite sum of positively weighted directed paths and directed cycles, with equality on every arrow. No conservation or capacity condition is needed: each path runs from a vertex of negative excess of f (a supply vertex) to a vertex of positive excess (a demand vertex), and its interior vertices are unrestricted. The total weight of the paths leaving a supply vertex is minus its excess, the total weight of the paths entering a demand vertex is its excess, and every component is bounded arrowwise by f. A walk of weight q contributes n • q to an arrow it traverses n times, as in TauCeti.walkAssignment, so the theory needs no multiplicative unit; paths and cycles traverse each arrow at most once.

There is such a decomposition with at most as many components as arrows of positive value, and with all weights in any additive subgroup containing the values of f. For an ordinary s–t flow every path of a decomposition runs from s to t, and the path weights add up to the value of the flow; for a circulation there are no paths at all.

Main definitions

• TauCeti.WeightedWalk and TauCeti.WeightedClosedWalk: directed walks and closed walks with a weight, and their assignments.
• TauCeti.PathCycleDecomposition f: a decomposition of f into positively weighted directed paths from supply to demand vertices and positively weighted directed cycles.
• TauCeti.PathCycleDecomposition.pathAssignment and TauCeti.PathCycleDecomposition.cycleAssignment: the sums of the path and cycle components.

Main results

• TauCeti.exists_pathCycleDecomposition: every nonnegative assignment has a path–cycle decomposition with at most as many components as arrows of positive value, all of whose weights lie in any given additive subgroup containing the values of the assignment.
• TauCeti.PathCycleDecomposition.sum_weight_filter_source_eq_negPart and TauCeti.PathCycleDecomposition.sum_weight_filter_target_eq_posPart: the supply and demand identities.
• TauCeti.PathCycleDecomposition.assignment_le_of_mem_paths and TauCeti.PathCycleDecomposition.assignment_le_of_mem_cycles: every component is bounded arrowwise by the decomposed assignment.
• TauCeti.PathCycleDecomposition.paths_eq_nil: a decomposition of a circulation consists of cycles only.
• TauCeti.PathCycleDecomposition.source_eq_of_mem_paths, TauCeti.PathCycleDecomposition.target_eq_of_mem_paths and TauCeti.PathCycleDecomposition.sum_weight_paths_eq_val: the decomposition of an ordinary s–t flow, whose paths run from s to t with total weight the value of the flow.
• TauCeti.PathCycleDecomposition.pathAssignment_apply_le_val: the path components of a decomposition of an ordinary flow carry at most its value on every arrow.
• TauCeti.PathCycleDecomposition.weight_eq_one_of_mem_paths and TauCeti.PathCycleDecomposition.pairwise_disjoint_arrows: for an integer assignment carrying at most one unit on every arrow, every path component has weight one and different path components traverse no common arrow.
• TauCeti.Flow.exists_paths_card_eq_val: an integer s–t flow carrying at most one unit on every arrow carries as many arrow-disjoint s–t paths as its value.
• TauCeti.Flow.exists_paths_card_eq_val_card_filter_le: an integer s–t flow carries a family of s–t paths, repetitions allowed, with as many members as its value, such that every vertex other than s lies on at most as many members as the value entering it.

Implementation notes

The decomposition is built by peeling off one weighted path or cycle at a time. If the arrows of positive value contain a directed cycle, that cycle is subtracted with its bottleneck as weight; otherwise a path of positive arrows from a vertex that no positive arrow enters to a vertex that no positive arrow leaves is subtracted with its bottleneck as weight. Each step makes the value of a positive arrow zero, which bounds the number of components, and each weight is a value of the current assignment, which keeps the weights in the subgroup.

References

• L. R. Ford, D. R. Fulkerson, Flows in Networks, Princeton University Press, 1962.
• R. K. Ahuja, T. L. Magnanti, J. B. Orlin, Network Flows: Theory, Algorithms, and Applications, Prentice Hall, 1993, Section 3.5.

structure TauCeti.WeightedWalk {V : Type u} (Q : V → V → Type v) (K : Type w) : Type (max (max u v) w)

A directed walk along the arrow family Q, together with its endpoints and a weight.

• source : V

  The first vertex of the walk.

• target : V

  The last vertex of the walk.

• walk : ArrowWalk Q self.source self.target

  The walk itself.

• weight : K

  The weight of the walk.

structure TauCeti.WeightedClosedWalk {V : Type u} (Q : V → V → Type v) (K : Type w) : Type (max (max u v) w)

A closed directed walk along the arrow family Q, together with its base vertex and a weight.

• base : V

  The first and last vertex of the closed walk.

• walk : ArrowWalk Q self.base self.base

  The closed walk itself.

• weight : K

  The weight of the closed walk.

noncomputable def TauCeti.WeightedWalk.assignment {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] (p : WeightedWalk Q K) : Assignment Q K

The assignment of a weighted walk: its walk weighted by its weight.

theorem TauCeti.WeightedWalk.assignment_def {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] (p : WeightedWalk Q K) : p.assignment = walkAssignment p.walk p.weight

noncomputable def TauCeti.WeightedClosedWalk.assignment {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] (c : WeightedClosedWalk Q K) : Assignment Q K

The assignment of a weighted closed walk: its walk weighted by its weight.

theorem TauCeti.WeightedClosedWalk.assignment_def {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] (c : WeightedClosedWalk Q K) : c.assignment = walkAssignment c.walk c.weight

theorem TauCeti.WeightedWalk.excessAt_sum_map_assignment {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [DecidableEq V] (l : List (WeightedWalk Q K)) (v : V) : excessAt (List.map assignment l).sum v = (List.map weight (List.filter (fun (p : WeightedWalk Q K) => decide (p.target = v)) l)).sum - (List.map weight (List.filter (fun (p : WeightedWalk Q K) => decide (p.source = v)) l)).sum

The excess at v of a sum of weighted walks is the total weight of the walks ending at v minus the total weight of the walks starting at v.

theorem TauCeti.WeightedWalk.sum_excessAt_sum_map_assignment {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [DecidableEq V] (l : List (WeightedWalk Q K)) (S : Finset V) : ∑ v ∈ S, excessAt (List.map assignment l).sum v = (List.map weight (List.filter (fun (p : WeightedWalk Q K) => decide (p.target ∈ S)) l)).sum - (List.map weight (List.filter (fun (p : WeightedWalk Q K) => decide (p.source ∈ S)) l)).sum

The total excess on a vertex set S of a sum of weighted walks is the total weight of the walks ending in S minus the total weight of the walks starting in S.

theorem TauCeti.WeightedClosedWalk.isCirculation_sum_map_assignment {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] (l : List (WeightedClosedWalk Q K)) : IsCirculation (List.map assignment l).sum

The excess of a sum of weighted closed walks vanishes.

structure TauCeti.PathCycleDecomposition {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [Preorder K] (f : Assignment Q K) : Type (max (max u v) w)

A path–cycle decomposition of the arrow assignment f: finite lists of positively weighted directed paths and positively weighted directed cycles whose assignments add up to f, such that every path starts at a vertex of negative excess of f and ends at a vertex of positive excess of f.

• paths : List (WeightedWalk Q K)

  The weighted paths.

• cycles : List (WeightedClosedWalk Q K)

  The weighted cycles.

• isPath_walk (p : WeightedWalk Q K) : p ∈ self.paths → p.walk.IsPath

  Every path component is a directed path.

• isCycle_walk (c : WeightedClosedWalk Q K) : c ∈ self.cycles → c.walk.IsCycle

  Every cycle component is a directed cycle.

• weight_pos_of_mem_paths (p : WeightedWalk Q K) : p ∈ self.paths → 0 < p.weight

  Every path component has positive weight.

• weight_pos_of_mem_cycles (c : WeightedClosedWalk Q K) : c ∈ self.cycles → 0 < c.weight

  Every cycle component has positive weight.

• excessAt_source_neg (p : WeightedWalk Q K) : p ∈ self.paths → excessAt f p.source < 0

  Every path starts at a vertex of negative excess.

• excessAt_target_pos (p : WeightedWalk Q K) : p ∈ self.paths → 0 < excessAt f p.target

  Every path ends at a vertex of positive excess.

• sum_paths_add_sum_cycles : (List.map WeightedWalk.assignment self.paths).sum + (List.map WeightedClosedWalk.assignment self.cycles).sum = f

  The components add up to the decomposed assignment.

theorem TauCeti.PathCycleDecomposition.ext_iff {V : Type u} {Q : V → V → Type v} {K : Type w} {inst✝ : Fintype V} {inst✝¹ : (x y : V) → Fintype (Q x y)} {inst✝² : AddCommGroup K} {inst✝³ : Preorder K} {f : Assignment Q K} {x y : PathCycleDecomposition f} : x = y ↔ x.paths = y.paths ∧ x.cycles = y.cycles

theorem TauCeti.PathCycleDecomposition.ext {V : Type u} {Q : V → V → Type v} {K : Type w} {inst✝ : Fintype V} {inst✝¹ : (x y : V) → Fintype (Q x y)} {inst✝² : AddCommGroup K} {inst✝³ : Preorder K} {f : Assignment Q K} {x y : PathCycleDecomposition f} (paths : x.paths = y.paths) (cycles : x.cycles = y.cycles) : x = y

noncomputable def TauCeti.PathCycleDecomposition.pathAssignment {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [Preorder K] {f : Assignment Q K} (D : PathCycleDecomposition f) : Assignment Q K

The sum of the path components of a decomposition.

noncomputable def TauCeti.PathCycleDecomposition.cycleAssignment {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [Preorder K] {f : Assignment Q K} (D : PathCycleDecomposition f) : Assignment Q K

The sum of the cycle components of a decomposition.

theorem TauCeti.PathCycleDecomposition.pathAssignment_def {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [Preorder K] {f : Assignment Q K} (D : PathCycleDecomposition f) : D.pathAssignment = (List.map WeightedWalk.assignment D.paths).sum

theorem TauCeti.PathCycleDecomposition.cycleAssignment_def {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [Preorder K] {f : Assignment Q K} (D : PathCycleDecomposition f) : D.cycleAssignment = (List.map WeightedClosedWalk.assignment D.cycles).sum

@[simp]

theorem TauCeti.PathCycleDecomposition.pathAssignment_add_cycleAssignment {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [Preorder K] {f : Assignment Q K} (D : PathCycleDecomposition f) : D.pathAssignment + D.cycleAssignment = f

theorem TauCeti.PathCycleDecomposition.isCirculation_cycleAssignment {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [Preorder K] {f : Assignment Q K} (D : PathCycleDecomposition f) : IsCirculation D.cycleAssignment

The cycle components form a circulation.

@[simp]

theorem TauCeti.PathCycleDecomposition.excessAt_pathAssignment {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [Preorder K] {f : Assignment Q K} (D : PathCycleDecomposition f) (v : V) : excessAt D.pathAssignment v = excessAt f v

The path components have the same excess as the decomposed assignment.

theorem TauCeti.PathCycleDecomposition.excessAt_eq_sum_sub_sum {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [Preorder K] {f : Assignment Q K} (D : PathCycleDecomposition f) [DecidableEq V] (v : V) : excessAt f v = (List.map WeightedWalk.weight (List.filter (fun (p : WeightedWalk Q K) => decide (p.target = v)) D.paths)).sum - (List.map WeightedWalk.weight (List.filter (fun (p : WeightedWalk Q K) => decide (p.source = v)) D.paths)).sum

The excess of the decomposed assignment at v is the total weight of the paths ending at v minus the total weight of the paths starting at v.

theorem TauCeti.PathCycleDecomposition.source_ne_of_mem_paths {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [Preorder K] {f : Assignment Q K} (D : PathCycleDecomposition f) {p : WeightedWalk Q K} (hp : p ∈ D.paths) {v : V} (hv : 0 ≤ excessAt f v) : p.source ≠ v

No path of a decomposition starts at a vertex of nonnegative excess.

theorem TauCeti.PathCycleDecomposition.target_ne_of_mem_paths {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [Preorder K] {f : Assignment Q K} (D : PathCycleDecomposition f) {p : WeightedWalk Q K} (hp : p ∈ D.paths) {v : V} (hv : excessAt f v ≤ 0) : p.target ≠ v

No path of a decomposition ends at a vertex of nonpositive excess.

theorem TauCeti.PathCycleDecomposition.assignment_apply_of_mem_arrows {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [Preorder K] {f : Assignment Q K} (D : PathCycleDecomposition f) {p : WeightedWalk Q K} (hp : p ∈ D.paths) {x y : V} {e : Q x y} (he : ⟨x, ⟨y, e⟩⟩ ∈ p.walk.arrows) : p.assignment e = p.weight

A path component of a decomposition places its weight on each of its arrows.

theorem TauCeti.PathCycleDecomposition.paths_eq_nil {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [Preorder K] {f : Assignment Q K} (D : PathCycleDecomposition f) (hf : IsCirculation f) : D.paths = []

A decomposition of a circulation has no path components.

theorem TauCeti.PathCycleDecomposition.assignment_nonneg_of_mem_paths {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [Preorder K] {f : Assignment Q K} (D : PathCycleDecomposition f) {p : WeightedWalk Q K} (hp : p ∈ D.paths) : 0 ≤ p.assignment

A path component of a decomposition is nonnegative.

theorem TauCeti.PathCycleDecomposition.assignment_nonneg_of_mem_cycles {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} (D : PathCycleDecomposition f) {c : WeightedClosedWalk Q K} (hc : c ∈ D.cycles) : 0 ≤ c.assignment

theorem TauCeti.PathCycleDecomposition.pathAssignment_nonneg {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} (D : PathCycleDecomposition f) : 0 ≤ D.pathAssignment

theorem TauCeti.PathCycleDecomposition.cycleAssignment_nonneg {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} (D : PathCycleDecomposition f) : 0 ≤ D.cycleAssignment

theorem TauCeti.PathCycleDecomposition.nonneg {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} (D : PathCycleDecomposition f) : 0 ≤ f

An assignment with a path–cycle decomposition is nonnegative.

theorem TauCeti.PathCycleDecomposition.pathAssignment_le {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} (D : PathCycleDecomposition f) : D.pathAssignment ≤ f

theorem TauCeti.PathCycleDecomposition.cycleAssignment_le {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} (D : PathCycleDecomposition f) : D.cycleAssignment ≤ f

theorem TauCeti.PathCycleDecomposition.assignment_le_of_mem_paths {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} (D : PathCycleDecomposition f) {p : WeightedWalk Q K} (hp : p ∈ D.paths) : p.assignment ≤ f

Every path component is bounded arrowwise by the decomposed assignment.

theorem TauCeti.PathCycleDecomposition.assignment_le_of_mem_cycles {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} (D : PathCycleDecomposition f) {c : WeightedClosedWalk Q K} (hc : c ∈ D.cycles) : c.assignment ≤ f

Every cycle component is bounded arrowwise by the decomposed assignment.

theorem TauCeti.PathCycleDecomposition.pos_of_mem_arrows_of_mem_cycles {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} (D : PathCycleDecomposition f) {c : WeightedClosedWalk Q K} (hc : c ∈ D.cycles) {a : (x : V) × (y : V) × Q x y} (ha : a ∈ c.walk.arrows) : 0 < f a.snd.snd

Every arrow of a cycle component has positive value in the decomposed assignment.

theorem TauCeti.PathCycleDecomposition.paths_eq_nil_and_cycles_eq_nil_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} (D : PathCycleDecomposition f) : D.paths = [] ∧ D.cycles = [] ↔ f = 0

A decomposition has no components exactly when it decomposes the zero assignment.

Decompositions of ordinary flows

theorem TauCeti.PathCycleDecomposition.source_eq_of_mem_paths {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] {cap : Assignment Q K} {s t : V} [Preorder K] {f : Flow cap s t} (D : PathCycleDecomposition f.toFun) {p : WeightedWalk Q K} (hp : p ∈ D.paths) : p.source = s

Every path of a decomposition of an ordinary s–t flow starts at s.

theorem TauCeti.PathCycleDecomposition.target_eq_of_mem_paths {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] {cap : Assignment Q K} {s t : V} [PartialOrder K] [IsOrderedAddMonoid K] {f : Flow cap s t} (D : PathCycleDecomposition f.toFun) {p : WeightedWalk Q K} (hp : p ∈ D.paths) : p.target = t

Every path of a decomposition of an ordinary s–t flow ends at t.

theorem TauCeti.PathCycleDecomposition.sum_weight_paths_eq_val {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] {cap : Assignment Q K} {s t : V} [PartialOrder K] [IsOrderedAddMonoid K] {f : Flow cap s t} (D : PathCycleDecomposition f.toFun) : (List.map WeightedWalk.weight D.paths).sum = f.val

The path weights of a decomposition of an ordinary s–t flow add up to its value.

theorem TauCeti.PathCycleDecomposition.pathAssignment_apply_le_val {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] {cap : Assignment Q K} {s t : V} [PartialOrder K] [IsOrderedAddMonoid K] {f : Flow cap s t} (D : PathCycleDecomposition f.toFun) {x y : V} (e : Q x y) : D.pathAssignment e ≤ f.val

The path components of a decomposition of an ordinary s–t flow carry at most the value of the flow on every arrow.

theorem TauCeti.PathCycleDecomposition.sum_weight_filter_source_eq_negPart {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} (D : PathCycleDecomposition f) [DecidableEq V] (v : V) : (List.map WeightedWalk.weight (List.filter (fun (p : WeightedWalk Q K) => decide (p.source = v)) D.paths)).sum = (excessAt f v)⁻

Supply identity. The total weight of the paths starting at v is the negative part of the excess at v: minus the excess at a supply vertex, and zero elsewhere.

theorem TauCeti.PathCycleDecomposition.sum_weight_filter_target_eq_posPart {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] {f : Assignment Q K} (D : PathCycleDecomposition f) [DecidableEq V] (v : V) : (List.map WeightedWalk.weight (List.filter (fun (p : WeightedWalk Q K) => decide (p.target = v)) D.paths)).sum = (excessAt f v)⁺

Demand identity. The total weight of the paths ending at v is the positive part of the excess at v: the excess at a demand vertex, and zero elsewhere.

Existence

theorem TauCeti.exists_pathCycleDecomposition {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} (H : AddSubgroup K) (hf : 0 ≤ f) (hH : ∀ ⦃x y : V⦄ (e : Q x y), f e ∈ H) : ∃ (D : PathCycleDecomposition f), (∀ p ∈ D.paths, p.weight ∈ H) ∧ (∀ c ∈ D.cycles, c.weight ∈ H) ∧ D.paths.length + D.cycles.length ≤ {a : (x : V) × (y : V) × Q x y | 0 < f a.snd.snd}.card

Path–cycle decomposition. Every nonnegative arrow assignment f on a finite arrow family is a sum of positively weighted directed paths, each from a vertex of negative excess to a vertex of positive excess, and positively weighted directed cycles. The number of components is at most the number of arrows on which f is positive, and if the values of f lie in an additive subgroup H, then so do all weights.

theorem TauCeti.nonempty_pathCycleDecomposition {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} (hf : 0 ≤ f) : Nonempty (PathCycleDecomposition f)

Every nonnegative arrow assignment on a finite arrow family has a path–cycle decomposition.

Decompositions of assignments carrying at most one unit on every arrow

theorem TauCeti.PathCycleDecomposition.weight_eq_one_of_mem_paths {V : Type u} {Q : V → V → Type v} [Fintype V] [(x y : V) → Fintype (Q x y)] {f : Assignment Q ℤ} (D : PathCycleDecomposition f) (hf : ∀ ⦃x y : V⦄ (e : Q x y), f e ≤ 1) {p : WeightedWalk Q ℤ} (hp : p ∈ D.paths) : p.weight = 1

Every path component of a decomposition of an integer assignment carrying at most one unit on every arrow has weight one.

theorem TauCeti.PathCycleDecomposition.apply_eq_one_of_mem_arrows {V : Type u} {Q : V → V → Type v} [Fintype V] [(x y : V) → Fintype (Q x y)] {f : Assignment Q ℤ} (D : PathCycleDecomposition f) (hf : ∀ ⦃x y : V⦄ (e : Q x y), f e ≤ 1) {p : WeightedWalk Q ℤ} (hp : p ∈ D.paths) {x y : V} {e : Q x y} (he : ⟨x, ⟨y, e⟩⟩ ∈ p.walk.arrows) : f e = 1

In a decomposition of an integer assignment carrying at most one unit on every arrow, every arrow traversed by a path component carries exactly one unit.

theorem TauCeti.PathCycleDecomposition.pairwise_disjoint_arrows {V : Type u} {Q : V → V → Type v} [Fintype V] [(x y : V) → Fintype (Q x y)] {f : Assignment Q ℤ} (D : PathCycleDecomposition f) (hf : ∀ ⦃x y : V⦄ (e : Q x y), f e ≤ 1) : Pairwise fun (i j : Fin D.paths.length) => D.paths[↑i].walk.arrows.Disjoint D.paths[↑j].walk.arrows

In a decomposition of an integer assignment carrying at most one unit on every arrow, no two different path components traverse a common arrow.

theorem TauCeti.Flow.exists_paths_card_eq_val {V : Type u} {Q : V → V → Type v} [Fintype V] [(x y : V) → Fintype (Q x y)] {cap : Assignment Q ℤ} {s t : V} (f : Flow cap s t) (hf : ∀ ⦃x y : V⦄ (e : Q x y), f.toFun e ≤ 1) : ∃ (k : ℕ) (P : Fin k → ArrowWalk Q s t), ↑k = f.val ∧ (∀ (i : Fin k), (P i).IsPath) ∧ (∀ (i : Fin k), ∀ a ∈ (P i).arrows, f.toFun a.snd.snd = 1) ∧ Pairwise fun (i j : Fin k) => (P i).arrows.Disjoint (P j).arrows

An integer s–t flow carrying at most one unit on every arrow carries as many directed s–t paths as its value, no two of which traverse a common arrow: every arrow of these paths carries one unit of the flow.

theorem TauCeti.Flow.exists_paths_card_eq_val_card_filter_le {V : Type u} {Q : V → V → Type v} [Fintype V] [(x y : V) → Fintype (Q x y)] [DecidableEq V] {cap : Assignment Q ℤ} {s t : V} (f : Flow cap s t) : ∃ (k : ℕ) (P : Fin k → ArrowWalk Q s t), ↑k = f.val ∧ (∀ (i : Fin k), (P i).IsPath) ∧ ∀ (v : V), v ≠ s → ↑{i : Fin k | v ∈ (P i).vertices}.card ≤ arrowSum f.toFun Finset.univ {v}

An integer s–t flow carries a family of directed s–t paths, repetitions allowed, with as many members as its value, such that every vertex v ≠ s lies on at most as many members as the total value entering v.