Prime-power contraction in a formal group ($[p^n](x)⟶0(x\in \mathfrak{m})$)

Let $R$ be the valuation ring of a complete non-Archimedean valued field whose residue field has characteristic $p$, and let $\mathfrak{m}=\{x:|x|<1\}$. For a one-dimensional formal group law over $R$, repeated addition gives $[p](X)=pX+{\sum }_{j\ge 2}{c}_j{X}^j$ with $c_j\in R$. Hence $|[p](x)|\le \max (|p||x|,|x{|}^2)$. The series converges for $x\in \mathfrak{m}$ because its coefficients are bounded and $|x|<1$.

For $x_0=x$ and $x_{n+1}=[p](x_n)$, choose $\rho =\max (|p|,|x|)<1$. The values remain in the ball $|x_n|\le |x|$, so $|x_n|\le {\rho }^n|x|\to 0$. Associativity identifies $x_n=[p^n](x)$. The argument also works in equal characteristic $p$, where the linear coefficient vanishes, and does not require a discrete valuation. It proves contraction of prime-power multiplication near the formal identity without assuming a characteristic-zero formal logarithm.