Exact dyadic bisection for square-root endpoints

Input: a nonnegative exact dyadic rational $x$ and integer request $n\ge 1$. Output: an exact dyadic lower and upper bound for $\sqrt{x}$; no finite storage format is needed by this procedure.

1. If $x=0$, return $[0,0]$.
2. Otherwise determine the unique integer $j$ with $2^j\le x<2^{j+1}$ from the exact dyadic representation, put $m=\lfloor j\mathrm{/}2\rfloor$ and $\delta =2^{m-n}$.
3. Set integer indices $L=0$ and $U=2^{n+1}$. While $U-L>1$, put $Q=\lfloor (L+U)\mathrm{/}2\rfloor$. If $(Q\delta {)}^2\le x$, replace $L$ by $Q$; otherwise replace $U$ by $Q$.
4. Return the exact dyadic pair $[L\delta ,U\delta ]$. A caller that stores these endpoints in a selected finite format must separately round the lower endpoint down and the upper endpoint up, propagating the resulting subnormal or overflow status.

All comparisons and multiplications in the loop are exact integer/dyadic operations.