[proofplan] We prove by induction on $n$ that $f_n$ has no repeated roots. The key tool is the formal derivative: $f_n$ has a repeated root at $\alpha$ if and only if $f_n(\alpha) = 0$ and $f_n'(\alpha) = 0$. Using the chain rule, $f_{n+1}'(x) = e'(f_n(x)) \cdot f_n'(x)$, so we reduce to showing that $e'(f_n(x)) \neq 0$ for any root $x$ of $f_{n+1}$ and that $f_n'(x) \neq 0$ by the inductive hypothesis. The crucial valuation estimate is that $e'(\alpha) = q\alpha^{q-1} + \pi$ has $|e'(\alpha)| = |\pi|$ whenever $|\alpha| < 1$, since $|q/\pi| \leq 1$ forces the $\pi$ term to dominate. [/proofplan] [step:Establish that every root of $f_n$ lies in $\bar{\mathfrak{m}}$ and compute $e'(\alpha)$ for $|\alpha| < 1$] We first observe that every root of $f_n$ has absolute value strictly less than $1$. For $n = 1$: $f_1(x) = e(x) = x^q + \pi x = x(x^{q-1} + \pi)$. The nonzero roots satisfy $x^{q-1} = -\pi$, so $|x|^{q-1} = |\pi| < 1$, giving $|x| < 1$. For $n \geq 2$: $f_n(x) = e(f_{n-1}(x)) = 0$ means either $f_{n-1}(x) = 0$ (in which case $|x| < 1$ by induction) or $f_{n-1}(x)$ is a nonzero root of $e$, which satisfies $|f_{n-1}(x)| < 1$. In the latter case, since $f_{n-1}(X) = \pi X + \text{higher order terms}$, the equation $f_{n-1}(x) = \beta$ with $|\beta| < 1$ forces $|x| < 1$ (the Newton polygon of $f_{n-1}(X) - \beta$ shows all roots have absolute value less than $1$). Now compute $e'(\alpha)$ for any $\alpha$ with $|\alpha| < 1$. We have \begin{align*} e'(X) = qX^{q-1} + \pi. \end{align*} Since $K$ is a local field with residue characteristic $p$ and $q = |\kappa_K| = p^f$ is the cardinality of the residue field, we have $q \in \mathfrak{m}_K$ (because $q = p \cdot p^{f-1}$ and $|p| < 1$ in $K$). Moreover, $\pi$ is a uniformizer of $K$, so $v_K(q) \geq 1 = v_K(\pi)$, which gives $|q/\pi| \leq 1$, i.e., $q/\pi \in \mathcal{O}_K$. For $|\alpha| < 1$: \begin{align*} |q\alpha^{q-1}| = |q| \cdot |\alpha|^{q-1} \leq |q| < |\pi| \cdot |q/\pi|^{-1} \cdot |q/\pi| = |q|. \end{align*} More directly: $|q\alpha^{q-1}| = |q| \cdot |\alpha|^{q-1}$. Since $|\alpha| < 1$, we have $|\alpha|^{q-1} < 1$, so $|q\alpha^{q-1}| < |q| \leq |\pi| \cdot |q/\pi|^{-1}$. But we need only $|q\alpha^{q-1}| < |\pi|$. We have $|q\alpha^{q-1}| = |q| \cdot |\alpha|^{q-1}$. Since $|\alpha| < 1$ and $q - 1 \geq 1$, we get $|\alpha|^{q-1} < 1$. And $|q| = |(q/\pi) \cdot \pi| = |q/\pi| \cdot |\pi| \leq |\pi|$ since $|q/\pi| \leq 1$. Therefore $|q\alpha^{q-1}| \leq |\pi| \cdot |\alpha|^{q-1} < |\pi|$. By the [Isoceles Triangle Principle](/theorems/???), since $|q\alpha^{q-1}| < |\pi|$, we have \begin{align*} |e'(\alpha)| = |q\alpha^{q-1} + \pi| = \max(|q\alpha^{q-1}|, |\pi|) = |\pi| \neq 0. \end{align*} [guided] This step sets up the valuation estimate that powers the induction. The formal derivative of $e(X) = X^q + \pi X$ is $e'(X) = qX^{q-1} + \pi$. At any root $\alpha$ of $f_n$, we will need $e'(\alpha) \neq 0$ (or more generally, $e'$ evaluated at elements of $\bar{\mathfrak{m}}$ is nonzero). The argument is a competition between the two terms $q\alpha^{q-1}$ and $\pi$. Why is $|q/\pi| \leq 1$? The integer $q = p^f$ is a power of the residue characteristic $p$. In the local field $K$, we have $v_K(p) \geq 1$ (since $p$ maps to $0$ in the residue field $\kappa_K$). The uniformizer $\pi$ has $v_K(\pi) = 1$. Since $q = p^f$, we get $v_K(q) = f \cdot v_K(p) \geq f \geq 1 = v_K(\pi)$. Therefore $v_K(q/\pi) = v_K(q) - v_K(\pi) \geq 0$, i.e., $q/\pi \in \mathcal{O}_K$. Now for $|\alpha| < 1$: $|q\alpha^{q-1}| = |q| \cdot |\alpha|^{q-1} \leq |\pi| \cdot |\alpha|^{q-1} < |\pi|$ (using $|q| \leq |\pi|$ and $|\alpha|^{q-1} < 1$). Since the two terms $q\alpha^{q-1}$ and $\pi$ have different absolute values, the Isoceles Triangle Principle gives $|e'(\alpha)| = \max(|q\alpha^{q-1}|, |\pi|) = |\pi| > 0$. The $\pi$ term dominates the $q\alpha^{q-1}$ term. We also verify that every root of $f_n$ lies in $\bar{\mathfrak{m}}$. For $n = 1$, the nonzero roots of $e(x) = x(x^{q-1} + \pi)$ satisfy $|x|^{q-1} = |\pi| < 1$, so $|x| < 1$. For general $n$, $f_n(x) = 0$ means $e(f_{n-1}(x)) = 0$, so $f_{n-1}(x)$ is a root of $e$, hence $|f_{n-1}(x)| < 1$ (or $f_{n-1}(x) = 0$), and inductively $|x| < 1$. [/guided] [/step] [step:Prove by induction that $f_n'(\alpha) \neq 0$ for every root $\alpha$ of $f_n$] We proceed by induction on $n$. **Base case ($n = 1$).** Let $\alpha$ be a root of $f_1 = e$. From the previous step, $|\alpha| < 1$ (for $\alpha \neq 0$; and $\alpha = 0$ gives $f_1'(0) = e'(0) = \pi \neq 0$). The previous step showed $|e'(\alpha)| = |\pi| \neq 0$, so $f_1'(\alpha) = e'(\alpha) \neq 0$. **Inductive step.** Assume that for all roots $\beta$ of $f_n$, we have $f_n'(\beta) \neq 0$. Let $\alpha$ be a root of $f_{n+1} = e \circ f_n$. By the chain rule for formal derivatives: \begin{align*} f_{n+1}'(\alpha) = e'(f_n(\alpha)) \cdot f_n'(\alpha). \end{align*} Since $f_{n+1}(\alpha) = e(f_n(\alpha)) = 0$, the element $\beta := f_n(\alpha)$ is a root of $e$. If $\beta = 0$, then $\alpha$ is a root of $f_n$, and by the inductive hypothesis $f_n'(\alpha) \neq 0$; also $e'(0) = \pi \neq 0$, so $f_{n+1}'(\alpha) \neq 0$. If $\beta \neq 0$, then $|\beta| < 1$ (since $\beta$ is a nonzero root of $e$). By the estimate from the previous step, $|e'(\beta)| = |\pi| \neq 0$. It remains to show $f_n'(\alpha) \neq 0$. We verify that $\alpha$ is a root of $f_n - \beta$, and we need to check that $f_n$ separates its level sets. But in fact, we can argue more directly: $f_n'(\alpha) \neq 0$ follows from a stronger inductive claim. We strengthen the induction: for every $n \geq 1$ and every $\alpha \in \bar{\mathfrak{m}}$ with $f_n(\alpha) \in \bar{\mathfrak{m}}$ (i.e., $|f_n(\alpha)| < 1$, which holds for all roots of $f_{n+1}$ since $f_n(\alpha)$ is then a root of $e$), we have $|f_n'(\alpha)| = |\pi|^n$. For $n = 1$: $f_1'(\alpha) = e'(\alpha)$ and $|e'(\alpha)| = |\pi|$ by the previous step, confirming $|f_1'(\alpha)| = |\pi|$. For the inductive step: $f_{n+1}'(\alpha) = e'(f_n(\alpha)) \cdot f_n'(\alpha)$. Since $f_{n+1}(\alpha) = e(f_n(\alpha)) = 0$ implies $f_n(\alpha)$ is a root of $e$ with $|f_n(\alpha)| < 1$, we have $|e'(f_n(\alpha))| = |\pi|$ by the previous step. By the inductive hypothesis (applied to $\alpha$ as an element with $|f_n(\alpha)| < 1$, hence $|f_{n-1}(\alpha)| < 1$ as well by backwards propagation), $|f_n'(\alpha)| = |\pi|^n$. Therefore \begin{align*} |f_{n+1}'(\alpha)| = |e'(f_n(\alpha))| \cdot |f_n'(\alpha)| = |\pi| \cdot |\pi|^n = |\pi|^{n+1} \neq 0. \end{align*} Since $f_n'(\alpha) \neq 0$ at every root $\alpha$ of $f_n$, the polynomial $f_n$ has no repeated roots. [guided] The chain rule is the engine of the induction. Since $f_{n+1} = e \circ f_n$, the derivative satisfies $f_{n+1}'(X) = e'(f_n(X)) \cdot f_n'(X)$. At a root $\alpha$ of $f_{n+1}$, the value $f_n(\alpha)$ is a root of $e$, and we showed $|e'(\beta)| = |\pi|$ for any root $\beta$ of $e$ with $|\beta| < 1$. So the first factor $e'(f_n(\alpha))$ is always nonzero. For the second factor $f_n'(\alpha)$, we use the inductive hypothesis. The subtle point is that $\alpha$ need not be a root of $f_n$ itself -- it is a root of $f_{n+1}$, which means $f_n(\alpha)$ is a root of $e$ but $\alpha$ may not be a root of $f_n$. This is why we strengthen the induction to: $|f_n'(\alpha)| = |\pi|^n$ whenever $|\alpha| < 1$ and $|f_n(\alpha)| < 1$. Why does this strengthening work? Because $f_n'(\alpha) = e'(f_{n-1}(\alpha)) \cdot f_{n-1}'(\alpha)$ (by the chain rule applied to $f_n = e \circ f_{n-1}$). The condition $|f_n(\alpha)| = |e(f_{n-1}(\alpha))| < 1$ implies $|f_{n-1}(\alpha)| < 1$ (since the roots of $e(\beta) = \gamma$ for $|\gamma| < 1$ all satisfy $|\beta| < 1$ -- this follows from $e(\beta) = \beta^q + \pi\beta = \beta(\beta^{q-1} + \pi)$). So the inductive hypothesis applies to $f_{n-1}'(\alpha)$, giving $|f_{n-1}'(\alpha)| = |\pi|^{n-1}$, and $|e'(f_{n-1}(\alpha))| = |\pi|$ since $|f_{n-1}(\alpha)| < 1$, completing the induction. The upshot is the clean formula $|f_n'(\alpha)| = |\pi|^n > 0$ for any root $\alpha$ of $f_n$ (or more generally, any $\alpha \in \bar{\mathfrak{m}}$ in the appropriate domain). Since $f_n'$ does not vanish at any root of $f_n$, the polynomial $f_n$ has no repeated roots. [/guided] [/step]