Dot-product cancellation under normal-range rounding

Given: The vectors, binary64 round-to-nearest ties-to-even arithmetic, unit roundoff $u=2^{-53}$, and the left-to-right evaluation order. Check the exact result, computed result, normal-range hypotheses, and gamma bound.

If $n\ge 1$, $nu<1$, and every exact product $x_j{y}_j$, rounded product $p_j:=\mathrm{fl}(x_j{y}_j)$, and intermediate sum lies in the normal range, the computed left-to-right dot product satisfies $\mathrm{\mid }\mathrm{fl}(x\cdot y)-x\cdot y\mathrm{\mid }\le {\gamma }_n{\sum }_j\mathrm{\mid }{x}_j{y}_j\mathrm{\mid }$, where ${\gamma }_n=nu\mathrm{/}(1-nu)$. (The computed floating-point dot product obeys componentwise and normwise error bounds)

The floating-point model uses relative error at most $u$ only on its stated normal-range operation domain; exact zero is handled separately. (The standard relative floating-point model and unit roundoff)

The final numerical error is $e_{\mathrm{f}\mathrm{p}}=\tilde{r}-r_m$ for the error ledger. (Successive statistical and computational error targets)

The total error along a finite scalar reference chain is the sum of its signed adjacent-stage errors. (Pathwise error decomposition along a reference chain)

In the binade $[2^{53},2^{54})$, a radix-two format with precision $53$ has spacing $2$. Since $2^{53}<{10}^{16}<2^{54}$, ${10}^{16}$ and ${10}^{16}+2$ are adjacent representable values. The lower significand is ${10}^{16}\mathrm{/}2=5000000000000000$, an even integer, whereas the upper significand is odd; therefore the exact midpoint ${10}^{16}+1$ rounds to ${10}^{16}$ under ties-to-even.