Termination of label correcting (Prop. 2.3.1)

Proved

BertsekasDP.label_correcting_terminates

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

labelcorrectingtermination

Proposition 2.3.1 (termination of the label correcting method). Consider the shortest path problem of §2.3 on a finite directed graph, and assume that every cycle has nonnegative length — formally, that every closed walk $l$ from a node $v$ back to itself satisfies

\ell(l) \;\ge\; 0 .

Then the label correcting algorithm terminates: there is no infinite sequence of states $\sigma_0, \sigma_1, \sigma_2, \dots$ with $\sigma_0$ the initial state and $\sigma_{k+1}$ obtained from $\sigma_k$ by one iteration of the algorithm.

Termination is the half of Prop. 2.3.1 that survives under the weaker hypothesis: it needs only that cycles do not pay, whereas the correctness half needs nonnegative arcs. The argument in the source is a counting one — each time a node enters $\mathrm{OPEN}$ its label strictly decreases to the length of some walk from the origin, and below any given bound there are only finitely many such lengths.

Formalization Note The claim is the negation of the existence of an infinite run starting at the initial state; it does not bound the number of iterations, and it says nothing about runs started elsewhere. Because a step requires a node in $\mathrm{OPEN}$ , an infinite run would in particular keep $\mathrm{OPEN}$ nonempty forever.

Preamble

import Mathlib
import Definitions.Def_BertsekasSPGraph
import Definitions.Def_BertsekasLCState

Formal statement

namespace BertsekasDP

theorem label_correcting_terminates {V : Type} [Fintype V] [DecidableEq V]
    (G : BertsekasSPGraph V)
    (hcyc : ∀ v l, BertsekasIsWalkFrom G v v l → 0 ≤ BertsekasWalkLength G l) :
    ¬ ∃ seq : ℕ → BertsekasLCState V,
        seq 0 = BertsekasLCInit G ∧
        ∀ k, BertsekasLCStep G (seq k) (seq (k + 1)) := by sorry

end BertsekasDP

Source

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, Proposition 2.3.1 (termination 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$ . Assume (hcyc): for every vertex $v$ and every list $l$ with $\mathrm{IsWalkFrom}(G, v, v, l)$ (nonempty, consecutive pairs are arcs, first and last element both $v$ ), the walk length $\sum \ell$ over consecutive pairs is $\ge 0$ — i.e. no closed walk of $G$ has negative length. Then the theorem asserts: there is no infinite run of the algorithm, i.e. there exists no function $\sigma_\bullet : \mathbb{N} \to$ states such that

\sigma_0 = \mathrm{Init}(G) \quad\text{and}\quad \forall k \in \mathbb{N},\ \mathrm{Step}(G, \sigma_k, \sigma_{k+1}),

where $\mathrm{Init}$ and $\mathrm{Step}$ are as expanded above ( $\mathrm{Step}$ requires at each stage a vertex in the current open set, so an infinite run in particular requires every $\sigma_k$ to have a nonempty open set). The statement is a plain negation of existence of such a sequence starting at the initial state; it says nothing about runs starting from other states, and nothing about how many steps a finite run may take. The proof is left as sorry.

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