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
,

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

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

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.

PROOF: Let
*rtz-sqrt*. If , then by Lemmas4.2.16,

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
*rtz-sqrt* *rtz-sqrt*. Then by Lemma 6.1.15,

David Russinoff 2016-09-28