Solution (source code)

= Solution

A one-dimensional commutative <formal group law> over $\mathcal O_K$ is a power series $F(X,Y)\in\mathcal O_K[[X,Y]]$ satisfying
$$
F(X,0)=X,
\quad F(0,Y)=Y,
\quad F(F(X,Y),Z)=F(X,F(Y,Z)),
\quad F(X,Y)=F(Y,X).
$$
For $r\geq1$, the ideal $\pi^r\mathcal O_K$ becomes a group, denoted $F(\pi^r\mathcal O_K)$, under $x+_Fy=F(x,y)$; convergence follows because both inputs lie in the maximal ideal.

Over the characteristic-zero field $K$, there is a unique <formal logarithm>
$$
\log_F(T)=T+O(T^2)
$$
satisfying $\log_F(F(X,Y))=\log_F(X)+\log_F(Y)$. Its coefficients have bounded denominator growth, so for sufficiently large $r$ both $\log_F$ and its inverse <formal group exponential> converge on $\pi^r\mathcal O_K$ and preserve that ideal. They give
$$
F(\pi^r\mathcal O_K)\simeq(\pi^r\mathcal O_K,+)\simeq(\mathcal O_K,+),
$$
where the final isomorphism is multiplication by $\pi^{-r}$.