# 7.1  Truncated Square Root

The first step toward the definition of qsqrt is the following recursive function, the name of which is motivated by the (unproven) observation that for ,

Definition 7.1.1   (rtz-sqrt) Let and . If , then and if and , then

PROOF: If , then and the claim is trivial. Proceeding by induction, let , , and , and assume that . If , the claim follows trivially; otherwise, and

Corollary 7.1.2   (expo-rtz-sqrt) Let . If and , then .

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

PROOF: The claim is trivial for . Let , , and , and assume that is -exact, i.e., . Then either and or

(rtz-sqrt-square-bounds) Let and . Assume that and , and let . Then .

PROOF: The claim is trivial for . Let , , and assume that . If and , the claim is trivial. Otherwise, , , and

Accordoing to the next lemma, is uniquelt determined by the above properties.

(rtz-sqrt-unique) Let , , and . Assume that , , and . If is -exact and , then .

PROOF: Let . If , then by Lemmas4.2.16,

which implies , contradicting Lemma 7.1.4. But if , then

and by Lemma 7.1.4, , contradicting our hypothesis.

We have the following variation of Lemma 6.1.15.

PROOF: The case follows from Lemmas 6.1.10 and 7.1.3. We proceed by induction on . Let and assume that . Then by Lemma 6.1.15,

and we need only show that . Let and . If , then is -exact by Lemma 7.1.3 and by Lemma 6.1.10. But otherwise, , by Corollary 7.1.2, and hence, by Definition 6.1.1,

David Russinoff 2017-08-01