Label correcting correctness under nonnegative arc lengths (Bertsekas Prop. 2.3.1)

Proved

BertsekasDP.label_correcting_correctness_of_nonneg_arcs

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

correctnessdynamic-programminglabelcorrectingshortestpath

Proposition 2.3.1 (correctness of the label correcting method). Consider the shortest path problem of §2.3 on a finite directed graph with origin $s$ and destination $t$ , under the standing assumption of that section:

a_{ij} \;\ge\; 0 \qquad \text{for every arc } (i,j) \in \mathcal{A}.

Run the label correcting algorithm from its initial state ( $d_s = 0$ , all other labels $+\infty$ , $\mathrm{UPPER} = +\infty$ , $\mathrm{OPEN} = \{s\}$ ), with the node removed from $\mathrm{OPEN}$ and the order of child processing chosen arbitrarily at every iteration. Then for every execution that terminates, i.e. every reachable state $\sigma$ with $\sigma.\mathrm{OPEN} = \varnothing$ ,

\sigma.\mathrm{UPPER} \;=\; \operatorname{dist}(s,t) \;\in\; \overline{\mathbb{R}}.

In particular $\mathrm{UPPER}$ is the shortest path length when a path from $s$ to $t$ exists, and $+\infty$ when none does.

The nonnegative arc hypothesis is essential, not a formalization artifact. Step 2 prunes a child whenever $d_i + a_{ij} \ge \mathrm{UPPER}$ , which is sound only if no suffix from $j$ to $t$ can have negative length. With a negative arc the pruning discards a node that lies on a cheaper route: for arcs $a_{02} = 1$ , $a_{01} = 2$ , $a_{12} = -2$ — a graph with no cycles at all — the run terminates with $\mathrm{UPPER} = 1$ while $\operatorname{dist}(0,2) = 0$ . Exercise 2.7 of the source treats the case where only cycle lengths are assumed nonnegative; that case calls for a modified algorithm.

Formalization Note The statement quantifies over every terminal state reachable by the nondeterministic step relation, so it certifies every removal discipline and every child-processing order simultaneously. The conclusion is an equation in EReal, so the no-path case is the genuine empty infimum $+\infty$ .

Preamble

import Mathlib
import Definitions.Def_BertsekasSPGraph
import Definitions.Def_BertsekasLCState

Formal statement

namespace BertsekasDP

theorem label_correcting_correctness_of_nonneg_arcs {V : Type} [Fintype V] [DecidableEq V]
    (G : BertsekasSPGraph V)
    (hnn : ∀ i j, (i, j) ∈ G.arcs → 0 ≤ G.length i j)
    (σ : 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), Section 2.3.1 Label Correcting Methods, under the nonnegative arc length assumption; cf. MIT 6.231 lecture notes (Bertsekas, Fall 2015), slide 'Label Correcting Methods' ('lengths a_ij >= 0'), and the Vol. I solutions manual, Exercise 2.6 ('in view of the nonnegative arc length assumption')

View graph