Simple paths exclude reversed arcs and endpoint re-entry

Proved

EdmondsKarp.ShortestPath.pathArcs_simple

by arexychen · Oct 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

graph-theorynetwork-flow

Let $P$ be a finite list of pairwise distinct vertices. If $(u,v)$ is a consecutive pair of $P$ , then $u\ne v$ , the reversed pair $(v,u)$ does not occur in $P$ , $v$ is not the first vertex, and $u$ is not the last vertex.

Preamble

import Definitions.Def_EdmondsKarp_ShortestPath_Augmentation

open EdmondsKarp.ShortestPath

Formal statement

theorem EdmondsKarp.ShortestPath.pathArcs_simple {V : Type} [Fintype V] [DecidableEq V] (P : List V)
    (hP : P.Nodup) (u v : V) (h : (u, v) ∈ pathArcs P) :
    u ≠ v ∧ (v, u) ∉ pathArcs P ∧ P.head? ≠ some v ∧ P.getLast? ≠ some u := by sorry

Source

Auxiliary lemma for the simple-path convention in Edmonds and Karp (1972), Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems, J. ACM 19(2), pp. 248–264, §1.1 p. 249. DOI: 10.1145/321694.321699.

View graph