TwoSum returns the exact rounding error of a floating point sum

Let $R$ denote unbounded binary nearest-even rounding from [F3]. On the closed normal range, bounded-format rounding equals $R$: the normal grid is identical, its endpoints are representable, and a point beyond either endpoint cannot beat that endpoint for an exact argument inside the range. Additional subnormal values cannot alter a nearest choice there. At a boundary power of two the normalized even significand gives the same tie choice; zero is exact. All inputs belong to ${\mathbb{B}}_p$. By [F2], induction over the six operations [F1] therefore identifies the actual successful computation with the same sequence using $R$. It suffices to prove its unbounded identity.

Put $\rho =s-(a+b)$. If $\mathrm{\mid }a\mathrm{\mid }\ge \mathrm{\mid }b\mathrm{\mid }$, the ordered transform [F3] gives $z=s-a$ and $R(b-z)=-\rho$ exactly. Consequently $v=R(s-z)=a$, $w=0$, $t=-\rho$, and $e=-\rho$. This includes $a=b=0$.

Suppose $\mathrm{\mid }a\mathrm{\mid }<\mathrm{\mid }b\mathrm{\mid }$. If $\mathrm{\mid }s\mathrm{\mid }<\mathrm{\mid }a\mathrm{\mid }$, the small-rounded-sum assertion [F3] makes $s=a+b$ exact. Then $z=b$, $v=a$, $w=t=e=0$ and $\rho =0$. For the remaining case $\mathrm{\mid }s\mathrm{\mid }\ge \mathrm{\mid }a\mathrm{\mid }$, apply the ordered transform to $(s,-a)$: it says $R(z-s)=z-s$ and $R(-a-(z-s))=(s-a)-z$. Oddness therefore gives $v=R(s-z)=s-z$ and $w=R(a-v)=z-(s-a)$ exactly. Writing $\sigma =z-(s-a)$, we have $w=\sigma$ and $z=b+\rho +\sigma$.

In this remaining case, oddness permits simultaneous sign reversal so that $b>0$. Since $\mathrm{\mid }a\mathrm{\mid }<b$, we have $0<a+b<2b$, and monotonicity gives $0<s\le 2b$. Thus $q(s)\le q(2b)=2q(b)$ and the rounding bound yields $\mathrm{\mid }\rho \mathrm{\mid }\le q(b)\le b\mathrm{/}2$, since $p\ge 2$. Also $\mathrm{\mid }\rho \mathrm{\mid }\le \mathrm{\mid }a\mathrm{\mid }<b$ by the addition-error bound. Therefore $b\mathrm{/}2\le s-a=b+\rho <2b$; monotonicity, fixing $b\mathrm{/}2$ and $2b$, gives $b\mathrm{/}2\le z\le 2b$. Sterbenz [F3] makes $t=R(b-z)=b-z=-\rho -\sigma$ exact. Finally $w+t=-\rho$ is representable by the addition-error assertion [F3], so $e=R(w+t)=-\rho$ exactly. Oddness gives the same conclusion before sign reversal.

The branches in steps 2.1, 2.2, and 3.1 cover every magnitude order and sign, and each gives $e=-\rho =(a+b)-s$. Step 1.1 transfers this identity to every successful finite-range call, proving $s+e=a+b$. A nonzero subnormal exact intermediate or overflow returns failure under [F2] and is outside the success conclusion; no extra hidden range assumption is used in any successful boundary case.