# 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 ,

rtz-sqrt

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

rtz-sqrt

(rtz-sqrt-bounds) Let and . If and , then

rtz-sqrt

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

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

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

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

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

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

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

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

PROOF: Let    rtz-sqrt. 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.

(rtz-rtz-sqrt) Let , . If and , then

rtz-sqrt   rtz-sqrt

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

rtz-sqrtrtz-sqrtrtz-sqrt

and we need only show that rtz-sqrt   rtz-sqrt. Let    rtz-sqrt and    rtz-sqrt. 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 2016-09-28