Budgeted uniformization accumulation with time splitting

Inputs. A finite column generator $Q$, a column probability vector $p_0$, $t\ge 0$, an admissible rate $\nu \ge {\max }_j{r}_j$, a positive tail budget $\epsilon$, a positive integer total-term cap $B$, and either exact real arithmetic or a validated arithmetic backend. In a rounded execution, the backend must certify the scalar control decisions defining $m$ and $\mu$, each finite tail-budget comparison, and an outward upper bound $T\ge m{G}_K(\mu )$; it must also return a certified ${\mathrm{\ell }}^1$ error bound $E_{\mathrm{a}\mathrm{l}\mathrm{g}}:=\mathrm{\parallel }\widehat{p}-R_{\mu ,K}^m{p}_0{\mathrm{\parallel }}_1$ for its computed vector. The vector bound includes any arithmetic error from the weights, time split, and matrix-free $P$ actions. If any scalar or vector certificate is unavailable, return certificate-unavailable.

Outputs. Return $(p_0,0,0)$ when $\nu =0$ or $t=0$. Otherwise return budget-exhausted or certificate-unavailable, or an approximate vector $\widehat{p}$ and certified bounds $(T,E_{\mathrm{a}\mathrm{l}\mathrm{g}})$ for which $\mathrm{\parallel }p(t)-\widehat{p}{\mathrm{\parallel }}_1\le T+E_{\mathrm{a}\mathrm{l}\mathrm{g}}$. Here $T\ge m{G}_K(\mu )$ is an outward-certified Poisson-tail upper bound and $E_{\mathrm{a}\mathrm{l}\mathrm{g}}$ bounds the arithmetic/algebraic error relative to the exact truncated accumulation. In exact real arithmetic, $T=m{G}_K(\mu )$ and $E_{\mathrm{a}\mathrm{l}\mathrm{g}}=0$.

Procedure. For $\nu t>0$, set $m=\lceil \nu t\rceil$ and $\mu =\nu t\mathrm{/}m$, so $0<\mu \le 1$. A rounded backend must certify these values and inequalities; if it cannot, return certificate-unavailable. If $m>B$, return budget-exhausted. Set $K_{\max }=\lfloor B\mathrm{/}m\rfloor -1$. Search the finite list $K=0,1,\dots ,K_{\max }$ for a member satisfying

$G_K(\mu ):=\frac{e^{-\mu }{\mu }^{K+1}}{(K+1)!(1-\mu \mathrm{/}(K+2))}\le \epsilon \mathrm{/}m\mathrm{.}$

In rounded arithmetic, accept a candidate only when a validated upper enclosure proves the displayed inequality, and set $T=\epsilon$, copying the already certified accepted tail budget. This is an exact bound because the accepted comparison certifies $m{G}_K(\mu )\le \epsilon$. If no candidate works, return budget-exhausted when the comparisons certify that every candidate fails, and certificate-unavailable when they do not decide the search. In exact arithmetic set $T=m{G}_K(\mu )$. Set $P=I+Q\mathrm{/}\nu$ and $x_0=p_0$. For each substep $j=1,\dots ,m$, initialize $v_0=x_{j-1}$, $w_0=e^{-\mu }$, and $x_j=w_0{v}_0$. For $k=0,\dots ,K-1$, update

$v_{k+1}=P{v}_k,w_{k+1}=w_k\frac{\mu }{k+1},x_j\leftarrow x_j+w_{k+1}{v}_{k+1}\mathrm{.}$

These $P$ actions use the exact operator-application interface of The matrix-free access model for Krylov methods: the routine supplies $v\mapsto Pv$ and vector additions and scalar multiples, without requiring stored matrix entries. No CSR representation, operation-count estimate, or convergence claim is part of this procedure. The exact term count is $m(K+1)\le B$ and the certified tail bound satisfies $T\le \epsilon$. Never replace a tail certificate by floating-point $1-{\sum }_{k\le K}{w}_k$.