Normwise certified matrix-vector and vector-step arithmetic

Fix a finite complex matrix $M\in {\mathbb{C}}^{r\times s}$ with $r,s\ge 1$ and the Euclidean norms from The norm $\parallel v\parallel =\sqrt{⟨v,v⟩}$ induced by a real or complex inner product. A normwise certified vector arithmetic provider supplies the following outputs together with the stated bounds:

• For a real scalar $c$ and $z\in {\mathbb{C}}^s$, a scaled matvec output $\widehat{z}\in {\mathbb{C}}^r$ and an exactly represented nonnegative rational upper bound $\alpha$ satisfying $\mathrm{\parallel }\widehat{z}-cMz{\mathrm{\parallel }}_2\le \alpha$. This includes square matrix-vector products and the final Arnoldi basis projection.
• For a real scalar $c$ and vector $z\in {\mathbb{C}}^s$, a scaled-vector output $\widehat{q}\in {\mathbb{C}}^s$ and an exactly represented nonnegative rational upper bound $\xi$ satisfying $\mathrm{\parallel }\widehat{q}-cz{\mathrm{\parallel }}_2\le \xi$.
• For vectors $x,z\in {\mathbb{C}}^s$, a sum output $\widehat{s}\in {\mathbb{C}}^s$ and an exactly represented nonnegative rational upper bound $\zeta$ satisfying $\mathrm{\parallel }\widehat{s}-(x+z){\mathrm{\parallel }}_2\le \zeta$.

The bounds are part of the provider's mathematical contract and must enclose the exact norm errors for the supplied inputs. A call without a sound bound is uncertified and can only lead to an inconclusive status. This definition does not assert that a particular floating-point kernel supplies the contract.