7.2  Odd-Rounded Square Root

The name of the following function is motivated by the (again unproven) observation that for $ \frac{1}{4} \leq x < 1$,

$\displaystyle \mathit{rto\mbox{-}sqrt}(x, n) = \mathit{RTO}(\sqrt{x}, n).
$

Definition 7.2.1   (rto-sqrt) Let $ x \in \mathbb{R}$ and $ n \in \mathbb{N}$ with $ n > 0$, and let $ z = \mathit{rtz\mbox{-}sqrt}(x,n-1)$. Then

$\displaystyle \mathit{rto\mbox{-}sqrt}(x,n) = \left\{\begin{array}{ll}
z & \mbox{if $x \leq z*2$}\\
z + 2^{-n} & \mbox{if $x > z^2$.}\end{array}\right.
$

  (rto-sqrt-bounds) Let $ x \in \mathbb{Q}$ and $ n \in \mathbb{N}$. If $ x \geq \frac{1}{4}$ and $ n > 0$, then

$\displaystyle \frac{1}{2} \leq \mathit{rto\mbox{-}sqrt}(x,n) \leq 1 - 2^{-n}.
$

PROOF: If $ n=1$, then $ \mathit{rto\mbox{-}sqrt}(x,n) = \frac{1}{2}$ and the claim is trivial. Let $ n>1$ and $ z = \mathit{rtz\mbox{-}sqrt}(x,n-1)$. By Lemma 7.1.1, $ \frac{1}{2} \leq z < 1$, which implies

$\displaystyle \frac{1}{2} \leq z \leq \mathit{rto\mbox{-}sqrt}(x,n) \leq z + 2^{-n} \leq (1 - 2^{1-n}) + 2^{-n} = 1 - 2^{-n}. \mbox{$\Box$}
$

Corollary 7.2.2   (expo-rto-sqrt) Let $ x \in \mathbb{Q}$ $ n \in \mathbb{N}$. If $ x \geq \frac{1}{4}$ and $ n > 0$, then $ \mathit{expo}(\mathit{rto\mbox{-}sqrt}(x,n)) = -1$.

  (exactp-rto-sqrt) Let $ x \in \mathbb{Q}$ and $ n \in \mathbb{N}$. If $ x \geq \frac{1}{4}$ and $ n > 0$, then $ \mathit{rto\mbox{-}sqrt}(x,n)$ is $ n$-exact.

PROOF: Let $ z = \mathit{rtz\mbox{-}sqrt}(x,n-1)$ and $ w = \mathit{rto\mbox{-}sqrt}(x,n)$. By Corollaries 7.1.2 and 7.2.2, $ \mathit{expo}(z) = \mathit{expo}(w) = -1$. By Lemma 7.1.3, $ 2^{n-1}z \in \mathbb{Z}$. Consequently, since $ w$ is either $ z$ or $ z + 2^{-n}$, $ 2^nw \in \mathbb{Z}$, i.e., $ w$ is $ n$-exact. 

  (rto-rto-sqrt) Let $ x \in \mathbb{Q}$, $ m \in \mathbb{N}$, and $ n \in \mathbb{N}$. Assume that $ \frac{1}{4} \leq x < 1$ and $ 2 \leq n \leq m$. Then

$\displaystyle \mathit{rto}(\mathit{rto\mbox{-}sqrt}(x,m), n) = \mathit{rto\mbox{-}sqrt}(x, n).
$

PROOF: We first consider the case $ n = m-1$. Let $ z_1 = \mathit{rtz\mbox{-}sqrt}(x, m-2)$, $ w_1 = \mathit{rto\mbox{-}sqrt}(x, m-1)$, $ z_2 = \mathit{rtz\mbox{-}sqrt}(x, m-1)$, and $ w_2 = \mathit{rto\mbox{-}sqrt}(x, m)$. We shall show that $ \mathit{rto}(w_2, m-1) = w_1$. Note that by Lemmas 7.1.27.1.6, and 7.1.4, $ \frac{1}{2} \leq z_1^2 \leq z_2^2 \leq x$.

Case 1: $ z_1 = z_2$ and $ z_2^2 < x$.Case 1: $ z_1 = z_2$ and $ z_2^2 = x$.

$ z_1 = w_1 = z_2 = w_2$. Since $ w_2$ is $ (m-1)$-exact, Lemma 6.4.6 implies $ \mathit{rto}(w_2, m-1) = w_2 = w_1$.

Case 2: $ z_1 = z_2$ and $ z_2^2 < x$.

Since $ w_1$ is $ (m-2)$-exact, Lemma 4.2.16 implies that $ w_1 = z_1 + 2^{1-n}$ is not $ (m-2)$-exact; similarly, since $ w_2$ is $ (m-1)$-exact, $ w_2 = z_2 + 2^{-m}$ is not $ (m-1)$-exact. Therefore,

$\displaystyle \mathit{rto}(w_2, m-1) = \mathit{RTZ}(w_2, m-2) + 2^{1-n} = z_1 + 2^{1-m} = w_1.
$

Case 3: $ z_1 < z_2$ and $ z_2^2 = x$.

By Lemma 7.1.3, $ z_1$ is $ (m-1)$-exact and $ z_2$ is $ (m-2)$-exact. By Lemma 7.1.6, $ z_1 = \mathit{RTZ}(z_2, m-2) < z_2$, and it follows from Lemma 6.1.11 that $ z_2 = z_1 + 2^{1-m}$. Thus, $ w_1 = z_2 = w_2$ and by Lemma 6.4.6, $ \mathit{rto}(w_2, m-1) = w_2 = w_1$.

Case 4: $ z_1 < z_2$ and $ z_2^2 < x$.

In this case, $ w_1 = z_2 = z_1 + 2^{1-m}$ and $ w_2 = z_2 + 2^{-m} = z_1 + 2^{1-m} + 2^{-m}$, which is not $ (m-2)$-exact. Thus,

$\displaystyle \mathit{rto}(w_2, m-1) = \mathit{RTZ}(w_2, m-2) + 2^{1-m} = z_1 + 2^{1-m} = w_1.
$

The proof is completed by induction on $ m$. If $ m>n$, then by Lemma 6.4.11,

$\displaystyle \mathit{rto}(\mathit{rto\mbox{-}sqrt}(x,m), n)$ $\displaystyle =$ $\displaystyle \mathit{rto}(\mathit{rto}(\mathit{rto\mbox{-}sqrt}(x,m), m-1), n)$  
  $\displaystyle =$ $\displaystyle \mathit{rto}(\mathit{rto\mbox{-}sqrt}(x,m-1), n)$  
  $\displaystyle =$  

  (rnd-rto-sqrt) Let $ x \in \mathbb{Q}$, $ \ell \in \mathbb{Q}$ , $ h \in \mathbb{Q}$, and $ n \in \mathbb{N}$. Assume that $ \frac{1}{4} \leq x < 1$, $ n > 0$, $ h>0$, and $ \ell^2 \leq x \leq h^2$. Then

$\displaystyle \mathit{rto}(\ell,n) \leq \mathit{rto\mbox{-}sqrt}(x,n) \leq \mathit{rto}(h,n).
$

PROOF: Let $ z = \mathit{rtz\mbox{-}sqrt}(x,n-1)$ and $ w = \mathit{rto\mbox{-}sqrt}(x,n)$. Suppose $ z^2 = x$. Then $ w = z$, $ \ell^2 \leq x = w^2$, and hence $ \ell \leq w$. By Lemmas 6.4.7, 6.4.6, and 7.1.3,

$\displaystyle \mathit{rto}(l, n) \leq \mathit{rto}(w, n) = w.
$

Thus, we may assume $ z^2 < x$ and $ w = z + 2^{-n}$. By Lemma 7.1.4, $ \ell^2 \leq x < w^2$, and hence $ \ell < w = fp^+(z, n-1)$. It follows from Lemmas 6.1.5, 6.1.9, and 4.2.16 that $ \mathit{RTZ}(\ell, n-1) \leq z$. Therefore,

$\displaystyle \mathit{rto}(\ell, n) \leq \mathit{RTZ}(\ell, n-1) + 2^{1+expo(\ell)-n} \leq z + 2^{-n} = w.
$

To prove the second inequality, we note that if $ h \geq w$, then by Lemmas 6.4.7, 6.4.6, and 7.1.3,

$\displaystyle \mathit{rto}(h, n) \geq \mathit{rto}(w, n) = w.
$

Therefore, we may assume that $ h < w$. If $ z^2 = x$, then $ w = z$, $ h^2 \geq x = w^2$, and $ h \geq w$. Thus, by Lemma 7.1.4, $ z^2 < x$ and $ w = z + 2^{-n} = fp^+(z, n-1)$. Since $ h^2 \geq x > z^2$, $ h > z$. It follows from Lemma 6.1.11 that $ \mathit{RTZ}(h, n-1) \geq a$. By Lemma 4.2.16, $ h$ is not $ n$-exact, and hence

$\displaystyle \mathit{rto}(h, n) = \mathit{RTZ}(h, n-1) + 2^{-n} \geq z + 2^{-n} = w. $

  (exactp-cmp-rto-sqrt) Let $ x \in \mathbb{Q}$, $ q \in \mathbb{Q}$, and $ n \in \mathbb{N}$. Assume that $ \frac{1}{4} \leq x < 1$, $ q>0$, $ N>0$, and $ q$ is $ (n-1)$-exact. Then

(a) $ q^2 < x \Leftrightarrow q < \mathit{rto\mbox{-}sqrt}(x,n)$;

(a) $ q^2 > x \Leftrightarrow q > \mathit{rto\mbox{-}sqrt}(x,n)$.

PROOF: Let $ z = \mathit{rtz\mbox{-}sqrt}(x,n-1)$ and $ w = \mathit{rto\mbox{-}sqrt}(x,n)$. If $ q^2 > x$, then by Lemma 7.1.4, $ q^2 > z^2$, so that $ q > z$ and by Lemma 4.2.16,

$\displaystyle q \geq z + 2^{1-n} > z + 2^{-n} \geq w.
$

We may assume, therefore, that $ q^2 \leq x < (z + 2^{-n})^2$, and hence $ q < z + 2^{-n}$. We must show that $ q < x^2$ iff $ q < w$. By Lemma 4.2.16, $ q \leq z$. If $ q < z$, then $ q < x^2$ and $ q < w$. If $ q = z = x^2$, then $ q = z = w$. Finally, if $ q = z < x^2$, then $ q = z < z + 2^{-n} = w$

David Russinoff 2017-08-01