Correct and certify a finite-chain stationary candidate

Inputs. An integer $n\ge 1$, an exact rational matrix $P\in {\mathbb{Q}}^{n\times n}$, an exact rational raw candidate $y\in {\mathbb{Q}}^n$, and an integer $m\ge 1$. The represented rational entries are the exact data for this certificate; certification proceeds only when P is column-stochastic, as checked in the first instruction.

Outputs. Return invalid-input if P has a negative entry or a column not summing exactly to one. Set $y_i^{+}=\max (y_i,0)$ and $s={\sum }_i{y}_i^{+}$. If $s=0$, return candidate-unavailable. Otherwise set $x=y^{+}\mathrm{/}s$ and $c=\mathrm{\parallel }y-x{\mathrm{\parallel }}_1$. Compute $M=P^m$ by $M_0=I$ and $M_{k+1}=P{M}_k$ for $0\le k<m$. Compute $r=Px-x$ and

$q=1-{\min }_{j,k}{\sum }_i\min (M_{ij},M_{ik})\mathrm{.}$

If $q\ge 1$, return certificate-unavailable with the corrected candidate and computed quantities; do not report an accuracy bound. If $q<1$, return certified with the candidate $x$, correction ledger $c$, residual $r$, coefficient $q$, and bound

$B=c+\frac{m\mathrm{\parallel }r{\mathrm{\parallel }}_1}{1-q}\mathrm{.}$

All operations above use exact rational arithmetic and finitely many loops. If $q\ge 1$, the procedure reports no accuracy bound; if $q<1$, it returns the stated exact bound. The procedure takes $y$ as input and makes no claim about how a stationary solver produced it.