Corrected exchange claim: at most one simple cycle occurs more than n times
ProvedMDPComplexity.StationaryHorizon.one_frequent_cycleLet have states, with arbitrary real decision costs, and fix an initial state and a horizon . Some cheapest -arc walk from has a decomposition into a simple path and simple cycles in which any cycle occurring more than times has the least mean cost among the cycles in that decomposition, and no two distinct cycles each occur more than times.
The claim controls the repeated cycles that appear in the finite-horizon structure argument.
Formalization Note The paper prints an exchange that repeats the lower-mean cycle fewer times and the other cycle more times, reversing the cost inequality. The cost-reducing exchange runs in the opposite direction. The conclusion uses “more than ” to leave a copy of a cycle in place when other cycles attach there. Equality of recorded cycles includes their chosen decision arcs, so parallel arcs remain distinct.
import Mathlib import Definitions.Def_MDPComplexity_StationaryHorizon_Model
namespace MDPComplexity.StationaryHorizon
variable {S : Type} [Fintype S]
/-- §3, p. 447, exchange claim, corrected: a minimum-cost `T`-arc walk has a
decomposition in which at most one simple cycle occurs more than `n` times. -/
theorem one_frequent_cycle (M : DetMDP S) (s₀ : S) (T : ℕ) :
∃ (W : M.Walk T), W.x 0 = s₀ ∧
IsLeast {y : ℝ | ∃ V : M.Walk T, V.x 0 = s₀ ∧ y = V.cost} W.cost ∧
∃ (p : ℕ) (P : M.Walk p) (Cs : List (Σ k : ℕ, M.Walk k)),
M.IsCycleDecomposition W P Cs ∧
∀ C₁ ∈ Cs, ∀ C₂ ∈ Cs,
Fintype.card S < Set.ncard {i : Fin Cs.length | Cs[i] = C₁} →
(C₁.2.cost / (C₁.1 : ℝ) ≤ C₂.2.cost / (C₂.1 : ℝ)) ∧
(Fintype.card S < Set.ncard {i : Fin Cs.length | Cs[i] = C₂} → C₁ = C₂) := by sorry
end MDPComplexity.StationaryHorizon
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.