原です。

>正木です。

>【定理】x, k を自然数で 2|k|x, k**4 <= 4*a とするとき、
>
>        N(x) = (x + a/x)/2
>
>    に対し次が成り立つ。
>
>        -1 < x/k - sqrt(a)/k <= 1 ならば 0 <= N(x) - sqrt(a) < 1.

仮定をできるだけ弱め、結論をできるだけ強くしているわけですね。

>【系】同じ前提条件で
>
>        0 <= x/k - [sqrt([a/k**2])] <= 1 ならば 0 <= [N(x)] - [sqrt(a)] <= 1.

こちらは今回の問題への適用ですね。


>    [sqrt([x])] = [sqrt(x)]

この証明なんですが、lg(x) という記法を調べていたら、クヌース他著の
「コンピュータの数学」(共立出版)で発見しました。で、そこにこの命
題がちょっと面白いフォーミュレーションででていました。

【命題】  f(x) が次の条件を満たすとする:

  (*) f は単調増加な連続関数で、整数の f の逆像は整数である。

  この時次が成り立つ:

   [f([x])] = [f(x)]

そしてこれの応用として

  [[x]/n] = [x/n]    (n は自然数)
  [sqrt([x])] = [sqrt(x)]

が出ていました。

命題の証明は、例えば (*) を

  (**) 任意の整数 n に対し半開区間 [n, n+1) の f による逆像は
       やはり整数端の半開区間 [a, b) である。

に弱めてしまった方が見通しがよくて、

   n = [f(x)]  <==>  f(x) は [n, n+1) に属する
               <==>  x は [a, b) に属する
               <==>  [x] は [a, b) に属する
               <==>  f([x]) は [n, n+1) に属する
               <==>  n = [f([x])]

です。