Solution (source code)

= Solution

One strong form of <Hensel lemma> is this: if $K$ is complete for a <discrete valuation> $v$, $f\in\mathcal O_K[X]$, and $a_0\in\mathcal O_K$ satisfies
$$
v(f(a_0))>2v(f'(a_0)),
$$
then there is a unique root $\alpha$ satisfying
$$
v(\alpha-a_0)>v(f'(a_0)).
$$

Define the <Newton iteration over a valued field>
$$
a_{n+1}=a_n-\frac{f(a_n)}{f'(a_n)}.
$$
Taylor expansion and the <ultrametric inequality> show inductively that $v(f'(a_n))=v(f'(a_0))$ and
$$
v(f(a_{n+1}))\geq2v(f(a_n))-2v(f'(a_0)).
$$
Thus the valuations of the corrections $a_{n+1}-a_n$ tend to infinity, so $(a_n)$ is a <Cauchy sequence>. <Completeness> gives a limit $\alpha$, and <continuity> gives $f(\alpha)=0$. If $\beta$ is another root in the stated ball, Taylor expansion of $f(\beta)-f(\alpha)$ shows that the linear term has strictly smaller valuation than all higher terms unless $\beta=\alpha$, proving uniqueness.