Binary rounding grids, exact subtraction, and ordered TwoSum

Integer induction gives $2^n\ge n+1$ for $n\ge 0$: the initial equality is immediate and $2^{n+1}\ge 2(n+1)\ge n+2$. For $t>0$, [F1] supplies a natural $N>\max (t,1\mathrm{/}t,1)$, so $2^{-N}<t<2^N$. The finite set of integers $j\in [-N,N]$ with $2^j\le t$ is nonempty and has a largest element $E$; it satisfies $2^E\le t<2^{E+1}$. Strict increase of powers of two makes $E$ unique. Thus the stated $E(x)$ exists for every $x\mathrm{\ne }0$. In its binade, the finitely many points $m{2}^{E-p+1}$, $2^{p-1}\le m\le 2^p$, bracket $t$; their adjacent neighbors determine its nearest point. Points outside that bracket cannot be nearer, and zero is farther than a positive grid point; negative arguments follow by reflection. On a binade $[2^j,2^{j+1}]$, the nonnegative grid has spacing $2^{j-p+1}$. Its consecutive midpoints partition the real line into nearest-point cells, proving monotonicity and exactness on the grid; reflection preserves the even-significand tie rule, proving oddness. Every nonzero real number has two bracketing grid points, so a nearest point exists and is nonzero for a nonzero argument. The gaps on either side of a grid point $c\mathrm{\ne }0$ are at most $q(c)$, including the half-sized lower gap at a power of two. Its rounding cell therefore gives $\mathrm{\mid }R(t)-t\mathrm{\mid }\le q(R(t))\mathrm{/}2$. Also, for any power of two $h$, every integer multiple $nh$ with $\mathrm{\mid }n\mathrm{\mid }\le 2^p$ is in ${\mathbb{B}}_p$: the integer has at most $p$ significant bits, except $\mathrm{\mid }n\mathrm{\mid }=2^p$, which is a power of two.

Suppose $x,y\mathrm{\ne }0$ and $\mathrm{\mid }x\mathrm{\mid }\ge \mathrm{\mid }y\mathrm{\mid }$, and put $h=q(y)$. Both operands and their exact sum $t=x+y$ are integer multiples of $h$. Whenever $\mathrm{\mid }t\mathrm{\mid }\le \mathrm{\mid }y\mathrm{\mid }$, step 1.1 makes $t$ representable because $\mathrm{\mid }y\mathrm{\mid }<2^{p}h$. In particular, if $\mathrm{\mid }R(t)\mathrm{\mid }<\mathrm{\mid }y\mathrm{\mid }$, monotonicity and the fixed grid points $\pm \mathrm{\mid }y\mathrm{\mid }$ imply $\mathrm{\mid }t\mathrm{\mid }<\mathrm{\mid }y\mathrm{\mid }$, so $R(t)=t$. Otherwise $\mathrm{\mid }R(t)\mathrm{\mid }\ge \mathrm{\mid }y\mathrm{\mid }$, hence its binade spacing is an integer multiple of $h$, so $\rho =R(t)-t$ is an integer multiple of $h$. Since $x$ and $y$ themselves are candidate nearest points, $\mathrm{\mid }\rho \mathrm{\mid }\le \min (\mathrm{\mid }t-x\mathrm{\mid },\mathrm{\mid }t-y\mathrm{\mid })=\mathrm{\mid }y\mathrm{\mid }<2^{p}h$; step 1.1 makes $\rho$ representable. The zero-operand cases have $\rho =0$, and interchange handles the other magnitude order. This proves the second assertion, including the strict small-rounded-sum case.

For the subtraction assertion, change both signs and interchange operands so that $x\ge y>0$ and $x\le 2y$. Then $0\le x-y\le y$, and the grid argument in step 2.1, applied to $x$ and $-y$, shows that $x-y$ is representable. Reversing the transformations proves all same-sign cases; zero gives only the trivial zero pair.

For the ordered transform, if $A=0$ then $B=0$ and all outputs vanish. Otherwise oddness allows $A>0$. Since $0\le A+B\le 2A$ and $2A$ is representable, monotonicity gives $0\le S\le 2A$. If $B\ge -A\mathrm{/}2$, it also gives $S\ge A\mathrm{/}2$; step 3.1 then makes $S-A$ exact. If $B<-A\mathrm{/}2$, the operands $A$ and $-B$ meet step 3.1, so $S=A+B$ exactly and $S-A=B$ is exact as well. Thus always $Z=S-A=B+\rho$, where $\rho =S-(A+B)$. Step 2.1 makes $-\rho$ representable, so $T=R(B-Z)=-\rho =A+B-S$ exactly.