Directed walks, unsplittable loads, and Goemans' cost conjecture

def GoemansFlow.IsWalk {W E : Type} (tail head : E → W) : W → List E → W → Prop

IsWalk tail head x l y: the list of arcs l, read left to right, is a walk from vertex x to vertex y. Repeated vertices and arcs are permitted.

Equations

• GoemansFlow.IsWalk tail head x✝¹ [] x✝ = (x✝¹ = x✝)
• GoemansFlow.IsWalk tail head x✝¹ (e :: l) x✝ = (tail e = x✝¹ ∧ GoemansFlow.IsWalk tail head (head e) l x✝)

@[simp]

theorem GoemansFlow.IsWalk_nil {W E : Type} (tail head : E → W) (x y : W) : IsWalk tail head x [] y ↔ x = y

@[simp]

theorem GoemansFlow.IsWalk_cons {W E : Type} (tail head : E → W) (x : W) (e : E) (l : List E) (y : W) : IsWalk tail head x (e :: l) y ↔ tail e = x ∧ IsWalk tail head (head e) l y

def GoemansFlow.walkBool {W E : Type} [DecidableEq W] (tail head : E → W) : W → List E → W → Bool

Boolean decision procedure for IsWalk (kernel-friendly).

Equations

• GoemansFlow.walkBool tail head x✝¹ [] x✝ = decide (x✝¹ = x✝)
• GoemansFlow.walkBool tail head x✝¹ (e :: l) x✝ = (decide (tail e = x✝¹) && GoemansFlow.walkBool tail head (head e) l x✝)

theorem GoemansFlow.walkBool_iff {W E : Type} [DecidableEq W] (tail head : E → W) (x : W) (l : List E) (y : W) : walkBool tail head x l y = true ↔ IsWalk tail head x l y

@[instance_reducible]

instance GoemansFlow.instDecidableIsWalk {W E : Type} [DecidableEq W] (tail head : E → W) (x : W) (l : List E) (y : W) : Decidable (IsWalk tail head x l y)

Equations

• GoemansFlow.instDecidableIsWalk tail head x l y = decidable_of_iff (GoemansFlow.walkBool tail head x l y = true) ⋯

def GoemansFlow.unsplittableLoad {R K E : Type} [AddCommMonoid R] [Fintype K] [DecidableEq E] (d : K → R) (P : K → List E) (a : E) : R

Load induced on arc a by routing P with demands d, counting every traversal. For arc-simple paths this is the sum of demands of commodities whose path contains a.

Equations

• GoemansFlow.unsplittableLoad d P a = ∑ k : K, List.count a (P k) • d k

theorem GoemansFlow.unsplittableLoad_eq_sum_of_nodup {R K E : Type} [AddCommMonoid R] [Fintype K] [DecidableEq E] (d : K → R) (P : K → List E) (a : E) (h : ∀ (k : K), (P k).Nodup) : unsplittableLoad d P a = ∑ k : K, if a ∈ P k then d k else 0

On arc-simple paths, traversal-counting load agrees with the membership formula.

def GoemansFlow.GoemansCostConjectureFull (R : Type) [CommRing R] [LinearOrder R] : Prop

Goemans' cost conjecture (Conjecture 1.3 of arXiv:2308.02651), restricted to simple, loopless, acyclic digraphs, with explicit capacities and strictly positive demands.

A refutation of this restricted form also refutes the conjecture over general digraphs. The conclusion allows arbitrary walks; the counterexample proves that every admissible walk is a simple path. The coefficient ring is generic, with the rational case matching the source's setting.

Equations

• One or more equations did not get rendered due to their size.