Incidence balance of a simple path

Proved

EdmondsKarp.ShortestPath.pathArcs_incidence

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

graph-theorynetwork-flow

For any simple vertex list, any vertex u, and any real weight r, the total weight of path arcs leaving u minus the total weight entering u is r at the first vertex, minus r at the last vertex, and zero elsewhere.

Preamble

import Definitions.Def_EdmondsKarp_ShortestPath_Augmentation
open EdmondsKarp.ShortestPath

Formal statement

theorem EdmondsKarp.ShortestPath.pathArcs_incidence {V : Type} [Fintype V] [DecidableEq V] (P : List V)
    (hP : P.Nodup) (u : V) (r : ℝ) :
    (∑ v : V, if (u, v) ∈ pathArcs P then r else 0) -
      (∑ v : V, if (v, u) ∈ pathArcs P then r else 0) =
    (if P.head? = some u then r else 0) - (if P.getLast? = some u then r else 0) := by sorry

Source

Edmonds and Karp (1972), §1.1 p. 249, preservation of node balances under path augmentation. Auxiliary finite-list identity. DOI: 10.1145/321694.321699.

View graph