Let \(\mathcal Y_0\) be a nonempty finite set of candidate outcomes. Let \(U:\mathcal Y_0\to \mathbb R\) be an independently declared utility and \(\widehat U:\mathcal Y_0\to \mathbb R\) a proxy score. The proxy is a uniform approximation to \(U\) on \(\mathcal Y_0\) with error \(\varepsilon \) when \(\varepsilon \geq 0\) and

The candidate set is part of the claim. Approximation on training outcomes, on one policy's support, or in expectation is not uniform approximation on a larger set reached after optimization.

Under the conditions of Definition 1, choose

Then the utility regret of selecting by the proxy satisfies

This finite statement follows from the displayed hypotheses.

The bound in Theorem 2 follows directly from the uniform approximation condition. It compares two maximizers on one fixed finite candidate set. It does not describe how either score was learned or how a policy changes when that score becomes a training objective.

The result is useful because its transfer assumption is visible. To apply it after an update or a larger search, the uniform bound must hold on the outcomes that the new procedure can actually select. The verifier evidence of Definition [ftip-0047] can support such an audit, but reproducible evidence alone does not establish the bound.

Let the finite decision set be \(\mathcal Y_0=\{y_{\rm safe},y_{\rm exploit}\}\). Define its utility and proxy utility by the following table.

For \(0<\delta <1\), let a reference law \(P_\delta \) assign probability \(\delta \) to \(y_{\rm exploit}\). Its mean absolute proxy error is

which tends to zero with \(\delta \). Nevertheless, proxy maximization selects \(y_{\rm exploit}\) and incurs utility regret \(1\). Under the shifted law concentrated on that selected outcome, the mean error is \(2\). Thus no vanishing selection-regret bound can depend only on average error under the reference law.

This two-outcome construction isolates the distribution-shift warning in Remark [ftip-0061]. It does not claim that a particular learned verifier has this error profile; Example [ftip-0060] gives a source-linked checker instance with the same proxy-versus-utility separation.

A repeated verifier audit of size \(N\geq 1\) records pairs \((S_i,A_i)\in \{0,1\}^2\) for candidates \(1\leq i\leq N\). Here \(S_i\) is an independently defined success label and \(A_i\) is the verifier decision, as in Definition [ftip-005Z]. Define

The event \(\mathcal E_N^{\rm fa}\) says that at least one invalid candidate was accepted. It does not say which candidate a downstream selector returns. Write \(\phi _i=\Pr (C_i^{\rm fa})\). When \(\iota _i=\Pr (S_i=0)>0\), the conditional false-accept rate \(\eta _{+,i}=\Pr (A_i=1\mid S_i=0)\) is defined and \(\phi _i=\iota _i\eta _{+,i}\).

In the repeated audit of Definition 5, suppose the pairs \((S_i,A_i)\) are independent and identically distributed. Assume

Then the probability that at least one accepted invalid candidate exists among the \(N\) audited candidates is

It is strictly increasing in \(N\) when \(0<\iota \eta _+<1\), and it converges to \(1\) when \(\iota \eta _+>0\).

This finite statement follows from the displayed hypotheses.

For any joint law of a repeated verifier audit,

If \(\iota _i=\Pr (S_i=0)>0\) for every \(i\), this becomes

Without a dependence assumption, matching marginal error rates do not give the equality in Theorem 6; the events \(C_i^{\rm fa}\) could coincide.

This finite statement follows from the displayed hypotheses.

A proxy score can enter a training operator or a selection operator. In the first route it changes the policy; in the second it ranks a finite sample from a policy whose weights remain fixed.

The lifecycle accounting of Definition [ftip-005H] places the first route's rollout and update work in separate coordinates. The second route incurs rollout and evaluation work but no parameter update. Consequently, the event \(\mathcal E_N^{\rm fa}\) in Definition 5 concerns the candidate set presented to selection; it is not a claim about the selected output or a training-time policy change.

The rates in Definition [ftip-005Z] are properties of a declared audit law. They do not identify where errors occur within the task family, how error events depend across repeated candidates, or which accepted candidate a selector returns. Theorem 6 adds identical marginals and independence; Theorem 7 retains only the union bound.

Nor do these rates determine the effect of optimizing against the verifier. That effect depends on how the induced policy or selection law moves mass toward particular outcomes. The incomplete-checker example Example [ftip-0060] demonstrates one such movement, while Example 4 shows why an average reference-law error cannot rule it out. These are local finite statements. Any claim about a named verifier still requires its own audit distribution, evidence, and transfer argument.

The deterministic regret lemma Theorem 2, the independent-audit identity Theorem 6, and the union bound Theorem 7 follow from uniform approximation, independent trials, and subadditivity, respectively. Their hypotheses need not hold for a verifier chosen only for its empirical performance.