Finite-budget DPO preserves its valid pair and terminates with finite oracle work

Fix an accepted parameter in $\mathrm{\Theta }$. The reference and policy coordinates are positive, so every log ratio is a finite real and each $u_i$ is finite. By [F5], $1+e^{-u_i}>0$ and its logarithm is finite. For $u\ge 0$, the stable evaluation expression is exactly $\log (1+e^{-u})$. For $u<0$, put $a=-u>0$ and $b=\log (1+e^u)$. The exponential addition and reciprocal identities give $e^{a+b}=e^{-u}(1+e^u)=1+e^{-u}$, so [F5] gives $a+b=\log (1+e^{-u})$. Thus the stable expression equals the same finite loss on both branches, including $u=0$, and finite dataset and batch averages are finite.

Each supplied graph is finite and its specified exact primitive value, pullback and domain/branch tests terminate. Therefore its forward and reverse traversals terminate. At every successful strict-branch evaluation, [F4] gives both exact policy-log-probability gradients. Apply [F2] to the ordered batch of size $m_t\ge 1$, counting duplicated indices with their multiplicity; its gradient is exactly $g_t$. The algorithm does not differentiate the nonsmooth max/absolute-value implementation of the loss value.

There are finitely many record graphs with fixed finite node, slot and value-space dimensions. Forward evaluation, cotangent initialization and reverse accumulation consequently have a finite uniform upper bound in the declared unit-cost primitive model; finite branch tables are covered by their supplied terminating tests. Choose $C\ge d+1$ large enough to bound either one record's loss evaluation or its value-and-gradient computation, including the scalar sigmoid and loss operations. This bound depends on graph sizes and dimensions, not on parameter values, since primitive calls have unit cost in this model.

The initial parameter lies in $\mathrm{\Theta }$, and step 1.1 makes its full-data loss finite, proving the stored-pair invariant at initialization. Suppose it holds before an attempted update. A reverse-mode diagnostic returns that unchanged pair. Otherwise step 1.2 gives a finite vector $g_t$, and the finite step size gives a finite trial ${\theta }^{\mathrm{\prime }}$. The supplied exact oracle terminates and decides its membership. On rejection the unchanged valid pair is returned, without a policy evaluation at ${\theta }^{\mathrm{\prime }}$. On acceptance ${\theta }^{\mathrm{\prime }}\in \mathrm{\Theta }$, so step 1.1 gives its finite full-data loss; replacing the stored pair preserves the invariant. Finite induction therefore proves the invariant at every attempted update and every return.

Every attempted update traverses only finite graph and coordinate lists, finitely many records, and at most one terminating membership call. Hence it finishes or exits with the specified diagnostic. The outer loop has only $T$ entries, so there are at most $T$ attempts and no infinite search or convergence test. If none exits early, [F1] returns the pair after update $T$ with COMPLETED; for $T=0$ it performs no updates and returns the initialized pair.

The procedure evaluates the full-data loss initially and after at most $T$ accepted updates, using at most $n(T+1)$ record loss computations. Computing all attempted mini-batch objectives and gradients uses at most a constant times $M$ record computations, even if their forward values are recomputed. The remaining vector updates, loop and status bookkeeping cost $O((d+1)(T+1))$, bounded by $O(C(T+1))$. Step 1.3 gives the stated total work excluding membership. Each attempt makes at most one membership call, so $Q\le T$; the actual costs sum to a finite number and, when bounded uniformly, to at most $T{C}_{\mathrm{\Theta }}$. This proves the work bound without assigning any general computability property to arbitrary open $\mathrm{\Theta }$.