Use the finite controller model of Definition [ftip-00M5]. For each time, choose a finite nonempty state set \(S_t\) and a map \(\phi _t:\mathcal H_t\to S_t\). Require finite nonempty action sets \(A_t(s)\) such that \(A_t(h)=A_t(\phi _t(h))\) at every history. The state retains residual budgets and enough information for the same hard admission rule. The controller still observes the full history.

Let \(Q_t(\cdot \mid h,a)\) be the image of the fixed history kernel under \(\phi _{t+1}\), and let \(\widehat P_t(\cdot \mid s,a)\) be a proposed state transition law. Choose finite errors \(\epsilon _t(s,a)\geq 0\) so that, for every permitted history and action,

This condition includes histories unvisited by a chosen policy: the kernel there is part of the model. For finite functions \(\widehat q:S_H\to \mathbb R\) and \(e_H:S_H\to \mathbb R_+\), require

Write \(\nu (s)=\mu \{h:\phi _0(h)=s\}\) for the initial state law. Low average prediction error on sampled histories does not establish these uniform inequalities. The erased-bit example in Example [ftip-00M7] shows why policy-relevant information cannot simply be averaged away.

Under Definition 1, let finite functions \(W_t:S_t\to \mathbb R\) satisfy \(W_H(s)\geq \widehat q(s)+e_H(s)\) and, for every \(t<H\), \(s\in S_t\), and \(a\in A_t(s)\),

Here \(\operatorname {span}(f)=\max f-\min f\). Every permitted history-dependent randomized controller then satisfies

For any feasible controller \(\pi _0\) with a justified finite lower bound \(L\leq J(\pi _0)\), the frontier of Definition [ftip-00M5] obeys

A numerical supersolution is a certificate only after all of its inequalities and the abstraction hypotheses are justified. If the model bounds hold jointly with probability at least \(1-\delta _M\) and the lower bound with probability at least \(1-\delta _E\), the bracket holds with probability at least \(1-\delta _M-\delta _E\) by a union bound. Each coverage statement must apply to the selected model or policy; no independence between the two events is required.

Suppose the abstraction is exact: \(Q_t(\cdot \mid h,a)= P_t(\cdot \mid \phi _t(h),a)\) for all histories and actions, and terminal quality is exactly \(q(h_H)=r(\phi _H(h_H))\). A one-sided terminal bound with zero error would not imply this equality. Retain the exact legal actions and hard-budget state from Definition 1.

Introduce nonnegative state masses \(z_t(s)\) and action masses \(x_t(s,a)\), with \(z_0=\nu \). For \(0\leq t<H\), impose

The linear program maximizes \(\sum _s z_H(s)r(s)\). Every full-history controller induces these flows because the next-state law given a state and action is exact. Conversely, at positive mass choose action \(a\) with probability \(x_t(s,a)/z_t(s)\); at zero mass choose any legal action. Induction on time reproduces the flows in the original history model. Hence the LP optimum equals its mathematical controller frontier. For \(H=0\), there are no action flows and the value is \(\nu r\).

Set \(W_H=r\) and recurse with \(W_t(s)=\max _{a\in A_t(s)}\sum _{s'}P_t(s'\mid s,a)W_{t+1}(s')\). A maximizing action exists by finiteness and gives a policy attaining \(\nu W_0\); the Bellman upper bound gives the reverse inequality. This proves equality with the optimum and exhibits matching lower and upper certificates. It does not establish an efficient implementation of the policy. The flow construction is the scalar finite-horizon specialization of Mifrani and Noll, Section 3; the hard-budget encoding is an additional modeling requirement here.

If hard admission is replaced by constraints on expected cost, the resulting program describes a different class. For \(B>0\), a one-step cost equal to \(2B\) or zero with probability \(1/2\) each has expectation \(B\), yet violates cap \(B\) with probability \(1/2\). An expected-cost model can upper-bound the hard-budget frontier only when it is a valid relaxation containing every hard-feasible policy. Its own policies need not respect the realized cap.

Fix the task law, evaluator, initial model, tools, observations, horizon, and intervention class. For \(\mathbf B\preceq \mathbf B'\), assume every controller feasible at \(\mathbf B\) remains permitted at \(\mathbf B'\) with the same outcome law. If a feasible controller at \(\mathbf B\) gives lower bound \(L_{\mathbf B}\) and Theorem 2 gives upper bound \(U_{\mathbf B'}\) at \(\mathbf B'\), then

If the certified gap is at most \(\varepsilon \), this instantiates Theorem [ftip-00LM]'s conditional saturation statement. An observed plateau alone supplies no such upper certificate. Changing an excluded tool, representation, or training procedure changes the comparison class.