正木です。

|原です。

|おお。証明も公開してもらえません?


もしかして何か勘違いしていて、間違いを指摘してもらえるかも知れ
ないので一応概略を書いておきます。
----

2 ** (4*n) <= a < 2**(4*n + 4)   , (n > 1)

と仮定して

b = a >> 2*n

x = b.isqrt_ini << n

と置く。

b.isqrt_ini に関する帰納法の仮定で

|b.isqrt_ini - sqrt(b)| < 1    (sqrt は本来の平方根:実数)

a の平方根の範囲は

sqrt(b)*2**n <= sqrt(a) < sqrt(b + 1) * 2**n 

n > 1 ならば b >= 4 なので

sqrt(b+1) - sqrt(b) < 1/4

|b.isqrt_ini - sqrt(b + 1)| < 5/4

となり、 x の誤差は

| x - sqrt(a)| < 5/4 * 2 ** n  

とおさえられる。有理数での Newton 法の近似

y = (x + a/x)/2      (y は有理数)

に対して

0 <=  y - sqrt(a) == (x - sqrt(a))**2/(2*x) < ((5/4)**2)/2 < 1

sqrt(a) <= y < sqrt(a) + 1

したがって

a.isqrt <= y.floor < a.isqrt + 1

Q.E.D.