# 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.