Finite-budget adaptive finite-state projection

Inputs. A given nonexplosive chain $X$ and initial law $p_0$; a finite positive integer $N$ and an explicitly supplied nested list of nonempty finite sets $F_1\subseteq \cdots \subseteq F_N$; for each $F_i$, its exact finite cemetery-lift generator ${\tilde{Q}}_{F_i}$ and lifted initial vector from Killed finite-state projection and cemetery lift; final time $T\ge 0$; tolerance $\epsilon >0$; a positive integer per-projection term cap $B$; and an arithmetic mode that is either exact real arithmetic or a validated arithmetic backend satisfying the requirements below and of Budgeted uniformization accumulation with time splitting.

The supplied lift data must be the exact rates and initial masses of the given chain. An implementation may obtain the cemetery rate from the exact exit rate minus the finite sum of within-$F_i$ rates. A validated backend must certify the lift-rate calculation and its admissibility, the solver's scalar and vector certificates, and an outward enclosure of each computed cemetery coordinate, including the certified arithmetic/algebraic error required by Uniformization truncation, mass loss, and arithmetic-error ledger; if any required certificate is unavailable, the corresponding projection is uncertified.

Procedure. For $i=1,\dots ,N$ in order:

1. Let $r_{i,z}:=-({\tilde{Q}}_{F_i}{)}_{zz}$ for $z\in F_i\cup \{†\}$ and set ${\nu }_i:={\max }_{z\in F_i\cup \{†\}}{r}_{i,z}={\max }_{x\in F_i}\lambda (x)$; this includes the cemetery state's zero exit rate. If a validated backend cannot certify ${\nu }_i$ and its admissibility, treat the solver status as certificate-unavailable. Otherwise apply Budgeted uniformization accumulation with time splitting to $({\tilde{Q}}_{F_i},{\tilde{p}}_{F_i,0},T)$ with admissible rate ${\nu }_i$, positive tail budget $\epsilon$, term cap $B$, and the supplied arithmetic mode. If ${\nu }_i=0$, use the solver's zero-rate branch. If the status is budget-exhausted or certificate-unavailable, or the exact lift data are unavailable, return inconclusive with the statuses and all completed projection records; do not skip an uncertified projection.
2. Let ${\widehat{c}}_i$ be the computed cemetery coordinate. If the solver returns tail and arithmetic/algebraic error bounds $T_i$ and $E_{\mathrm{a}\mathrm{l}\mathrm{g},i}$, put ${\delta }_i:=T_i+E_{\mathrm{a}\mathrm{l}\mathrm{g},i}$, the total certified ${\mathrm{\ell }}^1$ error bound. Form the outward-certified interval $L_i=\max (0,{\widehat{c}}_i-{\delta }_i),U_i=\min (1,{\widehat{c}}_i+{\delta }_i)\mathrm{.}$ Record $F_i$, ${\nu }_i$, the computed vector, ${\widehat{c}}_i$, $[L_i,U_i]$, its tail bound $T_i$, and its arithmetic/algebraic error $E_{\mathrm{a}\mathrm{l}\mathrm{g},i}$.
3. If exact comparison or validated interval arithmetic certifies $U_i\le \epsilon$, return certified with this projection and its record.

If all $N$ projections have valid records but none passes the tolerance, return inconclusive with every record. The algorithm uses at most $N$ projections and $NB$ uniformization terms. It makes no claim that some finite projection outside this supplied list meets $\epsilon$.