Min-plus powers record cheapest decision walks

Proved

MDPComplexity.AverageCost.min_plus_walks

by mikedeng1 · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

graph-theorymin-plusp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1shortest-walk

Let $A$ be the min-plus adjacency matrix of a finite deterministic process. For states $u,v$ and an integer $k\geq0$ , the entry $(A^k)_{uv}$ is $+\infty$ exactly when there is no $k$ -arc decision walk from $u$ to $v$ . Whenever there is such a walk, the entry is the least of their total costs:

(A^k)_{uv}=\min\left\{\sum_{j=0}^{k-1}c(e_j):e_0,\ldots,e_{k-1}\text{ is a decision walk from }u\text{ to }v\right\}.

This identifies the matrix computation used for shortest closed walks. Parallel decisions are compared by cost; an absent arc has the extended value $+\infty$ .

Formalization Note The zeroth power is the min-plus identity, so its diagonal entries are zero and other entries are infinite. A walk records each decision arc, not only its state sequence.

Preamble

import Definitions.Def_MDPComplexity_AverageCost_Model

Formal statement

namespace MDPComplexity.AverageCost

variable {S : Type*} [Fintype S] [DecidableEq S]

/-- §3, p. 446: the kth min-plus power records exactly the cheapest k-arc
decision walk, and infinity records the absence of such a walk. -/
theorem min_plus_walks (M : DetMDP S) (k : ℕ) (u v : S) :
    (M.minPlusPow k u v = ⊤ ↔
      ¬ ∃ W : M.Walk k, W.start = u ∧ W.finish = v) ∧
    (∀ W : M.Walk k, W.start = u → W.finish = v →
      ∃ r : ℝ, M.minPlusPow k u v = (r : WithTop ℝ) ∧
        IsLeast {x : ℝ | ∃ W' : M.Walk k,
          W'.start = u ∧ W'.finish = v ∧ x = W'.cost} r) := by sorry

end MDPComplexity.AverageCost

Source

Papadimitriou and Tsitsiklis, The Complexity of Markov Decision Processes, Math. Oper. Res. 12(3) (1987), p. 446, §3 The infinite horizon undiscounted case, proof of Theorem 3, https://doi.org/10.1287/moor.12.3.441

Human review

Endorsed by Shuze Chen · Oct 6, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph