Exact rollout cost identity (Prop. 6.4.3)

Proved

BertsekasDP.rollout_cost_decomposition

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

rollouttelescoping

Proposition 6.4.3 (exact cost identity for the rollout algorithm). For an arbitrary base heuristic $\mathcal{H}$ — sequentially improving or not — let $(i_1, \dots, i_{\bar m})$ be a path generated by a terminating run of the rollout algorithm from a non-destination node $i_1$ to a destination $i_{\bar m}$ . Writing

\delta_i \;=\; \min_{j \in N(i)} H(j) \;-\; H(i)

for the defect at a node, the rollout cost decomposes exactly as

g(i_{\bar m}) \;=\; H(i_1) \;+\; \sum_{m=1}^{\bar m - 1} \delta_{i_m} .

The identity is a telescoping one: each rollout step realizes precisely the neighborhood minimum, so the improvements accumulate additively along the run. It immediately yields Prop. 6.4.2 — under sequential improvement every $\delta_i \le 0$ , hence $g(i_{\bar m}) \le H(i_1)$ — but it says more, since it quantifies the improvement rather than merely bounding it, and it applies with no assumption on the heuristic at all. It is the discrete counterpart of the slack-accumulating bound of Prop. 6.3.2 for limited lookahead policies.

Formalization Note The defect takes the junk value $0$ at a node with no neighbors, which cannot occur along a run. The sum runs over the nodes of the path with the last one removed, in order and with multiplicity — a node visited twice contributes twice.

Preamble

import Mathlib
import Definitions.Def_BertsekasGraphSearch

Formal statement

namespace BertsekasDP

theorem rollout_cost_decomposition {V : Type} [Fintype V] [DecidableEq V]
    (G : BertsekasGraphSearch V) (H : BertsekasBaseHeuristic G)
    (l : List V) (hrun : BertsekasIsRolloutRun G H l)
    (i₁ : V) (hhead : l.head? = some i₁) (hstart : i₁ ∉ G.dest)
    (d : V) (hlast : l.getLast? = some d) :
    G.cost d = BertsekasHeurCost G H i₁ +
      (l.dropLast.map (BertsekasRolloutDelta G H)).sum := by sorry

end BertsekasDP

Source

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

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 BertsekasGraphSearch on $V$ , and $H$ a BertsekasBaseHeuristic for $G$ . Suppose:

$l$ is a list of vertices satisfying BertsekasIsRolloutRun for $(G,H)$ (nonempty; each consecutive step goes to an out-neighbour minimizing $\hat H$ over the current vertex's out-neighbours; all elements except the last are outside $G.\mathrm{dest}$ ; the last element is some destination vertex);
$i_1 \in V$ is the first element of $l$ (the hypothesis states literally that the head of $l$ is $i_1$ ), and $i_1 \notin G.\mathrm{dest}$ ;
$d \in V$ is the last element of $l$ (the hypothesis states literally that the last element of $l$ is $d$ ; membership of $d$ in $G.\mathrm{dest}$ is not restated here, though it follows from the rollout-run hypothesis).

Then the claimed equality is

G.\mathrm{cost}(d) \;=\; \hat H(i_1) \;+\; \sum_{v \in l' } \Delta(v),

where $\hat H$ is BertsekasHeurCost, $\Delta$ is BertsekasRolloutDelta (min-over-neighbours heuristic cost minus own heuristic cost, with junk value $0$ at neighbourless vertices), and $l'$ is the list $l$ with its last element removed, the sum being taken over the entries of $l'$ in order with multiplicity (a vertex occurring twice in $l'$ contributes twice). The proof is left as sorry (the statement carries no completed proof).

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