[proofplan] We prove the contrapositive: if some intermediate coefficient has absolute value exceeding $\max(|a_0|, |a_n|)$, then $f$ is reducible. After normalising $f$ to be primitive (so $\max_\ell |a_\ell| = 1$), the hypothesis $\max(|a_0|, |a_n|) < 1$ means both the constant and leading terms vanish in the reduction $\bar{f} \in k_K[x]$. Locating the smallest index $r$ with $|a_r| = 1$ produces a factorisation $\bar{f}(x) = x^r \cdot \bar{q}(x)$ with $\bar{q}(0) = \bar{a}_r \neq 0$, so $\gcd(x^r, \bar{q}) = 1$. Hensel's Lemma then lifts this to a non-trivial factorisation of $f$ over $\mathcal{O}_K$, contradicting irreducibility. [/proofplan] [step:Reduce to the case where $f$ is primitive with $\max(|a_0|, |a_n|) < 1$] We prove the contrapositive: assume $|a_\ell| > \max(|a_0|, |a_n|)$ for some $0 < \ell < n$, and show $f$ is reducible. Define $M := \max_{0 \leq i \leq n} |a_i|$. Since $|a_\ell| > 0$, we have $M > 0$. Replacing $f$ by $M^{-1} f$ (which does not change irreducibility, since $M^{-1} \in K^\times$ is a unit) produces a polynomial with $\max_i |a_i| = 1$, i.e., a primitive polynomial. Moreover, scaling all coefficients by $M^{-1}$ preserves the inequality $|a_\ell| > \max(|a_0|, |a_n|)$ (all absolute values are divided by $M$). After this normalisation, $f \in \mathcal{O}_K[x]$ is primitive with $\max_i |a_i| = 1$. The hypothesis $|a_\ell| > \max(|a_0|, |a_n|)$ together with $|a_\ell| \leq 1$ gives $\max(|a_0|, |a_n|) < 1$, i.e., both $a_0$ and $a_n$ lie in $\mathfrak{m}_K$. [/step] [step:Locate the smallest index $r$ with $|a_r| = 1$ and factor the reduction $\bar{f}$] Since $f$ is primitive, $\max_i |a_i| = 1$, so there exists at least one index with $|a_i| = 1$. Since $|a_0| < 1$ and $|a_n| < 1$, every such index satisfies $0 < i < n$. Let \begin{align*} r := \min\{i : |a_i| = 1\}. \end{align*} By the preceding observation, $0 < r < n$. In the reduction $\bar{f} \in k_K[x]$, the coefficients $\bar{a}_0 = \bar{a}_1 = \cdots = \bar{a}_{r-1} = 0$ (since $|a_i| < 1$ for $i < r$, meaning $a_i \in \mathfrak{m}_K$), and $\bar{a}_r \neq 0$ (since $|a_r| = 1$, meaning $a_r \in \mathcal{O}_K^\times$). Therefore \begin{align*} \bar{f}(x) = x^r \bigl(\bar{a}_r + \bar{a}_{r+1} x + \cdots + \bar{a}_n x^{n-r}\bigr) =: x^r \cdot \bar{q}(x). \end{align*} We verify $\gcd(x^r, \bar{q}) = 1$ in $k_K[x]$. The polynomial $x^r$ has $0$ as its only root (with multiplicity $r$). For $\bar{q}$, we compute $\bar{q}(0) = \bar{a}_r \neq 0$, so $0$ is not a root of $\bar{q}$. Since every irreducible factor of $x^r$ is (a power of) $x$, and $x \nmid \bar{q}$, we conclude $\gcd(x^r, \bar{q}) = 1$. [guided] The strategy is to find a coprime factorisation of the reduction $\bar{f}$ so that Hensel's Lemma applies. Since $|a_0| < 1$ and $|a_n| < 1$, both the constant and leading coefficients vanish in the reduction. But $f$ is primitive, so $\max_i |a_i| = 1$, meaning at least one coefficient survives the reduction. Let $r$ be the first index where this happens: $r = \min\{i : |a_i| = 1\}$. Then $\bar{f}(x) = 0 + 0 \cdot x + \cdots + 0 \cdot x^{r-1} + \bar{a}_r x^r + \cdots = x^r(\bar{a}_r + \bar{a}_{r+1}x + \cdots)$. The factor $\bar{q}(x) = \bar{a}_r + \bar{a}_{r+1}x + \cdots$ has nonzero constant term $\bar{a}_r$, so $\bar{q}(0) \neq 0$. This means $x \nmid \bar{q}(x)$, and since $x^r = x \cdot x \cdots x$ (all irreducible factors are $x$), we get $\gcd(x^r, \bar{q}) = 1$. Why do we need $0 < r < n$? If $r = 0$, then $|a_0| = 1$, contradicting $|a_0| < 1$. If $r = n$, then $|a_n| = 1$, contradicting $|a_n| < 1$. So $r$ is an interior index, and $\bar{f} = x^r \bar{q}$ is a non-trivial factorisation with $\deg(x^r) = r \geq 1$ and $\deg(\bar{q}) = n - r \geq 1$. [/guided] [/step] [step:Apply Hensel's Lemma to lift the factorisation and conclude reducibility] The polynomial $f \in \mathcal{O}_K[x]$ is primitive, and $\bar{f} = x^r \cdot \bar{q}$ is a coprime factorisation in $k_K[x]$ with $\deg(x^r) = r$ and $1 \leq r \leq n - 1$. By [Hensel's Lemma](/theorems/???), there exists a factorisation $f = g \cdot h$ in $\mathcal{O}_K[x]$ with $g \equiv x^r \pmod{\mathfrak{m}_K}$, $h \equiv \bar{q} \pmod{\mathfrak{m}_K}$, and $\deg g = r$. Since $1 \leq r \leq n - 1$, both $g$ and $h$ have degree at least 1 and at most $n - 1$. Therefore $f = g \cdot h$ is a non-trivial factorisation of $f$ over $\mathcal{O}_K[x] \subset K[x]$, so $f$ is reducible over $K$. This contradicts the assumption that $f$ is irreducible. Therefore the original inequality $|a_\ell| > \max(|a_0|, |a_n|)$ cannot hold for any $\ell$, completing the proof. [guided] [Hensel's Lemma](/theorems/???) requires three inputs: (i) $f$ is primitive over $\mathcal{O}_K$, (ii) the reduction $\bar{f}$ factors as a product of two polynomials in $k_K[x]$, and (iii) these two factors are coprime. We have verified all three: $f$ is primitive by normalisation, $\bar{f} = x^r \cdot \bar{q}$, and $\gcd(x^r, \bar{q}) = 1$. Hensel's Lemma then produces $g, h \in \mathcal{O}_K[x]$ with $f = gh$, $\deg g = r$, and the reductions matching. Since $1 \leq r \leq n - 1$, both factors are non-constant, giving a non-trivial factorisation of $f$ over $K[x]$. This is where completeness is essential. Without completeness of $K$, Hensel's Lemma fails: the iterative construction in Hensel's proof produces Cauchy sequences of coefficients that need not converge in an incomplete field. For example, $x^2 + 1$ is irreducible over $\mathbb{Q}$ even though its reduction modulo 5 factors as $(x - 2)(x + 2)$ with coprime factors. The issue is that $\mathbb{Q}$ is not complete with respect to $|\cdot|_5$; over $\mathbb{Q}_5$, the polynomial does factor (as guaranteed by Hensel), with roots $\pm\sqrt{-1} \in \mathbb{Q}_5$. [/guided] [/step]