Rollout under sequential consistency (Prop. 6.4.1)

Proved

BertsekasDP.rollout_sequential_consistency

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

rollouttermination

Proposition 6.4.1 (termination and improvement under sequential consistency). Let the base heuristic $\mathcal{H}$ be sequentially consistent, and run the rollout algorithm with the source's tie-breaking convention: when several neighbors attain $\min_{j \in N(i)} H(j)$ and one of them is the successor that $\mathcal{H}$ itself would take from $i$ , that one is chosen. Then:

The rollout terminates: the run reaches a destination node after finitely many steps.
It improves on the base heuristic: at any time $K$ at which a destination is reached,

H(i_K) \;\le\; H(i_1), \qquad H(i_K) \;=\; \min\Bigl\{\, H(i_1), \; \min_{j \in N(i_1)} H(j), \; \dots, \; \min_{j \in N(i_{K-1})} H(j) \,\Bigr\}.

The tie-breaking convention is not a technicality: the source exhibits a graph in which, with ties broken the other way, the rollout cycles forever without reaching a destination. Sequential consistency makes the $H$ -values along the run non-increasing, and each plateau shortens the base heuristic's remaining path by one arc, which is what forces termination.

Formalization Note The run is modeled as an infinite sequence that obeys the selection rule while at a non-destination node and stays put once at a destination, so "terminates" is the genuine claim that some index lands in the destination set, rather than an assumption built into the shape of the object. The cost claim is stated for every such index. As in Prop. 6.4.2, the minimum is phrased as a least element, asserting attainment as well as the bound.

Preamble

import Mathlib
import Definitions.Def_BertsekasGraphSearch

Formal statement

namespace BertsekasDP

theorem rollout_sequential_consistency {V : Type} [Fintype V] [DecidableEq V]
    (G : BertsekasGraphSearch V) (H : BertsekasBaseHeuristic G)
    (hcons : BertsekasSeqConsistent G H)
    (r : ℕ → V) (hstart : r 0 ∉ G.dest)
    (hstep : ∀ k, r k ∉ G.dest →
      r (k + 1) ∈ BertsekasNbrs G (r k) ∧
      (∀ j ∈ BertsekasNbrs G (r k),
        BertsekasHeurCost G H (r (k + 1)) ≤ BertsekasHeurCost G H j))
    (htie : ∀ k, r k ∉ G.dest → ∀ (jH : V) (l : List V),
      H.path (r k) = r k :: jH :: l →
      (∀ j ∈ BertsekasNbrs G (r k),
        BertsekasHeurCost G H jH ≤ BertsekasHeurCost G H j) →
      r (k + 1) = jH)
    (habsorb : ∀ k, r k ∈ G.dest → r (k + 1) = r k) :
    (∃ K, r K ∈ G.dest) ∧
    (∀ K, r K ∈ G.dest →
      BertsekasHeurCost G H (r K) ≤ BertsekasHeurCost G H (r 0) ∧
      IsLeast {c : ℝ | c = BertsekasHeurCost G H (r 0) ∨
          ∃ k < K, r k ∉ G.dest ∧
            ∃ j ∈ BertsekasNbrs G (r k), c = BertsekasHeurCost G H j}
        (BertsekasHeurCost G H (r K))) := by sorry

end BertsekasDP

Source

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, Proposition 6.4.1

Read-back

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

Let $V$ be a finite type with decidable equality, $G$ a graph structure, $H$ a base heuristic, and assume BertsekasSeqConsistent holds for $(G,H)$ (tails of heuristic paths from non-destination vertices are again heuristic paths). Let $r : \mathbb{N} \to V$ be an infinite sequence of vertices such that:

(hstart) $r_0 \notin G.\mathrm{dest}$ ;
(hstep) for every $k$ with $r_k \notin G.\mathrm{dest}$ : $r_{k+1} \in \mathcal{N}(r_k)$ and $\hat H(r_{k+1}) \le \hat H(j)$ for every $j \in \mathcal{N}(r_k)$ — the sequence always steps to a heuristic-cost-minimizing out-neighbour;
(htie) a tie-breaking rule: for every $k$ with $r_k \notin G.\mathrm{dest}$ , for every vertex $j_H$ and list $l$ , if the heuristic path from $r_k$ has the literal form $r_k :: j_H :: l$ and $j_H$ itself minimizes $\hat H$ over $\mathcal{N}(r_k)$ (i.e. $\hat H(j_H) \le \hat H(j)$ for all $j \in \mathcal{N}(r_k)$ ), then $r_{k+1} = j_H$ — i.e. whenever the base heuristic's own next vertex is among the minimizers, the sequence must follow it;
(habsorb) for every $k$ with $r_k \in G.\mathrm{dest}$ : $r_{k+1} = r_k$ (once at a destination the sequence is constant).

The conclusion is a conjunction:

There exists some index $K$ with $r_K \in G.\mathrm{dest}$ (termination: the sequence reaches the destination set at some finite time).
For every index $K$ with $r_K \in G.\mathrm{dest}$ : $\hat H(r_K) \le \hat H(r_0)$ , and the number $\hat H(r_K)$ is the least element (in the IsLeast sense: it both belongs to the set and is $\le$ every element of the set) of the set of real numbers

\Big\{ c \in \mathbb{R} \;\Big|\; c = \hat H(r_0) \;\lor\; \exists\, k < K,\ r_k \notin G.\mathrm{dest} \ \land\ \exists\, j \in \mathcal{N}(r_k),\ c = \hat H(j) \Big\},

i.e. the set consisting of $\hat H(r_0)$ together with the heuristic costs $\hat H(j)$ of all out-neighbours $j$ of all non-destination vertices $r_k$ visited strictly before time $K$ . Note $\hat H(r_K)$ is here $G.\mathrm{cost}(r_K)$ , since heuristic paths from destination vertices are singletons. The IsLeast claim includes membership: $\hat H(r_K)$ must literally equal one of the listed values, not merely bound them below. The proof is left as sorry.

Human review

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

View graph