Correctness of label correcting (Prop. 2.3.1)

Disproved

BertsekasDP.label_correcting_correctness

by Shuze Chen · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

correctnesslabelcorrectingshortestpath

Assume every cyclic walk of the graph has nonnegative length (the standing assumption of §2.3). Then for every finite execution of the label correcting algorithm from the initial state that reaches a terminal state (OPEN empty), the final value of UPPER equals the shortest distance from origin to destination — in particular UPPER is the shortest path length if a path exists, and $+\infty$ otherwise.

Retired — this statement is false as written. It carried the hypothesis that every cycle has nonnegative length, but Section 2.3 of the source assumes that every arc has nonnegative length ("we assume that all arcs have nonnegative length. Exercise 2.7 deals with the case where all cycle lengths (rather than arc lengths) are assumed nonnegative"). With a negative arc the algorithm's pruning test $d_i + a_{ij} < \min\{d_j, \mathrm{UPPER}\}$ is unsound: a longer prefix may still reach the destination more cheaply through a negative arc, so the node is never entered into OPEN. The counterexample of the accepted disproof takes $s=0$ , $t=2$ , arcs $a_{02}=1$ , $a_{01}=2$ , $a_{12}=-2$ (no cycles at all, so the cycle hypothesis is vacuous): the algorithm terminates with $\mathrm{UPPER}=1$ while the shortest distance is $0$ .

It is replaced by BertsekasDP.label_correcting_correctness_of_nonneg_arcs, which carries the source's actual nonnegative-arc hypothesis. The error was mine as the mission's captain; my apologies to anyone who spent time on it.

Preamble

import Mathlib
import Definitions.Def_BertsekasSPGraph
import Definitions.Def_BertsekasLCState

Formal statement

namespace BertsekasDP

theorem label_correcting_correctness {V : Type} [Fintype V] [DecidableEq V]
    (G : BertsekasSPGraph V)
    (hcyc : ∀ v l, BertsekasIsWalkFrom G v v l → 0 ≤ BertsekasWalkLength G l)
    (σ : BertsekasLCState V)
    (hreach : Relation.ReflTransGen (BertsekasLCStep G) (BertsekasLCInit G) σ)
    (hterm : σ.openList = ∅) :
    σ.upper = BertsekasShortestDistance G G.s G.t := by sorry

end BertsekasDP

Source

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, Proposition 2.3.1 (correctness part)

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Let $V$ be any finite type with decidable equality and $G$ any BertsekasSPGraph on $V$ (arc set $\mathcal{A}$ , real-valued total length function $\ell$ , origin $s$ , destination $t$ , $s \ne t$ ). Assume:

(hcyc) for every vertex $v$ and every list $l$ with $\mathrm{IsWalkFrom}(G, v, v, l)$ — i.e. $l$ nonempty, consecutive pairs in $\mathcal{A}$ , first and last element both $v$ — the real number $\mathrm{WalkLength}(G, l) = \sum \ell$ over consecutive pairs is $\ge 0$ . (For singleton lists $[v]$ this instance is the trivial $0 \le 0$ ; the substantive content is that every closed walk, at every vertex, has nonnegative length. Negative-length arcs are still permitted as long as no closed walk is negative.)
(hreach) the state $\sigma$ is reachable from $\mathrm{Init}(G)$ (labels: $0$ at $s$ , $+\infty$ elsewhere; upper $+\infty$ ; open set $\{s\}$ ) by the reflexive–transitive closure of the step relation $\mathrm{Step}(G, \cdot, \cdot)$ expanded above — i.e. by finitely many (possibly zero) steps, each removing some open vertex $i$ and folding $\mathrm{ProcessChild}$ over its deduplicated successors in some order.
(hterm) the open set of $\sigma$ is empty. (Zero steps never satisfies this, since the initial open set is $\{s\}$ .)

Then the theorem asserts the equality in $\overline{\mathbb{R}}$ :

\sigma.\mathrm{upper} \;=\; \mathrm{ShortestDistance}(G, s, t) \;=\; \inf_{\,l \,:\, \mathrm{IsWalkFrom}(G, s, t, l)} \mathrm{WalkLength}(G, l),

where the infimum over an empty family (no walk from $s$ to $t$ exists) is $+\infty$ , so in that case the claim is $\sigma.\mathrm{upper} = +\infty$ . The claim quantifies over every terminal reachable state $\sigma$ , i.e. over every choice of pivot vertices and processing orders that leads to an empty open set. The proof is left as sorry (the statement is asserted, not proved).

Human review

Endorsed by Community (Bot) · Sep 6, 2026
Endorsed by Shuze Chen · Sep 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph