Finite precision point linear solve certificate with explicit status

Input $n\ge 1$, stored finite real or complex square data $A\in {\mathbb{C}}^{n\times n}$, $b\in {\mathbb{C}}^n$, a proposed computed inverse $R\in {\mathbb{C}}^{n\times n}$, and a proposed computed solution $\widehat{x}\in {\mathbb{C}}^n$. All stored entries are interpreted as exact dyadics. Use the operationwise arithmetic model with unit roundoff $u$; if $(n-1)u\ge 1$, return inconclusive before applying the rounded-residual bounds. The procedure validates the proposals; it does not assume that the solver which produced them is stable.

1. Set $g_n=(1+6u)\mathrm{/}(1-(n-1)u)-1$. Evaluate each column $a_j$ of $A$ through the operationwise model as ${\widehat{m}}_j=\mathrm{fl}(R{a}_j)$. If any operation returns range-failure, return range-failure with its first operation index. Compute an outward upper bound $v_j$ for $g_n\mathrm{\parallel }R{\mathrm{\parallel }}_F\mathrm{\parallel }{a}_j{\mathrm{\parallel }}_2$, which by the rounded-linear-residual lemma bounds $\mathrm{\parallel }{\widehat{m}}_j-R{a}_j{\mathrm{\parallel }}_2$. Every dot product used for these allowances must complete successfully under the no-underflow model. Outward-evaluate $I-[{\widehat{m}}_1\cdots {\widehat{m}}_n]$ and let $q$ be an outward upper bound for its Frobenius norm plus $\sqrt{{\sum }_j{v}_j^2}$.

2. Evaluate $\widehat{v}=\mathrm{fl}(A\widehat{x})$ and $\widehat{w}=\mathrm{fl}(\widehat{v}-b)$. Compute an outward upper bound $W$ for $g_n\mathrm{\parallel }A{\mathrm{\parallel }}_F\mathrm{\parallel }\widehat{x}{\mathrm{\parallel }}_2+u(\mathrm{\parallel }\widehat{v}{\mathrm{\parallel }}_2+\mathrm{\parallel }b{\mathrm{\parallel }}_2)$, which bounds $\mathrm{\parallel }\widehat{w}-(A\widehat{x}-b){\mathrm{\parallel }}_2$. Evaluate $\widehat{c}=\mathrm{fl}(R\widehat{w})$ and compute an outward upper bound $v_c$ for $g_n\mathrm{\parallel }R{\mathrm{\parallel }}_F\mathrm{\parallel }\widehat{w}{\mathrm{\parallel }}_2$, which bounds $\mathrm{\parallel }\widehat{c}-R\widehat{w}{\mathrm{\parallel }}_2$. Let $r$ be an outward upper bound for

$$\mathrm{\parallel }\widehat{c}{\mathrm{\parallel }}_2+\mathrm{\parallel }R{\mathrm{\parallel }}_{F}W+v_c\mathrm{.}$$

The Frobenius norm bounds $\mathrm{\parallel }R{\mathrm{\parallel }}_2$.

3. All norm bounds, square roots, and final scalar operations are evaluated outward. If a bound cannot be enclosed finitely, return inconclusive. If $q\ge 1$, return inconclusive with the computed bounds. If $q<1$, outward-compute $s\ge r\mathrm{/}(1-q)$ and return certified with the Euclidean ball $B(\widehat{x},s)$.

The output range-failure describes failure of a requested floating operation. inconclusive means only that this validation did not prove a usable bound; it does not assert that $A$ is singular or that the proposed solution is inaccurate.