01 — Optimal policies and Bellman structure
Claims 1–2 — VERIFIED (4/4)
Theorem 1 establishes that the space of finite measures with bounded mass forms a compact metric space under the bounded Lipschitz metric, providing the topological foundation for the measure-valued goal encoding of the reachability MDP (Theorem 1, Section 3).
Theorem 2 proves that under mild Feller-type continuity conditions on the transition kernel, optimal deterministic Markov policies exist for the finite-horizon time-bounded reachability MDP (Theorem 2).
Source theorem chain
Version 2 encodes a proof state containing finitely many goals as a positive atomic measure on a compact goal-embedding space. With total mass truncated at W, Theorem 1 (thm:p1-2.1) states that M_{<=W}(X) is compact under the bounded-Lipschitz metric. A solved proof is the zero measure. This gives a permutation-invariant state representation that permits variable goal counts.
The time-bounded proving objective is finite-horizon reachability of {0}. Starting from V*_0(x)=1[x in G], the optimal recursion is
Q*_b(x,a) = integral V*_{b-1}(x') P(dx' | x,a)
and
V*_{b+1}(x) = 1[x in G] OR sup_a Q*_{b+1}(x,a).
Under compact actions, weak/Feller continuity of the kernel, and the closed goal set, Theorem 2 (thm:p1-4.2) states that every action supremum is attained and an optimal deterministic Markov policy exists.
Exact finite-MDP audit
The local audit constructs 48 finite compact reachability MDPs. Each has a goal, a dead state, three active proof states, two or three actions, rational transition probabilities, and horizons from 2 through 7. Finite state/action spaces satisfy compactness and Feller continuity trivially.
Every transition row sums to exactly one as a rational number. Backward induction performs 2,160 separate checks that V_b=T V_{b-1} and that the recorded action attains each maximum. There is no numerical tolerance and no sampled trajectory estimate.
For 18 smaller instances the audit independently enumerates all time-indexed deterministic Markov mappings: 1,152 policies total. Direct policy evaluation matches the Bellman optimum in every case. This is the operational content of the existence result: backward induction does not merely report a supremum; it constructs an attaining policy.
The compactness surface is separately exercised by 40 finite atomic-measure grids with 2–6 goal atoms and mass bounds 1–8. The largest contains 3,003 measure states. Finiteness certifies compactness for each grid and makes the bounded-mass constraint explicit.
Interpretation boundary
The finite grids do not prove Theorem 1 for arbitrary compact metric goal spaces. The general result relies on the primary proof's tightness/Prokhorov and bounded-Lipschitz weak-convergence argument. Likewise, finite kernel continuity is automatic and does not erase the Feller assumption for continuous state spaces. The package therefore combines source-locked universal theorems with exact finite witnesses, never extrapolating a sweep into a new proof.