# 7.2  Odd-Rounded Square Root

The name of the following function is motivated by the (again unproven) observation that for ,

Definition 7.2.1   (rto-sqrt) Let and with , and let . Then

PROOF: If , then and the claim is trivial. Let and . By Lemma 7.1.1, , which implies

Corollary 7.2.2   (expo-rto-sqrt) Let . If and , then .

(exactp-rto-sqrt) Let and . If and , then is -exact.

PROOF: Let and . By Corollaries 7.1.2 and 7.2.2, . By Lemma 7.1.3, . Consequently, since is either or , , i.e., is -exact.

(rto-rto-sqrt) Let , , and . Assume that and . Then

PROOF: We first consider the case . Let , , , and . We shall show that . Note that by Lemmas 7.1.27.1.6, and 7.1.4, .

Case 1: and .Case 1: and .

. Since is -exact, Lemma 6.4.6 implies .

Case 2: and .

Since is -exact, Lemma 4.2.16 implies that is not -exact; similarly, since is -exact, is not -exact. Therefore,

Case 3: and .

By Lemma 7.1.3, is -exact and is -exact. By Lemma 7.1.6, , and it follows from Lemma 6.1.11 that . Thus, and by Lemma 6.4.6, .

Case 4: and .

In this case, and , which is not -exact. Thus,

The proof is completed by induction on . If , then by Lemma 6.4.11,

(rnd-rto-sqrt) Let , , , and . Assume that , , , and . Then

PROOF: Let and . Suppose . Then , , and hence . By Lemmas 6.4.7, 6.4.6, and 7.1.3,

Thus, we may assume and . By Lemma 7.1.4, , and hence . It follows from Lemmas 6.1.5, 6.1.9, and 4.2.16 that . Therefore,

To prove the second inequality, we note that if , then by Lemmas 6.4.7, 6.4.6, and 7.1.3,

Therefore, we may assume that . If , then , , and . Thus, by Lemma 7.1.4, and . Since , . It follows from Lemma 6.1.11 that . By Lemma 4.2.16, is not -exact, and hence

(exactp-cmp-rto-sqrt) Let , , and . Assume that , , , and is -exact. Then

(a) ;

(a) .

PROOF: Let and . If , then by Lemma 7.1.4, , so that and by Lemma 4.2.16,

We may assume, therefore, that , and hence . We must show that iff . By Lemma 4.2.16, . If , then and . If , then . Finally, if , then

David Russinoff 2017-08-01