Newton iteration for a square root (source code)

= Newton iteration for a square root
{c}
{title2=$a_{n+1}=\frac12(a_n+c/a_n)$}

For $c>0$ and $a_0>0$, the displayed <recurrence relation> stays positive and satisfies
$$
a_{n+1}^2-c=\frac{(a_n^2-c)^2}{4a_n^2}\geq0.
$$
After the first step, $a_n^2\geq c$, so $a_{n+1}-a_n=(c-a_n^2)/(2a_n)\leq0$. The <bounded monotone sequence theorem> gives a <limit of a sequence> $L\geq0$; the inequality $L^2\geq c>0$ makes $L$ positive, and passage to the <limit of a sequence> in the <recurrence relation> gives $L^2=c$. This proves existence of the positive <square root> without assuming it in the construction. Once $s=\sqrt c$ is known, the exact error identity $a_{n+1}-s=(a_n-s)^2/(2a_n)$ explains the eventual <quadratic convergence>.