[proofplan] We verify three things: (1) the formal group law $F(x, y)$ converges for $x, y \in \bar{\mathfrak{m}}$ and produces an element of $\bar{\mathfrak{m}}$, so the addition $+_F$ is well-defined; (2) the endomorphism series $[a]_F(x)$ likewise converges and lands in $\bar{\mathfrak{m}}$, so scalar multiplication is well-defined; (3) the $\mathcal{O}_K$-module axioms (associativity and commutativity of $+_F$, distributivity of $[\cdot]_F$, and the unit law $[1]_F = \operatorname{id}$) hold because they are identities of formal power series that hold in $\mathcal{O}_K[[X, Y]]$, and convergence in $\bar{\mathfrak{m}}$ allows us to evaluate them. [/proofplan]

[step:Show that $F(x, y)$ converges in $\bar{\mathfrak{m}}$ for all $x, y \in \bar{\mathfrak{m}}$]Write $F(X, Y) = X + Y + \sum_{i+j \geq 2} c_{ij} X^i Y^j$ with $c_{ij} \in \mathcal{O}_K$. Let $x, y \in \bar{\mathfrak{m}}$, so there exists a finite extension $L/K$ with $x, y \in \mathfrak{m}_L$. The field $L$ is complete with respect to the unique extension of the absolute value on $K$. For each monomial $c_{ij} x^i y^j$ with $i + j \geq 2$, we have $|c_{ij}| \leq 1$ (since $c_{ij} \in \mathcal{O}_K$) and $|x^i y^j| = |x|^i |y|^j$. Set $\rho := \max(|x|, |y|) < 1$. Then $|c_{ij} x^i y^j| \leq \rho^{i+j} \leq \rho^2$ for $i + j \geq 2$, and more precisely $|c_{ij} x^i y^j| \leq \rho^{i+j} \to 0$ as $i + j \to \infty$. Since the absolute value on $L$ is non-archimedean, a series converges as soon as its terms tend to zero (by the [Convergence via Term Decay](/theorems/???) criterion, which applies because $L$ is complete and non-archimedean). The general term of $F(x, y)$ tends to $0$, so the series converges in $L$. The sum $F(x, y)$ satisfies $|F(x, y) - (x + y)| \leq \max_{i+j \geq 2} |c_{ij} x^i y^j| \leq \rho^2 < 1$. Since $|x + y| \leq \max(|x|, |y|) = \rho < 1$ by the strong triangle inequality, the [Isoceles Triangle Principle](/theorems/???) gives $|F(x, y)| \leq \max(|x + y|, \rho^2) < 1$. Therefore $F(x, y) \in \mathfrak{m}_L \subset \bar{\mathfrak{m}}$.[/step]

[guided]The formal group law $F(X, Y) \in \mathcal{O}_K[[X, Y]]$ is an infinite power series, so we must verify that substituting elements $x, y \in \bar{\mathfrak{m}}$ produces a convergent series. The key point is that $\bar{\mathfrak{m}} = \bigcup_{L/K \text{ finite}} \mathfrak{m}_L$, so any $x, y \in \bar{\mathfrak{m}}$ actually lie in $\mathfrak{m}_L$ for some single finite extension $L/K$. Since $L$ is a finite extension of the local field $K$, it is itself a local field (hence complete and non-archimedean). Write $F(X, Y) = X + Y + \sum_{i+j \geq 2} c_{ij} X^i Y^j$ with coefficients $c_{ij} \in \mathcal{O}_K$. Setting $\rho := \max(|x|, |y|) < 1$ (since $x, y \in \mathfrak{m}_L$), the general monomial satisfies \begin{align*} |c_{ij} x^i y^j| \leq |c_{ij}| \cdot |x|^i \cdot |y|^j \leq 1 \cdot \rho^{i+j}. \end{align*} As $i + j \to \infty$, the bound $\rho^{i+j} \to 0$ since $\rho < 1$. In a complete non-archimedean field, a series $\sum a_n$ converges if and only if $a_n \to 0$ (by the [Convergence via Term Decay](/theorems/???) theorem). The terms of $F(x, y)$ tend to zero, so the series converges in $L$. Why does the result land in $\mathfrak{m}_L$? By the strong triangle inequality, $|x + y| \leq \max(|x|, |y|) = \rho < 1$. The remaining terms contribute $|F(x,y) - (x+y)| \leq \max_{i+j \geq 2} \rho^{i+j} \leq \rho^2 < \rho < 1$. So $|F(x,y)| \leq \max(|x+y|, \rho^2) < 1$, which means $F(x,y) \in \mathfrak{m}_L \subset \bar{\mathfrak{m}}$.[/guided]

[step:Show that $[a]_F(x)$ converges in $\bar{\mathfrak{m}}$ for all $a \in \mathcal{O}_K$ and $x \in \bar{\mathfrak{m}}$] Write $[a]_F(X) = aX + \sum_{k \geq 2} d_k X^k$ with $d_k \in \mathcal{O}_K$. For $x \in \bar{\mathfrak{m}}$, choose a finite extension $L/K$ with $x \in \mathfrak{m}_L$. Each term satisfies $|d_k x^k| \leq |x|^k \to 0$ as $k \to \infty$ (since $|x| < 1$). By the [Convergence via Term Decay](/theorems/???) criterion, the series converges in $L$. The leading term gives $|[a]_F(x) - ax| \leq \max_{k \geq 2} |d_k x^k| \leq |x|^2 < |x|$. Since $|ax| = |a| \cdot |x| \leq |x| < 1$ (as $a \in \mathcal{O}_K$ means $|a| \leq 1$), the strong triangle inequality gives $|[a]_F(x)| \leq \max(|ax|, |x|^2) < 1$. Therefore $[a]_F(x) \in \mathfrak{m}_L \subset \bar{\mathfrak{m}}$. [/step]

[step:Verify the $\mathcal{O}_K$-module axioms by evaluating formal power series identities]The formal $\mathcal{O}_K$-module axioms assert the following identities of formal power series in $\mathcal{O}_K[[X, Y, Z]]$ (or the appropriate number of variables): 1. **Associativity of $+_F$**: $F(F(X, Y), Z) = F(X, F(Y, Z))$. 2. **Commutativity of $+_F$**: $F(X, Y) = F(Y, X)$. 3. **Identity element**: $F(X, 0) = X$. 4. **Inverse**: there exists $\iota(X) \in \mathcal{O}_K[[X]]$ with $F(X, \iota(X)) = 0$, and $\iota(x) \in \bar{\mathfrak{m}}$ for $x \in \bar{\mathfrak{m}}$ (since $\iota(X) = -X + \text{higher order terms}$, the same convergence argument as above applies). 5. **$[1]_F = \operatorname{id}$**: $[1]_F(X) = X$. 6. **$[ab]_F = [a]_F \circ [b]_F$**: this is part of the definition of a formal $\mathcal{O}_K$-module. 7. **$[a + b]_F = F([a]_F, [b]_F)$**: again part of the definition. 8. **Distributivity**: $[a]_F(F(X, Y)) = F([a]_F(X), [a]_F(Y))$, which is the endomorphism property of $[a]_F$. Each of these is an identity of formal power series holding coefficient-by-coefficient in $\mathcal{O}_K[[X, Y]]$ (or $\mathcal{O}_K[[X, Y, Z]]$). The previous two steps showed that all series involved converge when we substitute elements of $\bar{\mathfrak{m}}$. When two formal power series $P(X_1, \ldots, X_m) = Q(X_1, \ldots, X_m)$ agree coefficient-by-coefficient, their evaluations at any tuple $(x_1, \ldots, x_m) \in \bar{\mathfrak{m}}^m$ agree as well: the partial sums of $P$ and $Q$ agree at every finite stage, and the limits therefore coincide. This shows that $(\bar{\mathfrak{m}}, +_F, [\cdot]_F)$ satisfies all the $\mathcal{O}_K$-module axioms.[/step]

[guided]The point of this step is that the algebraic content — associativity, commutativity, distributivity, etc. — is already encoded in the formal group law and the formal $\mathcal{O}_K$-module structure. The axioms hold as identities between formal power series (this is the definition of a formal $\mathcal{O}_K$-module). Our task is to verify that these identities survive evaluation at elements of $\bar{\mathfrak{m}}$. Consider, for example, associativity. The identity $F(F(X, Y), Z) = F(X, F(Y, Z))$ means that every coefficient of $X^i Y^j Z^k$ on both sides matches. When we substitute $x, y, z \in \bar{\mathfrak{m}}$, the $N$-th partial sum of $F(F(x, y), z)$ depends only on finitely many coefficients. Since those coefficients agree with the corresponding ones of $F(x, F(y, z))$, the partial sums agree. Both series converge (by the estimates in the first step, applied iteratively: $F(x, y) \in \bar{\mathfrak{m}}$, so $F(F(x,y), z)$ is a valid substitution), so the limits agree. The same reasoning applies to each axiom. The formal inverse $\iota(X) = -X + \text{higher order terms}$ converges for $x \in \bar{\mathfrak{m}}$ by the same argument as in the second step (with $a = -1$ for the leading coefficient, plus higher-order terms bounded by $|x|^2$). The distributivity identity $[a]_F(F(X, Y)) = F([a]_F(X), [a]_F(Y))$ evaluates correctly because both sides converge and agree coefficient-by-coefficient. Why is this not circular? We are not proving the formal group axioms — those are given by hypothesis. We are only proving that the axioms, which hold in the ring of formal power series, remain valid after evaluation at convergent arguments. This is the passage from formal algebra to genuine algebra that makes $\bar{\mathfrak{m}}_F$ a genuine $\mathcal{O}_K$-module.[/guided]