Directed walks along an explicit arrow family

A directed walk along an arrow family Q : V → V → Type* is a Mathlib Quiver.Path for the quiver whose arrows from v to w are the terms of Q v w. The quiver is supplied explicitly, as @Quiver.Path V ⟨Q⟩ s t, so that several arrow families on one vertex type, such as a network and its residual network, have their own walks without competing Quiver instances. TauCeti.ArrowWalk Q s t abbreviates this type, and the abbreviations in its namespace expose the Mathlib path operations through dot notation.

A walk records the identities of the arrows it traverses, which TauCeti.ArrowWalk.arrows lists in order with repetitions. A directed path repeats no vertex, and a directed cycle is a closed walk of positive length that repeats no vertex other than its common endpoints. Since the target of each traversed arrow is a later vertex of the walk, neither repeats an arrow; this is what bounds the value a path or cycle places on a single arrow in flow augmentation. Every walk contains a path between the same endpoints that uses only arrows of the walk, and every closed walk of positive length contains a cycle at the same vertex that uses only arrows of the walk. The bottleneck of a walk for capacities c is the least capacity of an arrow it traverses, and a vertex is positively reachable from another when some walk joins them along arrows of positive capacity; for residual capacities these are augmenting walks.

Main definitions

• TauCeti.ArrowWalk Q s t: directed walks from s to t along the arrow family Q.
• TauCeti.ArrowWalk.arrows: the arrows traversed by a walk, in order.
• TauCeti.ArrowWalk.IsPath and TauCeti.ArrowWalk.IsCycle: directed paths and cycles.
• TauCeti.Assignment.IsAcyclic: arrow assignments whose positive support contains no directed cycle.
• TauCeti.ArrowWalk.bottleneck: the least capacity along a walk that traverses an arrow.
• TauCeti.PositiveReachable c s t: some walk from s to t traverses only arrows of positive capacity for c.
• TauCeti.ReachableWithout F s t: some walk from s to t traverses no arrow of the set F of arrows, so t stays reachable from s after deleting the arrows of F.
• TauCeti.WithoutHom F: the arrow family of the arrows outside F, with its inclusion TauCeti.WithoutHom.incl F into Q.
• TauCeti.ReachableAvoiding Q X s t: some walk from s to t visits no vertex of X, so t stays reachable from s after deleting the vertices of X.
• TauCeti.ArrowWalk.InternallyDisjoint: two walks from s to t sharing no vertex other than s and t.

Main results

• TauCeti.ArrowWalk.map_target_arrows: the targets of the traversed arrows are the vertices of the walk after its first.
• TauCeti.ArrowWalk.isChain_vertices and TauCeti.ArrowWalk.exists_vertices_eq_of_isChain: the vertex sequences of walks are the lists of vertices in which consecutive vertices are joined by an arrow; TauCeti.ArrowWalk.vertices_injective shows that they determine the walk when at most one arrow runs from any vertex to any other.
• TauCeti.ArrowWalk.IsPath.nodup_arrows and TauCeti.ArrowWalk.IsCycle.nodup_arrows: paths and cycles traverse every arrow at most once.
• TauCeti.ArrowWalk.exists_isPath_arrows_subset: every walk contains a path with the same endpoints.
• TauCeti.ArrowWalk.exists_isPath_interior_notMem: every walk from a vertex of A to a vertex of B contains a path from a vertex of A to a vertex of B with no other vertex in A or B, traversing only arrows of the walk.
• TauCeti.ArrowWalk.exists_isCycle_arrows_subset: every closed walk of positive length contains a cycle.
• TauCeti.ArrowWalk.exists_eq_comp_cons_comp_of_mem_arrows: a walk that traverses a specified arrow splits at that arrow.
• TauCeti.ArrowWalk.le_bottleneck_iff and TauCeti.ArrowWalk.exists_mem_bottleneck_eq: the bottleneck is the minimum of the capacities along the walk.
• TauCeti.positiveReachable_iff_exists_isPath and TauCeti.positiveReachable_iff_reflTransGen: positive reachability is witnessed by a path, and is the reflexive transitive closure of being joined by an arrow of positive capacity; TauCeti.exists_isCycle_iff_transGen is the counterpart for cycles.
• TauCeti.Assignment.isAcyclic_iff_forall_not_transGen: an assignment is acyclic exactly when no vertex reaches itself in one or more steps along arrows of positive value.
• TauCeti.positiveReachable_iff_nonempty_arrowWalk: positive reachability is reachability along the arrow family TauCeti.PositiveHom c of arrows of positive capacity, and TauCeti.reachableWithout_iff_nonempty_arrowWalk is the counterpart for deleted arrows.
• TauCeti.PositiveReachable.mem_of_mem: a vertex set that no arrow of positive capacity leaves contains every vertex positively reachable from one of its members, and TauCeti.ReachableWithout.mem_of_mem is the counterpart for deleted arrows.
• TauCeti.positiveReachable_map_iff and TauCeti.positiveReachable_map_iff_of_strictMono: a coefficient map preserving and reflecting positivity, such as a strictly monotone map fixing zero, does not change positive reachability.

@[reducible, inline]

abbrev TauCeti.ArrowWalk {V : Type u} (Q : V → V → Type v) (s t : V) : Type (max u v)

Directed walks from s to t along the arrow family Q: Mathlib's quiver paths for the quiver with arrow types Q, supplied explicitly rather than as an instance.

@[reducible, inline]

abbrev TauCeti.ArrowWalk.nil {V : Type u} {Q : V → V → Type v} (s : V) : ArrowWalk Q s s

The walk of length zero at s.

@[reducible, inline]

abbrev TauCeti.ArrowWalk.cons {V : Type u} {Q : V → V → Type v} {s t x : V} (p : ArrowWalk Q s t) (e : Q t x) : ArrowWalk Q s x

The walk p followed by the arrow e.

@[reducible, inline]

abbrev TauCeti.ArrowWalk.comp {V : Type u} {Q : V → V → Type v} {s t x : V} (p : ArrowWalk Q s t) (p' : ArrowWalk Q t x) : ArrowWalk Q s x

The walk p followed by the walk p'.

@[reducible, inline]

abbrev TauCeti.ArrowWalk.length {V : Type u} {Q : V → V → Type v} {s t : V} (p : ArrowWalk Q s t) : ℕ

The number of arrows traversed by a walk.

@[reducible, inline]

abbrev TauCeti.ArrowWalk.vertices {V : Type u} {Q : V → V → Type v} {s t : V} (p : ArrowWalk Q s t) : List V

The vertices visited by a walk, in order, from its source to its target.

def TauCeti.ArrowWalk.arrows {V : Type u} {Q : V → V → Type v} {s t : V} : ArrowWalk Q s t → List ((x : V) × (y : V) × Q x y)

The arrows traversed by a walk, in order and with repetitions, each recorded with its endpoints.

@[simp]

theorem TauCeti.ArrowWalk.arrows_nil {V : Type u} {Q : V → V → Type v} (s : V) : (nil s).arrows = []

@[simp]

theorem TauCeti.ArrowWalk.arrows_cons {V : Type u} {Q : V → V → Type v} {s t x : V} (p : ArrowWalk Q s t) (e : Q t x) : (p.cons e).arrows = p.arrows ++ [⟨t, ⟨x, e⟩⟩]

@[simp]

theorem TauCeti.ArrowWalk.vertices_nil {V : Type u} {Q : V → V → Type v} (s : V) : (nil s).vertices = [s]

theorem TauCeti.ArrowWalk.vertices_cons {V : Type u} {Q : V → V → Type v} {s t x : V} (p : ArrowWalk Q s t) (e : Q t x) : (p.cons e).vertices = p.vertices.concat x

The vertices of p.cons e are those of p followed by x. This is not a simp lemma, since simp already rewrites its left-hand side by Quiver.Path.vertices_cons.

theorem TauCeti.ArrowWalk.vertices_mapPath_of_obj_eq_id {V : Type u} {Q : V → V → Type v} {R : V → V → Type u_1} (φ : V ⥤q V) (hφ : φ.obj = id) {s t : V} (p : ArrowWalk Q s t) : vertices (φ.mapPath p) = p.vertices

Pushing a walk along a prefunctor that is the identity on vertices keeps its vertices.

theorem TauCeti.ArrowWalk.vertices_comp {V : Type u} {Q : V → V → Type v} {s t x : V} (p : ArrowWalk Q s t) (p' : ArrowWalk Q t x) : (p.comp p').vertices = p.vertices.dropLast ++ p'.vertices

The vertices of p.comp p' are those of p without its last vertex, followed by those of p'. This is not a simp lemma, since simp already rewrites its left-hand side by Quiver.Path.vertices_comp.

theorem TauCeti.ArrowWalk.vertices_nil_cons_comp {V : Type u} {Q : V → V → Type v} {x y t : V} (e : Q x y) (p : ArrowWalk Q y t) : (((nil x).cons e).comp p).vertices = x :: p.vertices

The vertices of the walk that traverses e from x and then follows p are x followed by the vertices of p.

@[simp]

theorem TauCeti.ArrowWalk.arrows_comp {V : Type u} {Q : V → V → Type v} {s t x : V} (p : ArrowWalk Q s t) (p' : ArrowWalk Q t x) : (p.comp p').arrows = p.arrows ++ p'.arrows

@[simp]

theorem TauCeti.ArrowWalk.length_arrows {V : Type u} {Q : V → V → Type v} {s t : V} (p : ArrowWalk Q s t) : p.arrows.length = p.length

@[simp]

theorem TauCeti.ArrowWalk.arrows_eq_nil_iff {V : Type u} {Q : V → V → Type v} {s t : V} {p : ArrowWalk Q s t} : p.arrows = [] ↔ p.length = 0

theorem TauCeti.ArrowWalk.arrows_ne_nil {V : Type u} {Q : V → V → Type v} {s t : V} (p : ArrowWalk Q s t) (hst : s ≠ t) : p.arrows ≠ []

A walk between distinct vertices traverses an arrow.

theorem TauCeti.ArrowWalk.map_target_arrows {V : Type u} {Q : V → V → Type v} {s t : V} (p : ArrowWalk Q s t) : List.map (fun (a : (x : V) × (y : V) × Q x y) => a.snd.fst) p.arrows = p.vertices.tail

The targets of the arrows traversed by a walk are its vertices after the first.

theorem TauCeti.ArrowWalk.vertices_eq_cons_map_target_arrows {V : Type u} {Q : V → V → Type v} {s t : V} (p : ArrowWalk Q s t) : p.vertices = s :: List.map (fun (a : (x : V) × (y : V) × Q x y) => a.snd.fst) p.arrows

The vertices of a walk are its source followed by the targets of its arrows.

theorem TauCeti.ArrowWalk.source_mem_vertices_of_mem_arrows {V : Type u} {Q : V → V → Type v} {s t x y : V} (p : ArrowWalk Q s t) {e : Q x y} (he : ⟨x, ⟨y, e⟩⟩ ∈ p.arrows) : x ∈ p.vertices

The source of every arrow traversed by a walk is one of its vertices.

theorem TauCeti.ArrowWalk.nodup_arrows_of_nodup_tail {V : Type u} {Q : V → V → Type v} {s t : V} {p : ArrowWalk Q s t} (hp : p.vertices.tail.Nodup) : p.arrows.Nodup

A walk whose vertices after the first are distinct traverses no arrow twice.

@[simp]

theorem TauCeti.ArrowWalk.vertices_getLast? {V : Type u} {Q : V → V → Type v} {s t : V} (p : ArrowWalk Q s t) : p.vertices.getLast? = some t

A walk ends at its target.

theorem TauCeti.ArrowWalk.reverse_vertices {V : Type u} {Q : V → V → Type v} {s t : V} (p : ArrowWalk Q s t) : p.vertices.reverse = t :: Quiver.Path.toList p

Read backwards, the vertices of a walk are its target followed by Quiver.Path.toList, which lists the sources of the traversed arrows from last to first.

theorem TauCeti.ArrowWalk.isChain_vertices {V : Type u} {Q : V → V → Type v} {s t : V} (p : ArrowWalk Q s t) : List.IsChain (fun (v w : V) => Nonempty (Q v w)) p.vertices

Consecutive vertices of a walk are joined by an arrow.

theorem TauCeti.ArrowWalk.exists_vertices_eq_of_isChain {V : Type u} {Q : V → V → Type v} {l : List V} (hl : List.IsChain (fun (v w : V) => Nonempty (Q v w)) l) {s t : V} (hs : l.head? = some s) (ht : l.getLast? = some t) : ∃ (p : ArrowWalk Q s t), p.vertices = l

Every list of vertices from s to t in which consecutive vertices are joined by an arrow is the vertex sequence of a walk from s to t.

theorem TauCeti.ArrowWalk.vertices_injective {V : Type u} {Q : V → V → Type v} [∀ (v w : V), Subsingleton (Q v w)] {s t : V} : Function.Injective vertices

When at most one arrow runs from any vertex to any other, a walk is determined by its vertices.

Paths and cycles

def TauCeti.ArrowWalk.IsPath {V : Type u} {Q : V → V → Type v} {s t : V} (p : ArrowWalk Q s t) : Prop

A directed path: a walk that visits no vertex twice.

theorem TauCeti.ArrowWalk.isPath_def {V : Type u} {Q : V → V → Type v} {s t : V} (p : ArrowWalk Q s t) : p.IsPath ↔ p.vertices.Nodup

@[simp]

theorem TauCeti.ArrowWalk.isPath_nil {V : Type u} {Q : V → V → Type v} (s : V) : (nil s).IsPath

theorem TauCeti.ArrowWalk.IsPath.nodup_arrows {V : Type u} {Q : V → V → Type v} {s t : V} {p : ArrowWalk Q s t} (hp : p.IsPath) : p.arrows.Nodup

A path traverses every arrow at most once.

def TauCeti.ArrowWalk.IsCycle {V : Type u} {Q : V → V → Type v} {s : V} (c : ArrowWalk Q s s) : Prop

A directed cycle: a closed walk of positive length that visits no vertex twice, apart from its common first and last vertex. A loop is a cycle of length one.

theorem TauCeti.ArrowWalk.isCycle_def {V : Type u} {Q : V → V → Type v} {s : V} (c : ArrowWalk Q s s) : c.IsCycle ↔ 0 < c.length ∧ c.vertices.tail.Nodup

theorem TauCeti.ArrowWalk.isCycle_loop {V : Type u} {Q : V → V → Type v} {s : V} (e : Q s s) : ((nil s).cons e).IsCycle

A loop is a cycle.

theorem TauCeti.ArrowWalk.IsCycle.nodup_arrows {V : Type u} {Q : V → V → Type v} {s : V} {c : ArrowWalk Q s s} (hc : c.IsCycle) : c.arrows.Nodup

A cycle traverses every arrow at most once.

theorem TauCeti.ArrowWalk.IsCycle.arrows_ne_nil {V : Type u} {Q : V → V → Type v} {s : V} {c : ArrowWalk Q s s} (hc : c.IsCycle) : c.arrows ≠ []

A cycle traverses at least one arrow.

theorem TauCeti.ArrowWalk.IsPath.isCycle_cons {V : Type u} {Q : V → V → Type v} {s t : V} {p : ArrowWalk Q s t} (hp : p.IsPath) (e : Q t s) : (p.cons e).IsCycle

Closing a directed path by an arrow from its target to its source produces a directed cycle.

theorem TauCeti.ArrowWalk.IsPath.of_comp_left {V : Type u} {Q : V → V → Type v} {s t x : V} {p : ArrowWalk Q s t} {p' : ArrowWalk Q t x} (hp : (p.comp p').IsPath) : p.IsPath

An initial segment of a path is a path.

theorem TauCeti.ArrowWalk.IsPath.of_comp_right {V : Type u} {Q : V → V → Type v} {s t x : V} {p : ArrowWalk Q s t} {p' : ArrowWalk Q t x} (hp : (p.comp p').IsPath) : p'.IsPath

A final segment of a path is a path.

theorem TauCeti.ArrowWalk.IsPath.of_cons {V : Type u} {Q : V → V → Type v} {s t x : V} {p : ArrowWalk Q s t} {e : Q t x} (hp : (p.cons e).IsPath) : p.IsPath

The walk before the last arrow of a path is a path.

theorem TauCeti.ArrowWalk.IsPath.target_notMem_vertices_of_cons {V : Type u} {Q : V → V → Type v} {s t x : V} {p : ArrowWalk Q s t} {e : Q t x} (hp : (p.cons e).IsPath) : x ∉ p.vertices

The last vertex of a path is not a vertex of the walk before its last arrow.

theorem TauCeti.ArrowWalk.IsPath.source_ne_target_of_mem_arrows {V : Type u} {Q : V → V → Type v} {s t x y : V} {p : ArrowWalk Q s t} (hp : p.IsPath) {e : Q x y} (he : ⟨x, ⟨y, e⟩⟩ ∈ p.arrows) : x ≠ t

The source of an arrow traversed by a path is not the path's target.

theorem TauCeti.ArrowWalk.IsPath.eq_cons_of_mem_arrows {V : Type u} {Q : V → V → Type v} {s t : V} {p : ArrowWalk Q s t} (hp : p.IsPath) {e : Q s t} (he : ⟨s, ⟨t, e⟩⟩ ∈ p.arrows) : p = (nil s).cons e

A path from s to t that traverses an arrow e from s to t consists of e alone.

theorem TauCeti.ArrowWalk.exists_mem_arrows_source_mem_target_notMem {V : Type u} {Q : V → V → Type v} {C : Set V} {s t : V} (p : ArrowWalk Q s t) (hs : s ∈ C) (ht : t ∉ C) : ∃ (x : V) (y : V) (e : Q x y), ⟨x, ⟨y, e⟩⟩ ∈ p.arrows ∧ x ∈ C ∧ y ∉ C

A walk from a vertex in C to a vertex outside C traverses an arrow leaving C.

theorem TauCeti.ArrowWalk.exists_eq_comp_cons_comp_of_mem_arrows {V : Type u} {Q : V → V → Type v} {s t x y : V} {p : ArrowWalk Q s t} {e : Q x y} (he : ⟨x, ⟨y, e⟩⟩ ∈ p.arrows) : ∃ (p₁ : ArrowWalk Q s x) (p₂ : ArrowWalk Q y t), p = p₁.comp (((nil x).cons e).comp p₂)

A walk that traverses a specified arrow splits into the part before that arrow, the arrow itself, and the part after it.

theorem TauCeti.ArrowWalk.IsPath.fst_ne_of_mem_arrows {V : Type u} {Q : V → V → Type v} {s t : V} {p : ArrowWalk Q s t} (hp : p.IsPath) {a : (x : V) × (y : V) × Q x y} (ha : a ∈ p.arrows) : a.fst ≠ t

No arrow traversed by a path leaves its last vertex.

theorem TauCeti.ArrowWalk.exists_isPath_arrows_subset {V : Type u} {Q : V → V → Type v} {s t : V} (p : ArrowWalk Q s t) : ∃ (p' : ArrowWalk Q s t), p'.IsPath ∧ p'.arrows ⊆ p.arrows

Path extraction. Every walk contains a path with the same endpoints that traverses only arrows of the walk.

theorem TauCeti.ArrowWalk.vertices_subset_of_arrows_subset {V : Type u} {Q : V → V → Type v} {s t t' : V} {p : ArrowWalk Q s t} {p' : ArrowWalk Q s t'} (h : p'.arrows ⊆ p.arrows) : p'.vertices ⊆ p.vertices

A walk traversing only arrows of another walk from the same vertex visits only vertices of that walk.

theorem TauCeti.ArrowWalk.exists_isPath_vertices_subset {V : Type u} {Q : V → V → Type v} {s t : V} (p : ArrowWalk Q s t) : ∃ (p' : ArrowWalk Q s t), p'.IsPath ∧ p'.vertices ⊆ p.vertices

Every walk contains a path with the same endpoints that visits only vertices of the walk.

theorem TauCeti.ArrowWalk.exists_isPath_interior_notMem {V : Type u} {Q : V → V → Type v} {A B : Set V} {s t : V} (p : ArrowWalk Q s t) (hs : s ∈ A) (ht : t ∈ B) : ∃ a ∈ A, ∃ b ∈ B, ∃ (q : ArrowWalk Q a b), q.IsPath ∧ q.vertices ⊆ p.vertices ∧ q.arrows ⊆ p.arrows ∧ ∀ v ∈ q.vertices, v ≠ a → v ≠ b → v ∉ A ∧ v ∉ B

Trimming a walk between two vertex sets. A walk from a vertex of A to a vertex of B contains a path from a vertex a ∈ A to a vertex b ∈ B whose vertices other than a and b lie in neither A nor B, and which visits only vertices and traverses only arrows of the walk.

theorem TauCeti.ArrowWalk.exists_isCycle_arrows_subset {V : Type u} {Q : V → V → Type v} {s : V} (c : ArrowWalk Q s s) (hc : 0 < c.length) : ∃ (c' : ArrowWalk Q s s), c'.IsCycle ∧ c'.arrows ⊆ c.arrows

Cycle extraction. Every closed walk of positive length contains a cycle at the same vertex that traverses only arrows of the walk.

Bottlenecks

def TauCeti.ArrowWalk.bottleneck {V : Type u} {Q : V → V → Type v} {K : Type w} [LinearOrder K] (c : Assignment Q K) {s t : V} (p : ArrowWalk Q s t) (hne : p.arrows ≠ []) : K

The bottleneck of a walk p that traverses at least one arrow, for the capacities c: the least capacity of an arrow traversed by p.

theorem TauCeti.ArrowWalk.le_bottleneck_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [LinearOrder K] {c : Assignment Q K} {s t : V} {p : ArrowWalk Q s t} {hne : p.arrows ≠ []} {x : K} : x ≤ bottleneck c p hne ↔ ∀ a ∈ p.arrows, x ≤ c a.snd.snd

A value is at most the bottleneck exactly when it is at most every capacity along the walk.

theorem TauCeti.ArrowWalk.bottleneck_le {V : Type u} {Q : V → V → Type v} {K : Type w} [LinearOrder K] {c : Assignment Q K} {s t : V} {p : ArrowWalk Q s t} {hne : p.arrows ≠ []} {a : (x : V) × (y : V) × Q x y} (ha : a ∈ p.arrows) : bottleneck c p hne ≤ c a.snd.snd

theorem TauCeti.ArrowWalk.exists_mem_bottleneck_eq {V : Type u} {Q : V → V → Type v} {K : Type w} [LinearOrder K] {c : Assignment Q K} {s t : V} {p : ArrowWalk Q s t} {hne : p.arrows ≠ []} : ∃ a ∈ p.arrows, bottleneck c p hne = c a.snd.snd

The bottleneck is attained on an arrow traversed by the walk.

theorem TauCeti.ArrowWalk.bottleneck_mem {V : Type u} {Q : V → V → Type v} {K : Type w} [LinearOrder K] {c : Assignment Q K} {s t : V} {p : ArrowWalk Q s t} {hne : p.arrows ≠ []} {A : Set K} (h : ∀ a ∈ p.arrows, c a.snd.snd ∈ A) : bottleneck c p hne ∈ A

The bottleneck lies in every set that contains the capacities along the walk.

theorem TauCeti.ArrowWalk.lt_bottleneck_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [LinearOrder K] {c : Assignment Q K} {s t : V} {p : ArrowWalk Q s t} {hne : p.arrows ≠ []} {x : K} : x < bottleneck c p hne ↔ ∀ a ∈ p.arrows, x < c a.snd.snd

A value is below the bottleneck exactly when it is below every capacity along the walk.

theorem TauCeti.injective_of_pairwise_disjoint_arrows {V : Type u} {Q : V → V → Type v} {s t : V} (hst : s ≠ t) {ι : Type u_1} {P : ι → ArrowWalk Q s t} (hP : Pairwise fun (i j : ι) => (P i).arrows.Disjoint (P j).arrows) : Function.Injective P

An arrow-disjoint family of walks between distinct vertices has distinct members: a walk between distinct vertices traverses some arrow, which a second copy of it would share.

Reachability along arrows of positive capacity

def TauCeti.PositiveReachable {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] (c : Assignment Q K) (s t : V) : Prop

The vertex t is positively reachable from s for the capacities c when some walk from s to t traverses only arrows of positive capacity. For the residual capacities of a flow, such a walk is an augmenting walk.

theorem TauCeti.positiveReachable_def {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] {c : Assignment Q K} {s t : V} : PositiveReachable c s t ↔ ∃ (p : ArrowWalk Q s t), ∀ a ∈ p.arrows, 0 < c a.snd.snd

theorem TauCeti.positiveReachable_map_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] {c : Assignment Q K} {s t : V} {L : Type u_1} [Zero L] [LT L] {φ : K → L} (hφ : ∀ (x : K), 0 < φ x ↔ 0 < x) : PositiveReachable (c.map φ) s t ↔ PositiveReachable c s t

Positive reachability is unchanged by a coefficient map that preserves and reflects positivity.

@[simp]

theorem TauCeti.PositiveReachable.refl {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] (c : Assignment Q K) (s : V) : PositiveReachable c s s

theorem TauCeti.PositiveReachable.tail {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] {c : Assignment Q K} {s t x : V} (h : PositiveReachable c s t) (e : Q t x) (he : 0 < c e) : PositiveReachable c s x

A positively reachable vertex stays reachable along a further arrow of positive capacity.

theorem TauCeti.PositiveReachable.single {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] {c : Assignment Q K} {s t : V} (e : Q s t) (he : 0 < c e) : PositiveReachable c s t

The head of an arrow of positive capacity is positively reachable from its tail.

theorem TauCeti.PositiveReachable.trans {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] {c : Assignment Q K} {s t x : V} (h : PositiveReachable c s t) (h' : PositiveReachable c t x) : PositiveReachable c s x

theorem TauCeti.positiveReachable_of_mem_arrows {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] {c : Assignment Q K} {s t : V} {p : ArrowWalk Q s t} (hp : ∀ a ∈ p.arrows, 0 < c a.snd.snd) {a : (x : V) × (y : V) × Q x y} (ha : a ∈ p.arrows) : PositiveReachable c s a.snd.fst

The target of every arrow on a walk from s along arrows of positive capacity is positively reachable from s.

theorem TauCeti.positiveReachable_iff_exists_isPath {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] {c : Assignment Q K} {s t : V} : PositiveReachable c s t ↔ ∃ (p : ArrowWalk Q s t), p.IsPath ∧ ∀ a ∈ p.arrows, 0 < c a.snd.snd

Positive reachability is witnessed by a path.

theorem TauCeti.positiveReachable_iff_reflTransGen {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] {c : Assignment Q K} {s t : V} : PositiveReachable c s t ↔ Relation.ReflTransGen (fun (v w : V) => ∃ (e : Q v w), 0 < c e) s t

Positive reachability is the reflexive transitive closure of being joined by an arrow of positive capacity.

theorem TauCeti.exists_isCycle_iff_transGen {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] {c : Assignment Q K} {v : V} : (∃ (p : ArrowWalk Q v v), p.IsCycle ∧ ∀ a ∈ p.arrows, 0 < c a.snd.snd) ↔ Relation.TransGen (fun (v w : V) => ∃ (e : Q v w), 0 < c e) v v

Cycles of positive arrows. Some cycle at v traverses only arrows of positive capacity exactly when v reaches itself in one or more steps along arrows of positive capacity.

def TauCeti.Assignment.IsAcyclic {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] (f : Assignment Q K) : Prop

An arrow assignment is acyclic when no directed cycle traverses only arrows of positive value.

theorem TauCeti.Assignment.isAcyclic_def {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] (f : Assignment Q K) : f.IsAcyclic ↔ ∀ ⦃v : V⦄ (c : ArrowWalk Q v v), c.IsCycle → ¬∀ a ∈ c.arrows, 0 < f a.snd.snd

theorem TauCeti.Assignment.isAcyclic_iff_forall_not_transGen {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] (f : Assignment Q K) : f.IsAcyclic ↔ ∀ (v : V), ¬Relation.TransGen (fun (v w : V) => ∃ (e : Q v w), 0 < f e) v v

An assignment is acyclic exactly when no vertex reaches itself in one or more steps along arrows of positive value.

@[reducible, inline]

abbrev TauCeti.PositiveHom {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] (c : Assignment Q K) (v w : V) : Type v

The arrows of positive capacity for c, retaining their identities: the arrow family of the part of Q along which positive reachability travels.

theorem TauCeti.positiveReachable_iff_nonempty_arrowWalk {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] {c : Assignment Q K} {s t : V} : PositiveReachable c s t ↔ Nonempty (ArrowWalk (PositiveHom c) s t)

Positive reachability is reachability along the arrows of positive capacity.

theorem TauCeti.PositiveReachable.mem_of_mem {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] {c : Assignment Q K} {s t : V} {C : Set V} (h : PositiveReachable c s t) (hs : s ∈ C) (hC : ∀ ⦃v w : V⦄ (e : Q v w), v ∈ C → 0 < c e → w ∈ C) : t ∈ C

A vertex set that no arrow of positive capacity leaves is closed under positive reachability.

theorem TauCeti.positiveReachable_map_iff_of_strictMono {V : Type u} {Q : V → V → Type v} {K : Type u_1} {L : Type u_2} [Zero K] [LinearOrder K] [Zero L] [Preorder L] {c : Assignment Q K} {φ : K → L} (hφ : StrictMono φ) (hφ₀ : φ 0 = 0) {s t : V} : PositiveReachable (c.map φ) s t ↔ PositiveReachable c s t

Positive reachability is unchanged by a strictly monotone coefficient map fixing zero.

theorem TauCeti.exists_isPath_of_isAcyclic {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LinearOrder K] [Finite V] {f : Assignment Q K} (hf : 0 ≤ f) (hacyc : f.IsAcyclic) {x y : V} (e : Q x y) (he : 0 < f e) : ∃ (s : V) (t : V) (p : ArrowWalk Q s t), p.IsPath ∧ s ≠ t ∧ (∀ a ∈ p.arrows, 0 < f a.snd.snd) ∧ (∀ (w : V) (e : Q w s), f e = 0) ∧ ∀ (w : V) (e : Q t w), f e = 0

If no vertex reaches itself along positive arrows and some arrow is positive, there is a positive path between distinct vertices, with no positive arrow entering its initial vertex and no positive arrow leaving its final vertex.

Reachability after deleting arrows

def TauCeti.ReachableWithout {V : Type u} {Q : V → V → Type v} (F : Set ((x : V) × (y : V) × Q x y)) (s t : V) : Prop

The vertex t is reachable from s without the arrows of F when some walk from s to t traverses no arrow of F: reachability after deleting the arrows of F, which are identified in the total arrow type, so that parallel arrows are deleted separately.

theorem TauCeti.reachableWithout_def {V : Type u} {Q : V → V → Type v} {F : Set ((x : V) × (y : V) × Q x y)} {s t : V} : ReachableWithout F s t ↔ ∃ (p : ArrowWalk Q s t), ∀ a ∈ p.arrows, a ∉ F

@[simp]

theorem TauCeti.reachableWithout_empty_iff {V : Type u} {Q : V → V → Type v} {s t : V} : ReachableWithout ∅ s t ↔ Nonempty (ArrowWalk Q s t)

Deleting no arrows, reachability is the existence of a walk.

@[simp]

theorem TauCeti.ReachableWithout.refl {V : Type u} {Q : V → V → Type v} (F : Set ((x : V) × (y : V) × Q x y)) (s : V) : ReachableWithout F s s

theorem TauCeti.ReachableWithout.tail {V : Type u} {Q : V → V → Type v} {F : Set ((x : V) × (y : V) × Q x y)} {s t x : V} (h : ReachableWithout F s t) (e : Q t x) (he : ⟨t, ⟨x, e⟩⟩ ∉ F) : ReachableWithout F s x

A reachable vertex stays reachable along a further arrow outside F.

theorem TauCeti.ReachableWithout.trans {V : Type u} {Q : V → V → Type v} {F : Set ((x : V) × (y : V) × Q x y)} {s t x : V} (h : ReachableWithout F s t) (h' : ReachableWithout F t x) : ReachableWithout F s x

theorem TauCeti.ReachableWithout.mono {V : Type u} {Q : V → V → Type v} {F G : Set ((x : V) × (y : V) × Q x y)} {s t : V} (hFG : F ⊆ G) (h : ReachableWithout G s t) : ReachableWithout F s t

Deleting fewer arrows preserves reachability.

theorem TauCeti.reachableWithout_iff_exists_isPath {V : Type u} {Q : V → V → Type v} {F : Set ((x : V) × (y : V) × Q x y)} {s t : V} : ReachableWithout F s t ↔ ∃ (p : ArrowWalk Q s t), p.IsPath ∧ ∀ a ∈ p.arrows, a ∉ F

Reachability after deleting arrows is witnessed by a path.

theorem TauCeti.ReachableWithout.mem_of_mem {V : Type u} {Q : V → V → Type v} {F : Set ((x : V) × (y : V) × Q x y)} {s t : V} {C : Set V} (h : ReachableWithout F s t) (hs : s ∈ C) (hC : ∀ ⦃v w : V⦄ (e : Q v w), v ∈ C → ⟨v, ⟨w, e⟩⟩ ∉ F → w ∈ C) : t ∈ C

A vertex set that no arrow outside F leaves contains every vertex reachable without the arrows of F from one of its members.

@[reducible, inline]

abbrev TauCeti.WithoutHom {V : Type u} {Q : V → V → Type v} (F : Set ((x : V) × (y : V) × Q x y)) (v w : V) : Type v

The arrows outside F, retaining their identities: the arrow family of Q with the arrows of F deleted, along which reachability without the arrows of F travels.

@[reducible, inline]

abbrev TauCeti.WithoutHom.incl {V : Type u} {Q : V → V → Type v} (F : Set ((x : V) × (y : V) × Q x y)) : V ⥤q V

The inclusion of the arrows outside F into the arrow family Q.

theorem TauCeti.WithoutHom.exists_mapPath_incl_eq {V : Type u} {Q : V → V → Type v} {F : Set ((x : V) × (y : V) × Q x y)} {s t : V} (p : ArrowWalk Q s t) (hp : ∀ a ∈ p.arrows, a ∉ F) : ∃ (p' : ArrowWalk (WithoutHom F) s t), (incl F).mapPath p' = p

A walk traversing no arrow of F is the image of a walk along the arrows outside F.

theorem TauCeti.reachableWithout_iff_nonempty_arrowWalk {V : Type u} {Q : V → V → Type v} {F : Set ((x : V) × (y : V) × Q x y)} {s t : V} : ReachableWithout F s t ↔ Nonempty (ArrowWalk (WithoutHom F) s t)

Reachability without the arrows of F is reachability along the arrows outside F.

Reachability avoiding a vertex set

theorem TauCeti.ArrowWalk.exists_mem_vertices_ne_ne {V : Type u} {Q : V → V → Type v} {s t : V} (hst : s ≠ t) (hadj : IsEmpty (Q s t)) (p : ArrowWalk Q s t) : ∃ v ∈ p.vertices, v ≠ s ∧ v ≠ t

A walk between distinct vertices s and t, with no arrow from s to t, visits a vertex other than s and t.

def TauCeti.ReachableAvoiding {V : Type u} (Q : V → V → Type v) (X : Set V) (s t : V) : Prop

The vertex t is reachable from s avoiding X when some walk from s to t visits no vertex of X: reachability after deleting the vertices of X. In particular neither endpoint lies in X.

theorem TauCeti.reachableAvoiding_def {V : Type u} {Q : V → V → Type v} {X : Set V} {s t : V} : ReachableAvoiding Q X s t ↔ ∃ (p : ArrowWalk Q s t), ∀ v ∈ p.vertices, v ∉ X

theorem TauCeti.ReachableAvoiding.source_notMem {V : Type u} {Q : V → V → Type v} {X : Set V} {s t : V} (h : ReachableAvoiding Q X s t) : s ∉ X

theorem TauCeti.ReachableAvoiding.target_notMem {V : Type u} {Q : V → V → Type v} {X : Set V} {s t : V} (h : ReachableAvoiding Q X s t) : t ∉ X

theorem TauCeti.ReachableAvoiding.refl {V : Type u} {Q : V → V → Type v} {X : Set V} {s : V} (hs : s ∉ X) : ReachableAvoiding Q X s s

@[simp]

theorem TauCeti.reachableAvoiding_self_iff {V : Type u} {Q : V → V → Type v} {X : Set V} {s : V} : ReachableAvoiding Q X s s ↔ s ∉ X

theorem TauCeti.ReachableAvoiding.trans {V : Type u} {Q : V → V → Type v} {X : Set V} {s t x : V} (h : ReachableAvoiding Q X s t) (h' : ReachableAvoiding Q X t x) : ReachableAvoiding Q X s x

theorem TauCeti.ReachableAvoiding.tail {V : Type u} {Q : V → V → Type v} {X : Set V} {s t x : V} (h : ReachableAvoiding Q X s t) (e : Q t x) (hx : x ∉ X) : ReachableAvoiding Q X s x

A reachable vertex stays reachable along a further arrow to a vertex outside X.

theorem TauCeti.ReachableAvoiding.mem_of_mem {V : Type u} {Q : V → V → Type v} {X : Set V} {s t : V} {C : Set V} (h : ReachableAvoiding Q X s t) (hs : s ∈ C) (hC : ∀ ⦃v w : V⦄ (a : Q v w), v ∈ C → v ∉ X → w ∉ X → w ∈ C) : t ∈ C

A vertex set that no arrow between vertices outside X leaves contains every vertex reachable avoiding X from one of its members.

theorem TauCeti.ReachableAvoiding.withoutHom {V : Type u} {Q : V → V → Type v} {X : Set V} {s t : V} {F : Set ((x : V) × (y : V) × Q x y)} (h : ReachableAvoiding Q X s t) (hF : ∀ a ∈ F, a.fst ∈ X ∨ a.snd.fst ∈ X) : ReachableAvoiding (WithoutHom F) X s t

Deleting arrows with an endpoint in X does not change reachability avoiding X.

theorem TauCeti.ReachableAvoiding.mono {V : Type u} {Q : V → V → Type v} {X Y : Set V} {s t : V} (hXY : X ⊆ Y) (h : ReachableAvoiding Q Y s t) : ReachableAvoiding Q X s t

Avoiding fewer vertices preserves reachability.

@[simp]

theorem TauCeti.reachableAvoiding_empty_iff {V : Type u} {Q : V → V → Type v} {s t : V} : ReachableAvoiding Q ∅ s t ↔ Nonempty (ArrowWalk Q s t)

Avoiding no vertices, reachability is the existence of a walk.

Internally disjoint walks

def TauCeti.ArrowWalk.InternallyDisjoint {V : Type u} {Q : V → V → Type v} {s t : V} (p q : ArrowWalk Q s t) : Prop

Two walks from s to t are internally disjoint when they share no vertex other than s and t.

theorem TauCeti.ArrowWalk.internallyDisjoint_def {V : Type u} {Q : V → V → Type v} {s t : V} {p q : ArrowWalk Q s t} : p.InternallyDisjoint q ↔ ∀ v ∈ p.vertices, v ∈ q.vertices → v = s ∨ v = t

theorem TauCeti.ArrowWalk.InternallyDisjoint.symm {V : Type u} {Q : V → V → Type v} {s t : V} {p q : ArrowWalk Q s t} (h : p.InternallyDisjoint q) : q.InternallyDisjoint p

theorem TauCeti.ArrowWalk.internallyDisjoint_comm {V : Type u} {Q : V → V → Type v} {s t : V} {p q : ArrowWalk Q s t} : p.InternallyDisjoint q ↔ q.InternallyDisjoint p

theorem TauCeti.injective_of_pairwise_internallyDisjoint {V : Type u} {Q : V → V → Type v} {s t : V} {ι : Type u_1} {P : ι → ArrowWalk Q s t} (hP : Pairwise fun (i j : ι) => (P i).InternallyDisjoint (P j)) (h : ∀ (i : ι), ∃ v ∈ (P i).vertices, v ≠ s ∧ v ≠ t) : Function.Injective P

A family of pairwise internally disjoint walks from s to t, each visiting a vertex other than s and t, has distinct members: such a vertex would be shared by two copies of a walk.