[proofplan] We prove Hensel's Lemma by iterative refinement. Starting from arbitrary lifts $g_0, h_0 \in \mathcal{O}_K[x]$ of the coprime factors $\bar{g}, \bar{h}$ of the reduction $\bar{f}$, we construct sequences $(g_k)$ and $(h_k)$ in $\mathcal{O}_K[x]$ satisfying $f \equiv g_k h_k \pmod{\pi^{k+1}}$ (where $\pi$ is a uniformiser), with $\deg g_k = \deg \bar{g}$ and each pair differing from the previous by a correction of order $\pi^k$. The coprimality of $\bar{g}$ and $\bar{h}$ provides a Bezout relation that drives the Newton-type iteration. By the completeness of $K$, the coefficient sequences converge, producing the desired factorisation $f = gh$ in $\mathcal{O}_K[x]$. [/proofplan] [step:Set up notation: uniformiser, lifts, and the initial Bezout relation] Let $\pi \in \mathfrak{m}_K$ be a uniformiser, i.e., a generator of the maximal ideal $\mathfrak{m}_K$ of $\mathcal{O}_K$, so that $\mathfrak{m}_K = \pi \mathcal{O}_K$ and $|\pi| = \max\{|x| : x \in \mathfrak{m}_K, |x| < 1\}$. Let $k_K = \mathcal{O}_K / \mathfrak{m}_K$ be the residue field, and let the reduction map $\mathcal{O}_K[x] \to k_K[x]$ be denoted by $f \mapsto \bar{f}$. Choose lifts $g_0, h_0 \in \mathcal{O}_K[x]$ of $\bar{g}$ and $\bar{h}$ with $\deg g_0 = \deg \bar{g}$ and $g_0$ monic (we may take $g_0$ monic since $\bar{g}$ divides $\bar{f}$ and we can adjust the leading coefficient; more precisely, since $f$ is primitive, its leading coefficient is a unit in $\mathcal{O}_K$, and we normalise so that $g_0$ has the same degree as $\bar{g}$ with leading coefficient a unit). Set $d = \deg \bar{g}$ and $e = \deg f - d$. Since $\gcd(\bar{g}, \bar{h}) = 1$ in $k_K[x]$, there exist $\bar{a}, \bar{b} \in k_K[x]$ with $\bar{a}\bar{g} + \bar{b}\bar{h} = 1$. Lift these to $a_0, b_0 \in \mathcal{O}_K[x]$ so that \begin{align*} a_0 g_0 + b_0 h_0 \equiv 1 \pmod{\pi}. \end{align*} Since $f$ is primitive (at least one coefficient is a unit in $\mathcal{O}_K$) and $\bar{f} = \bar{g}\bar{h}$, we have $f \equiv g_0 h_0 \pmod{\pi}$. Write $f - g_0 h_0 = \pi r_0$ with $r_0 \in \mathcal{O}_K[x]$. [guided] We set up the iteration that will produce the factorisation. The key algebraic input is the Bezout relation $\bar{a}\bar{g} + \bar{b}\bar{h} = 1$ in the residue field, which reflects the coprimality of $\bar{g}$ and $\bar{h}$. Why do we need a uniformiser $\pi$? The maximal ideal $\mathfrak{m}_K$ of the valuation ring $\mathcal{O}_K$ is principal (generated by any element of maximal absolute value less than $1$). Working modulo powers of $\pi$ gives us a filtration $\mathcal{O}_K \supset \pi\mathcal{O}_K \supset \pi^2\mathcal{O}_K \supset \cdots$ that replaces the role of $p, p^2, p^3, \ldots$ in the classical $p$-adic setting. The initial data is: $f \equiv g_0 h_0 \pmod{\pi}$ (approximate factorisation modulo $\pi$), and $a_0 g_0 + b_0 h_0 \equiv 1 \pmod{\pi}$ (Bezout relation that will allow us to "solve" for corrections). The goal of the iteration is to improve the factorisation from $\pmod{\pi}$ to $\pmod{\pi^2}$, then $\pmod{\pi^3}$, and so on. [/guided] [/step] [step:Perform one step of the iterative refinement from $\pmod{\pi^{k+1}}$ to $\pmod{\pi^{k+2}}$] Suppose by induction we have $g_k, h_k \in \mathcal{O}_K[x]$ with: - $\deg g_k = d$ (with $g_k$ monic of degree $d$), - $f \equiv g_k h_k \pmod{\pi^{k+1}}$, - $g_k \equiv g_0 \pmod{\pi}$ and $h_k \equiv h_0 \pmod{\pi}$. Write $f - g_k h_k = \pi^{k+1} r_k$ with $r_k \in \mathcal{O}_K[x]$. We seek $s_k, t_k \in \mathcal{O}_K[x]$ with $\deg s_k < d$ such that \begin{align*} g_{k+1} &:= g_k + \pi^{k+1} s_k, \\ h_{k+1} &:= h_k + \pi^{k+1} t_k, \end{align*} and $f \equiv g_{k+1} h_{k+1} \pmod{\pi^{k+2}}$. Expanding the product: \begin{align*} g_{k+1} h_{k+1} &= g_k h_k + \pi^{k+1}(g_k t_k + h_k s_k) + \pi^{2(k+1)} s_k t_k. \end{align*} Since $2(k+1) \geq k+2$ for all $k \geq 0$, the last term vanishes modulo $\pi^{k+2}$. So we need \begin{align*} \pi^{k+1} r_k \equiv \pi^{k+1}(g_k t_k + h_k s_k) \pmod{\pi^{k+2}}, \end{align*} i.e., $r_k \equiv g_k t_k + h_k s_k \pmod{\pi}$, i.e., $\bar{r}_k = \bar{g}\bar{t}_k + \bar{h}\bar{s}_k$ in $k_K[x]$. Multiply the Bezout relation $\bar{a}\bar{g} + \bar{b}\bar{h} = 1$ by $\bar{r}_k$: $(\bar{a}\bar{r}_k)\bar{g} + (\bar{b}\bar{r}_k)\bar{h} = \bar{r}_k$. Perform the Euclidean division of $\bar{b}\bar{r}_k$ by $\bar{g}$: write $\bar{b}\bar{r}_k = \bar{g}\bar{q} + \bar{s}$ with $\deg \bar{s} < d$. Then \begin{align*} \bar{r}_k = \bar{g}(\bar{a}\bar{r}_k + \bar{h}\bar{q}) + \bar{h}\bar{s}. \end{align*} Set $\bar{t}_k = \bar{a}\bar{r}_k + \bar{h}\bar{q}$ and $\bar{s}_k = \bar{s}$, and lift to $t_k, s_k \in \mathcal{O}_K[x]$ with $\deg s_k < d$. **Degree control:** $\deg g_{k+1} = d$ because $g_{k+1} = g_k + \pi^{k+1} s_k$ with $\deg s_k < d = \deg g_k$, and $g_k$ is monic of degree $d$, so the leading term is unchanged. [guided] This is the core of the Newton-type iteration. The problem reduces to: given the error $r_k = (f - g_k h_k)/\pi^{k+1}$, find corrections $s_k$ and $t_k$ such that $\bar{r}_k = \bar{g}\bar{t}_k + \bar{h}\bar{s}_k$ in $k_K[x]$. Why does the Bezout relation help? The coprimality $\gcd(\bar{g}, \bar{h}) = 1$ gives us $\bar{a}\bar{g} + \bar{b}\bar{h} = 1$, so multiplying by $\bar{r}_k$ gives a decomposition $\bar{r}_k = (\bar{a}\bar{r}_k)\bar{g} + (\bar{b}\bar{r}_k)\bar{h}$. However, the polynomial $\bar{b}\bar{r}_k$ paired with $\bar{h}$ might have degree $\geq d$, which would cause $\deg s_k \geq d$ and ruin the degree control on $g_{k+1}$. The fix is the Euclidean division: divide $\bar{b}\bar{r}_k$ by $\bar{g}$ to get $\bar{b}\bar{r}_k = \bar{g}\bar{q} + \bar{s}$ with $\deg \bar{s} < d$. The quotient $\bar{q}$ is absorbed into $\bar{t}_k$ (it contributes $\bar{h}\bar{g}\bar{q}$ which is paired with $\bar{g}$). After this rebalancing, we get $\bar{r}_k = \bar{g}\bar{t}_k + \bar{h}\bar{s}_k$ with $\deg \bar{s}_k < d$, which is exactly what we need. The degree constraint $\deg s_k < d$ is crucial: it ensures that $g_{k+1} = g_k + \pi^{k+1} s_k$ has the same degree $d$ as $g_k$ (and the same leading coefficient, since the correction $\pi^{k+1} s_k$ has degree $< d$). What about the cross term $\pi^{2(k+1)} s_k t_k$? Since $2(k+1) \geq k + 2$, this term is at least of order $\pi^{k+2}$ and vanishes in the next approximation. This is the "quadratic convergence" feature of Newton's method, though here we only use it to get single-step improvement (the error shrinks from $\pi^{k+1}$ to $\pi^{k+2}$, which is linear convergence in the $\pi$-adic sense, sufficient because we iterate infinitely many times). [/guided] [/step] [step:Verify the inductive hypotheses propagate] We verify that $g_{k+1}$ and $h_{k+1}$ satisfy the inductive hypotheses: 1. **Degree:** $\deg g_{k+1} = d$ (shown above, since $\deg s_k < d$ and the leading coefficient of $g_k$ is a unit unaffected by the lower-degree correction). 2. **Approximate factorisation:** $f - g_{k+1}h_{k+1} = f - g_k h_k - \pi^{k+1}(g_k t_k + h_k s_k) - \pi^{2(k+1)} s_k t_k = \pi^{k+1}(r_k - g_k t_k - h_k s_k) - \pi^{2(k+1)} s_k t_k$. By construction, $r_k - g_k t_k - h_k s_k \equiv 0 \pmod{\pi}$ (since $\bar{r}_k = \bar{g}\bar{t}_k + \bar{h}\bar{s}_k$), so $r_k - g_k t_k - h_k s_k = \pi w_k$ for some $w_k \in \mathcal{O}_K[x]$. Therefore \begin{align*} f - g_{k+1} h_{k+1} = \pi^{k+2} w_k - \pi^{2(k+1)} s_k t_k = \pi^{k+2}(w_k - \pi^k s_k t_k), \end{align*} so $f \equiv g_{k+1} h_{k+1} \pmod{\pi^{k+2}}$. 3. **Congruence to initial lifts:** $g_{k+1} = g_k + \pi^{k+1} s_k \equiv g_k \equiv g_0 \pmod{\pi}$, and similarly $h_{k+1} \equiv h_0 \pmod{\pi}$. 4. **Successive closeness:** $g_{k+1} \equiv g_k \pmod{\pi^{k+1}}$ and $h_{k+1} \equiv h_k \pmod{\pi^{k+1}}$. [/step] [step:Take the limit using completeness of $K$] The iteration produces sequences $(g_k)_{k \geq 0}$ and $(h_k)_{k \geq 0}$ in $\mathcal{O}_K[x]$ with $g_{k+1} \equiv g_k \pmod{\pi^{k+1}}$ and $h_{k+1} \equiv h_k \pmod{\pi^{k+1}}$. For each coefficient index $j$ (where $0 \leq j \leq d$ for $g_k$ and $0 \leq j \leq e$ for $h_k$), the $j$-th coefficient of $g_k$ forms a Cauchy sequence in $\mathcal{O}_K$: the $j$-th coefficients of $g_{k+1}$ and $g_k$ differ by an element of $\pi^{k+1}\mathcal{O}_K$, so their distance is at most $|\pi|^{k+1} \to 0$. Since $K$ is complete and $\mathcal{O}_K$ is closed in $K$ (as the closed unit ball), each coefficient sequence converges to an element of $\mathcal{O}_K$. Define \begin{align*} g &:= \lim_{k \to \infty} g_k \in \mathcal{O}_K[x], \\ h &:= \lim_{k \to \infty} h_k \in \mathcal{O}_K[x], \end{align*} where the limits are taken coefficient-wise. **Degree:** Since each $g_k$ is monic of degree $d$ and the leading coefficient is $1$ for all $k$, the limit $g$ is monic of degree $d$. For $h$: each $h_k$ has degree $\leq e = \deg f - d$, and the limit $h$ has degree $\leq e$. **Factorisation:** For each $k$, $|f - g_k h_k|_{\sup} \leq |\pi|^{k+1}$, where $|\cdot|_{\sup}$ denotes the supremum of the absolute values of the coefficients. Since $g_k \to g$ and $h_k \to h$ coefficient-wise, and multiplication of polynomials is continuous in the coefficient topology, $g_k h_k \to gh$ coefficient-wise. Therefore $|f - gh|_{\sup} = \lim_{k \to \infty} |f - g_k h_k|_{\sup} = 0$, giving $f = gh$. **Reduction:** $g \equiv g_0 \equiv \bar{g} \pmod{\pi}$ and $h \equiv h_0 \equiv \bar{h} \pmod{\pi}$. [guided] The passage to the limit is where the completeness hypothesis is used. Each coefficient of $g_k$ forms a Cauchy sequence in $\mathcal{O}_K$: the difference between successive terms lies in $\pi^{k+1}\mathcal{O}_K$, so the distance is at most $|\pi|^{k+1}$. In a non-archimedean setting, this is more than enough for the Cauchy property: the series $\sum_{k=0}^{\infty}(g_{k+1} - g_k)$ converges because $|g_{k+1} - g_k|_{\sup} \leq |\pi|^{k+1} \to 0$ (by the [Convergence via Term Decay](/theorems/???) theorem applied to each coefficient). The degree of $g$ requires care. Each $g_k$ has leading coefficient $1$ in degree $d$ (monic of degree $d$). The limit preserves this: the coefficient of $x^d$ in $g$ is $\lim_{k \to \infty} 1 = 1$, and for $j > d$, the coefficient is $\lim_{k \to \infty} 0 = 0$. So $g$ is monic of degree $d = \deg \bar{g}$. For the factorisation $f = gh$: the key point is that polynomial multiplication is a finite sum of products of coefficients, hence continuous in the coefficient topology. Since $g_k h_k \to gh$ and $g_k h_k \to f$ (because $|f - g_k h_k|_{\sup} \to 0$), we conclude $f = gh$ by the uniqueness of limits. [/guided] [/step]