# 02 — Bellman certificates and score regret --- # Claims 3–4 — VERIFIED (4/4) > Theorem 3 shows that sequences of functions satisfying Bellman sub-/super-solution inequalities yield provability certificates (upper and lower bounds on the optimal value function) without requiring the full MDP to be solved, with the certificate gap defined as UB(x0) - LB(x0) (Theorem 3, Definition 5, Section 5). > Theorem 4 bounds the worst-case regret of score-guided planning under uniform score-approximation error εb as 0 ≤ V*_B(x0) - V^{πh}_B(x0) ≤ 2∑_{b=1}^{B} εb, showing performance degrades linearly with accumulated approximation error (Theorem 4, Section 6). ## Certificates without solving the full MDP The Bellman operator is monotone: `V <= W` implies `T V <= T W`. Theorem 3 (`thm:p1-5.3`) turns that simple order fact into a certificate system. An upper sequence satisfying `U_0 >= 1_G`, `U_{b+1} >= T U_b` obeys `U_b >= V*_b`; a lower sequence satisfying `L_0 <= 1_G`, `L_{b+1} <= T L_b` obeys `L_b <= V*_b`. Definition 5 names `[L_B(x0), U_B(x0)]` a provability certificate and `U_B(x0)-L_B(x0)` its gap. The local reproduction creates **48** exact certificate pairs by shifting the exact value sequence up/down and clipping to `[0,1]`. It checks **3,720** initial, recursive, and sandwich inequalities. Every lower sequence remains below `V*`; every upper sequence remains above it; every reported gap is computed as an exact rational number. ## Score-guided planning Let `h_b` approximate `Q*_b` uniformly with error `epsilon_b`, and let the policy greedily maximize `h_b`. The one-step comparison uses three inequalities: `Q*(a*) <= h(a*) + epsilon <= h(a_hat) + epsilon <= Q*(a_hat) + 2 epsilon`. Theorem 4 (`thm:p1-6.3`) telescopes this through the finite horizon: `0 <= V*_B(x0) - V^pi_h_B(x0) <= 2 sum_{b=1}^B epsilon_b`. The audit perturbs exact action values inside a rational error envelope for **200** independent MDP/horizon cases. It then recomputes the greedy policy value from the kernel rather than assuming the bound. All regrets are nonnegative and all remain inside `2 sum epsilon_b`; **158** cases actually change policy and incur positive regret. The factor two cannot be casually reduced. A one-step witness has a bad action with `Q=0`, a best action with `Q=2 epsilon`, and tied scores `h=epsilon`. Deterministic tie-breaking selects the bad action. The realized regret is exactly `2 epsilon`, matching the theorem constant. ## Where statistical complexity enters The score error is not assumed free. Version 2's Lemma 7.1 controls adaptive uniform deviations with covering numbers, and its supplement distinguishes explicit net coverage from sequential Rademacher-complexity control under adaptive/on-policy data. This package reproduces the downstream bound exactly and preserves those hypotheses. It does not claim that arbitrary self-generated rollouts automatically satisfy uniform coverage.