Formal torsion radius for prime power order (source code)

= Formal torsion radius for prime power order
{title2=$|z|\ge|p|^{1/(p^n-p^{n-1})}$}

Let a one-dimensional <formal group law> be defined over the valuation ring of a complete discretely valued <non-Archimedean valued field> of characteristic zero and residue characteristic $p$. If $z$ in the maximal ideal has exact formal order $p^n$, its absolute value satisfies the displayed lower bound. Use the coefficient splitting $[p](T)=pf(T)+g(T^p)$, where $f(T)=T+O(T^2)$ and $g(0)=0$. On the maximal ideal, $|f(z)|=|z|$ and $|g(z^p)|\le|z|^p$. If $|z|<|p|^{1/(p-1)}$, the first term strictly dominates, so $|[p]z|=|p||z|$ and repeated multiplication never reaches zero. Every nonzero $p$-power torsion point is therefore at least that large.

On this remaining radius range, $|[p]z|\le|z|^p$. For $n=1$, cancellation in $[p]z=0$ gives $|z|^{p-1}\ge|p|$. For larger $n$, apply induction to the point $[p]z$ of order $p^{n-1}$ and take a $p$th root. This yields the stated exponent. Over $\mathbb Q_p$ for odd $p$, the radius already exceeds $p^{-1}$, excluding torsion from the formal group on $p\mathbb Z_p$.