 Solution

Here $F$ is the usual one-dimensional commutative formal group law. Normalize the valuation $v$ by $v(\pi )=1$, and put $e=v(p)$. We show explicitly that for any integer $m>e/(p-1)$,This subgroup will have finite index in $F(\pi {\mathcal{O}}_K)$.

Set $a(T)={\partial }_{Y}F(T,0)$. Since $F(X,Y)=X+Y+$ terms of total degree at least two, $a(T)\in 1+T{\mathcal{O}}_K[[T]]$. Its inverse has integral coefficients, say $a(T{)}^{-1}={\sum }_{j\ge 0}{c}_j{T}^j$ with $c_0=1$. Define the formal logarithm over $K$ byDifferentiate associativity $F(F(X,Y),Z)=F(X,F(Y,Z))$ with respect to $Z$ at zero. This gives $a(F(X,Y))={\partial }_{Y}F(X,Y)a(Y)$, soEvaluating at $Y=0$ proves the formal identity $\ell (F(X,Y))=\ell (X)+\ell (Y)$.

The coefficients satisfy $v(c_{n-1}/n)\ge -e{v}_p(n)$. Thus the series converges on $\pi {\mathcal{O}}_K$, since for $v(T)\ge 1$ the valuations of its terms are at least $n-e{v}_p(n)\to \infty$. More quantitatively,Indeed, if $k=v_p(n)$ then $n\ge p^k\ge 1+k(p-1)$. If $v(T)\ge m>e/(p-1)$, every nonlinear term has valuation strictly greater than $v(T)$. Write $h(T)=\ell (T)-T$. For $S,T\in {\pi }^m{\mathcal{O}}_K$, use $T^n-S^n=(T-S){\sum }_{j=0}^{n-1}{T}^{n-1-j}{S}^j$ to obtainThe extra valuation is integral and positive because $(n-1)m-e{v}_p(n)>0$ for all $n\ge 2$.

For any $b\in {\pi }^m{\mathcal{O}}_K$, solve $\ell (T)=b$ by iterating $T\mapsto b-h(T)$. This map preserves the complete ball ${\pi }^m{\mathcal{O}}_K$ and improves differences by at least one valuation step. The contraction mapping theorem gives a unique solution. Therefore $\ell$ is a bijection of this ball onto itself, and the formal identity, now evaluated in convergent series, makes it a group isomorphism. Multiplication by ${\pi }^{-m}$ then identifies the additive target with ${\mathcal{O}}_K$.

Integral coefficients in $F$ and its formal inverse ensure that every $F({\pi }^j{\mathcal{O}}_K)$ is a subgroup. Reduction modulo ${\pi }^m$ respects the group law; two parameters represent the same coset of $F({\pi }^m{\mathcal{O}}_K)$ exactly when they are congruent modulo ${\pi }^m$. If the residue field has $q_K$ elements, the quotient consequently has $q_K^{m-1}$ elements. This proves both the finite-index assertion and the claimed additive structure, with an explicit depth that also works in ramified extensions and when $p=2$.