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.