Labels are walk lengths (invariant)

Proved

BertsekasDP.label_correcting_invariant

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

invariantlabelcorrecting

The label invariant of the label correcting method (Bertsekas, Vol. I, §2.3.1, stated in the text preceding Prop. 2.3.1). At every state $\sigma$ reachable from the initial state — after any number of iterations, with any removal order — the labels are not arbitrary numbers but lengths of actual walks:

for every node $j$ , either $d_j = +\infty$ , or there is a walk $l$ from the origin $s$ to $j$ with

d_j \;=\; \ell(l);

either $\mathrm{UPPER} = +\infty$ , or there is a walk $l$ from $s$ to the destination $t$ with $\mathrm{UPPER} = \ell(l)$ .

Neither claim asserts optimality: the exhibited walk need not be shortest. What the invariant provides is the " $\ge$ " half of correctness — since $\mathrm{UPPER}$ is always the length of some genuine $s \to t$ walk, it can never fall below $\operatorname{dist}(s,t)$ — and it is also the engine of the termination argument, which counts the possible label values.

Formalization Note No hypothesis on arc or cycle lengths is needed here; the invariant holds for arbitrary real lengths. In the second disjunct the label is a coerced real number, so the statement also records that a non-infinite label is finite (never $-\infty$ ). For $j = s$ the one-element walk $(s)$ , of length $0$ , is among the witnesses.

Preamble

import Mathlib
import Definitions.Def_BertsekasSPGraph
import Definitions.Def_BertsekasLCState

Formal statement

namespace BertsekasDP

theorem label_correcting_invariant {V : Type} [Fintype V] [DecidableEq V]
    (G : BertsekasSPGraph V) (σ : BertsekasLCState V)
    (hreach : Relation.ReflTransGen (BertsekasLCStep G) (BertsekasLCInit G) σ) :
    (∀ j : V, σ.label j = ⊤ ∨
      ∃ l, BertsekasIsWalkFrom G G.s j l ∧
        σ.label j = (BertsekasWalkLength G l : EReal)) ∧
    (σ.upper = ⊤ ∨
      ∃ l, BertsekasIsWalkFrom G G.s G.t l ∧
        σ.upper = (BertsekasWalkLength G l : EReal)) := by sorry

end BertsekasDP

Source

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, Section 2.3.1 (in-text invariant)

Read-back

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

Let $V$ be any finite type with decidable equality, $G$ any BertsekasSPGraph on $V$ (origin $s$ , destination $t$ ), and $\sigma$ any state reachable from $\mathrm{Init}(G)$ by the reflexive–transitive closure of $\mathrm{Step}(G, \cdot, \cdot)$ (zero or more steps; the zero-step case $\sigma = \mathrm{Init}(G)$ is included). No assumption about cycle lengths is made in this theorem. The conclusion is a conjunction of two statements:

For every vertex $j \in V$ : either $\sigma.\mathrm{label}(j) = +\infty$ , or there exists a list $l$ with $\mathrm{IsWalkFrom}(G, s, j, l)$ (nonempty, consecutive pairs are arcs, starting at $s$ , ending at $j$ ) such that

\sigma.\mathrm{label}(j) = \big(\mathrm{WalkLength}(G, l)\big) \in \overline{\mathbb{R}},

the right-hand side being the coercion of a real number, so the second disjunct entails that the label is a finite value (neither $+\infty$ nor $-\infty$ ). (For $j = s$ the singleton walk $[s]$ , of length $0$ , is among the candidate witnesses.) The disjunction is inclusive and asserts nothing about which walk is exhibited — not that it is shortest, only that some walk from $s$ to $j$ has exactly the label's value as its length.

Either $\sigma.\mathrm{upper} = +\infty$ , or there exists a list $l$ with $\mathrm{IsWalkFrom}(G, s, t, l)$ such that $\sigma.\mathrm{upper} = \big(\mathrm{WalkLength}(G, l)\big)$ , again with no claim of optimality — only that the upper value is the exact length of some actual walk from $s$ to $t$ .

The theorem says nothing about the open set of $\sigma$ and does not relate labels to the upper value or to shortest distances. 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