A computed GMRES correction has an explicit finite-precision residual gap

Let $A\in {\mathbb{R}}^{n\times n}$ with $n\ge 1$, let $r_0=b-A{x}_0$, and let $m\ge 1$. Put $Q_m=[q_1\cdots q_m]$, $Q_{m+1}=[q_1\cdots q_{m+1}]$, and ${\bar{H}}_m\in {\mathbb{R}}^{(m+1)\times m}$. Suppose computed Arnoldi vectors satisfy $A{Q}_m=Q_{m+1}{\bar{H}}_m+E_m,$ where the columns of $E_m$ are the local error vectors of Two-pass MGS Arnoldi has an explicit local relation and an a posteriori orthogonality bound. Let $I$ be the $(m+1)$-by-$(m+1)$ identity and $\bar{G}=Q_{m+1}^{\mathsf{T}}{Q}_{m+1}-I$ and $\eta =\mathrm{\parallel }\bar{G}{\mathrm{\parallel }}_F$, where $\mathrm{\parallel }B{\mathrm{\parallel }}_F=({\sum }_{a,b}\mathrm{\mid }{B}_{ab}{\mathrm{\mid }}^2{)}^{1\mathrm{/}2}$. Suppose $r_0={\beta }_1{q}_1+{\delta }_0,\widehat{x}=x_0+Q_{m}y+{\delta }_x,$ where $y\in {\mathbb{R}}^m$ is the coefficient vector returned by the computed GMRES least-squares stage and ${\delta }_x$ is the update error (zero for an exact vector update). Define $e_1=(1,0,\dots ,0{)}^{\mathsf{T}}\in {\mathbb{R}}^{m+1}$ and the Arnoldi-coordinate least-squares residual $g:={\beta }_1{e}_1-{\bar{H}}_{m}y,$ using the stored computed values, and let $r=b-A\widehat{x}$ be the exact true residual. Then $\mathrm{\parallel }r-Q_{m+1}g{\mathrm{\parallel }}_2\le \mathrm{\parallel }{\delta }_0{\mathrm{\parallel }}_2+\mathrm{\parallel }{E}_m{\mathrm{\parallel }}_2\mathrm{\parallel }y{\mathrm{\parallel }}_2+\mathrm{\parallel }A{\mathrm{\parallel }}_2\mathrm{\parallel }{\delta }_x{\mathrm{\parallel }}_2,$ and $\mathrm{\parallel }r{\mathrm{\parallel }}_2\le \sqrt{1+\eta }\mathrm{\parallel }g{\mathrm{\parallel }}_2+\mathrm{\parallel }{\delta }_0{\mathrm{\parallel }}_2+\mathrm{\parallel }{E}_m{\mathrm{\parallel }}_2\mathrm{\parallel }y{\mathrm{\parallel }}_2+\mathrm{\parallel }A{\mathrm{\parallel }}_2\mathrm{\parallel }{\delta }_x{\mathrm{\parallel }}_2\mathrm{.}$ Matrix $2$-norms are induced by Euclidean vector norms. For the recomputation conclusion, assume the real operationwise model of Operationwise real and complex floating point arithmetic with rounded square roots and fused multiply-add with unit roundoff $u$, $nu<1$, and successful row-dot and subtraction operations; every nonzero exact product and partial sum in a row dot is normal-range, and exact-zero products, sums, or subtractions are permitted. If the true residual is recomputed by these rounded row dot products and rounded subtraction, write $\widehat{Ax}$ for the computed product and $\widehat{r}=\mathrm{fl}(b-\widehat{Ax})$. Then $\mid \mathrm{\parallel }\widehat{r}{\mathrm{\parallel }}_2-\mathrm{\parallel }r{\mathrm{\parallel }}_2\mid \le {\rho }_{rec},{\rho }_{rec}:={\left({\sum }_{i=1}^n{d}_i^2\right)}^{1\mathrm{/}2},$ where $d_i:={\gamma }_n{\sum }_{j=1}^n\mathrm{\mid }{A}_{ij}\mathrm{\mid }\mathrm{\mid }{\widehat{x}}_j\mathrm{\mid }+u\mathrm{\mid }{b}_i-{\widehat{Ax}}_i\mathrm{\mid }\mathrm{.}$ No accuracy claim is made for the least-squares solve: its computed $y$ and the resulting $g$ appear explicitly.