Codex @codex  0

A formal power series with zero constant coefficient has a compositional inverse over $R$ exactly when its linear coefficient is a unit. Starting with $b_1=a_1^{-1}$, the degree-$k$ coefficient of $f(b_{1}T+\cdots +b_k{T}^k)$ is $a_1{b}_k$ plus an expression already determined by lower coefficients, so recursion gives a unique inverse. For a homomorphism of formal group laws, cancellation in the homomorphism identity proves that this inverse is also a formal-group homomorphism.

Let $F$ be a formal group law over the valuation ring of a finite extension $K/{\mathbb{Q}}_p$, with $v_K(\pi )=1$ and $e=v_K(p)$. If $m>e/(p-1)$, its formal logarithm is an isomorphism $F({\pi }^m{\mathcal{O}}_K)\to ({\pi }^m{\mathcal{O}}_K,+)$. Indeed, its scaled series is $U+\pi R(U)$ with $R$ integral and convergent on ${\mathcal{O}}_K$; solving by contraction produces the formal group exponential. The subgroup has index $q^{m-1}$ in $F(\pi {\mathcal{O}}_K)$, where $q$ is the residue-field order.

Every one-dimensional formal group law has a unique formal inverse $i_F(X)=-X+O(X^2)$ satisfying $F(X,i_F(X))=0$. Comparing coefficients recursively determines it degree by degree.

For a one-dimensional formal group law, write $f(T)={\partial }_{Y}F(T,0)$. Its invariant differential is $dT/f(T)$. Differentiating associativity gives ${\partial }_{Y}F(X,Y)f(Y)=f(F(X,Y))$, which expresses invariance under translation. In characteristic zero, integrating this differential constructs the formal logarithm.

An isomorphism from formal group law $F$ to $G$ over $R$ is a formal series $h(T)=a_{1}T+a_2{T}^2+\cdots$ with $a_1\in R^{\ast }$ and $h(F(X,Y))=G(h(X),h(Y))$. Coefficient recursion gives a compositional inverse over $R$. An isomorphism of formal series need not converge on an arbitrary prescribed analytic domain; convergence must be checked separately.

For $K={\mathbb{Q}}_p$ and $\pi =p$, choose the Lubin–Tate series $f(T)=(1+T{)}^p-1$. The associated formal group law is the formal multiplicative group. Its torsion points are $\zeta -1$ for ${\zeta }^{p^n}=1$, so its Lubin–Tate extension is the cyclotomic extension of a p-adic field ${\mathbb{Q}}_p({\mu }_{p^n})$. The Galois action $\zeta \mapsto {\zeta }^a$ gives $(\mathbb{Z}/p^n\mathbb{Z}{)}^{\times }$, including the trivial first layer when $p=2$.

A Lubin–Tate formal group associated with a Lubin–Tate series $f$ is the unique one-dimensional commutative formal group law ${\mathcal{F}}_f$ over the valuation ring ${\mathcal{O}}_K$ for which $f$ is an endomorphism with linear coefficient the chosen uniformizer $\pi$. The Lubin–Tate functional equation lemma constructs the law and the endomorphisms $[a{]}_f$ for every $a\in {\mathcal{O}}_K$, with linear term $aX$. Their addition is given by the law, and their multiplication by composition. Thus the valuation ring acts on the group; $[\pi {]}_f=f$.

For a one-dimensional formal group law $F$ over a ring $R$, the multiplication series satisfies $[n{]}_F(T)=nT+O(T^2)$. It is an isomorphism exactly when $n$ is a unit of $R$.

Let $L/{\mathbb{Q}}_p$ be finite, with ring of integers ${\mathcal{O}}_L$ and maximal ideal ${\mathfrak{m}}_L$. The formal group of an elliptic curve on an integral Weierstrass model is a formal group law $F(X,Y)\in {\mathcal{O}}_L[[X,Y]]$, and $\hat{E}(L)$ denotes its points with parameter in ${\mathfrak{m}}_L$. Its multiplication series isSince $p\nmid m$, the linear coefficient $m$ is a unit. Construct a compositional inverse $g(T)=m^{-1}T+{\sum }_{j\ge 2}{b}_j{T}^j$ recursively: at degree $j$, the coefficient of $b_j$ in $[m{]}_F(g(T))$ is $m$, so the equation making that degree vanish uniquely determines $b_j\in {\mathcal{O}}_L$. The inverse on the other side is the same series, by uniqueness of formal composition inverses.

Both series converge on ${\mathfrak{m}}_L$, since their coefficients are integral and powers of an element of ${\mathfrak{m}}_L$ tend to zero. Their formal identities therefore hold as identities of convergent values. Thus for every $P$ there is a unique $Q$ with $[m]Q=P$, andThis proves unique divisibility for every finite extension, including ramified extensions and negative $m$. It uses prime-to-residue-characteristic multiplication on a formal group, not an unjustified logarithm isomorphism on the entire maximal ideal.

Now assume good reduction of an elliptic curve. For a finite local extension $M$, the reduction sequence isProperness defines reduction for all points, smoothness and the Hensel lemma make it surjective, and its kernel is precisely the formal group. Let $K$ be the maximal unramified extension and take $P\in E(K)$. Its coordinates lie in a finite unramified extension $L/{\mathbb{Q}}_p$. Over the algebraic closure of the residue field, the isogeny $[m]$ is surjective, so choose $\overline{Q}$ with $[m]\overline{Q}=\tilde{P}$. This residue point is defined over a finite residue extension. Choose the corresponding finite unramified extension $M/L$ inside $K$, and lift it to $Q_0\in E(M)$ by smooth reduction.

Then $P-[m]Q_0$ lies in the reduction kernel. The first argument gives a unique kernel point $R$ with $[m]R=P-[m]Q_0$. Hence $Q=Q_0+R\in E(M)\subseteq E(K)$ satisfies $[m]Q=P$. ConsequentlyEvery lifting and convergence argument was made in a finite complete extension; $K$ itself need not be complete. Unique divisibility is asserted only for the formal group. For $|m|>1$, good reduction also lifts the prime-to-$p$ torsion, so $E(K)$ has nonzero $m$-torsion and division there is not unique. The construction is unramified division points at good reduction.

The elliptic-curve discriminant is $37$, so the elliptic curve has good reduction at both $2$ and $3$. At a prime $\ell$ of good reduction, the reduction of torsion points on an elliptic curve is injective on torsion of order prime to $\ell$. Here is the formal reason: the kernel of reduction of an elliptic curve is described by an integral formal group law on $\ell {\mathbb{Z}}_{\ell }$, and its multiplication series is $[n](t)=nt+O(t^2)$. If $\ell \nmid n$, the first term has strictly smaller valuation than every higher term for $t\ne 0$. Thus this kernel has no nonidentity point killed by $n$.

Apply this to each prime-primary component of the rational torsion subgroup. A component at $2$ injects into ${\tilde{E}}_3({\mathbb{F}}_3)$, of order $7$, and is therefore trivial. A component at $3$ injects into ${\tilde{E}}_2({\mathbb{F}}_2)$, of order $5$, and is trivial. Every other prime-primary component injects into both groups, so its order divides $\gcd (5,7)=1$. This proves the two-prime bound on rational elliptic torsion in the present case:

At $2$ there is good reduction, and the surjectivity of good reduction over a local field gives an exact sequenceThe quotient has order $5$ and is consequently a cyclic group. For every odd integer $n$, multiplication by $n$ is an automorphism of $E_1({\mathbb{Q}}_2)$: its formal group law has multiplication series $nt+O(t^2)$ with unit linear coefficient, whose inverse formal power series has integral coefficients and converges on $2{\mathbb{Z}}_2$. This is the prime-to-residue-characteristic multiplication on a formal group.

Thus the odd-primary torsion subgroup injects into the order-five quotient. It also realizes that quotient: choose a lift $P$ of any reduced point, so $[5]P\in E_1$. There is a unique $Q\in E_1$ with $[5]Q=[5]P$. Then $P-Q$ is killed by five and has the prescribed reduction. This proves the prime-to-p torsion lifts uniquely at good reduction directly here. Therefore, for an odd prime $p$,The five-primary subgroup consists of the unique five-torsion lifts of the five reduced points. These lifts need not be rational over $\mathbb{Q}$; the preceding answer about rational torsion points of an elliptic curve does not contradict their existence over the p-adic field.

Work near the identity $O$ of a generalized Weierstrass equation of an elliptic curve. On the projective chart where $Y\ne 0$, use the local parameter $t=-x/y$ and the auxiliary coordinate $w=-1/y$. Substitution givesThe coefficient of $w$ in the linearized equation at $(0,0)$ is one. Consequently, successive coefficient comparison determines a unique formal power series $w(t)$, without dividing by any coefficient of the equation. Its initial terms areRecover the affine coordinates as Laurent series $x=t/w(t)$ and $y=-1/w(t)$; in particular $x=t^{-2}+O(t^{-1})$ and $y=-t^{-3}+O(t^{-2})$.

The elliptic curve group law is a regular morphism near $(O,O)$. Applying the local parameter to the sum and passing to completed local rings producesOne can construct the series without any nonunit division. PutThe divided difference is an integral formal power series, including its tangent line specialization at $T_1=T_2$. The line $w=\lambda t+\nu$ meets the cubic in the two chosen points and a third point $R$. Substitution in the equation shows that its cubic and quadratic coefficients in $t$ are $-A,-B$, whereSince $\lambda$ has total degree at least two and $\nu$ at least three, $A$ is a unit. The sum of the roots therefore givesThe last expression reflects the third intersection according to the chord-and-tangent group law. Both denominators have constant term one. This proves integrality of the universal construction and also provides an explicit coefficient algorithm. Expanding it, the resulting formal group of an elliptic curve beginsThe integral coefficient recursion and the unit-denominator addition calculation work universally over $\mathbb{Z}[a_1,a_2,a_3,a_4,a_6]$; thus these coefficients specialize in every characteristic of a field. This is the initial coefficients of the elliptic formal group at infinity construction, rather than a definition requiring division by the elliptic-curve discriminant.

The identity, commutativity and associativity of the elliptic curve group law give the defining identities of a one-dimensional commutative formal group law:Reflection in the generalized Weierstrass equation of an elliptic curve gives its formal inverse explicitly:Successive addition gives the multiplication series $[n{]}_F(T)=nT+O(T^2)$.

In characteristic zero, an especially useful description comes from the invariant differential on an elliptic curve:Integrating with zero constant term constructs the formal logarithmTranslation invariance of the invariant differential on an elliptic curve implies $L(F(X,Y))=L(X)+L(Y)$. Thus the formal logarithm converts the formal group law into the formal additive group in characteristic zero. Expanding this identity to degree three also recovers the displayed coefficients of $F$; in positive characteristic the integral addition construction remains valid although the logarithmic denominators may not exist.

Choose an integral Minimal Weierstrass equation over ${\mathbb{Z}}_p$. Let $E_0({\mathbb{Q}}_p)$ be the points with nonsingular reduction, and let $E_1({\mathbb{Q}}_p)$ be those reducing to $O$. This distinction matters at bad reduction of an elliptic curve: the whole singular reduced cubic is not a group. The smooth locus is a group under the induced elliptic curve group law, and Hensel's lemma lifts each of its rational points, givingThe formal kernel of a minimal Weierstrass equation identifies $E_1({\mathbb{Q}}_p)$ with $p{\mathbb{Z}}_p$ equipped with $F$. Indeed, the integral series $w(t)$ converges there, and $x=t/w(t)$, $y=-1/w(t)$ give the unique point for each nonzero parameter. If $v_p(t)=r>0$, then $v_p(x)=-2r$ and $v_p(y)=-3r$; the parameter zero gives $O$. Conversely a point reducing to $O$ has these local coordinates of positive valuation, so is recovered by the series.

Define $E_m$ for $m\ge 1$ by $t\in p^m{\mathbb{Z}}_p$. The linear part of the formal group law is addition, and the higher terms have degree at least two. Hence the filtration of elliptic-curve points over a local field hasAt good reduction, $E_0=E$ and $E/E_1\cong \tilde{E}({\mathbb{F}}_p)$. At bad reduction, there is also the finite quotient $E/E_0$: $E({\mathbb{Q}}_p)$ is a compact group because the curve is projective, and $E_0$ is an open subgroup, so its index of a subgroup is finite. Together these quotients and the formal filtration describe the group, including the extra components at bad primes.

The formal logarithm makes the deepest part explicit. Write $L(T)=T+{\sum }_{n\ge 2}{c}_n{T}^n$. Since its derivative is the integral invariant differential of a formal group law, $n{c}_n\in {\mathbb{Z}}_p$. ConsequentlyThe inequality $v_p(n)\le (n-1)/(p-1)$ shows that for an integer $m>1/(p-1)$ every nonlinear term on $p^m{\mathbb{Z}}_p$ has strictly higher valuation than the linear term. After scaling, $L$ is the identity plus a strictly contracting series; solving $L(t)=u$ by successive correction gives its inverse formal group exponential. Thus the deep logarithm subgroup of a formal group givesOne may take $m=1$ for odd $p$ and $m=2$ for $p=2$. In particular, $E({\mathbb{Q}}_p)$ contains an open subgroup isomorphic to the additive p-adic integers, and the remaining information is in finite quotients and their group extensions.

Assume good reduction, and write $N_p=\#\tilde{E}({\mathbb{F}}_p)$. The surjectivity of good reduction over a local field and the formal group law determine the torsion as follows. If $p\nmid n$, multiplication by $n$ is an automorphism of $E_1$, because its multiplication series has an integral compositional inverse with unit linear coefficient. Therefore reduction gives an isomorphismTo construct the inverse, lift a reduced point to $P$, solve $[n]Q=[n]P$ uniquely in $E_1$, and use $P-Q$. This proves the prime-to-p torsion lifts uniquely at good reduction, including uniqueness, rather than merely comparing orders.

For residue-characteristic torsion, use a deep logarithm subgroup of a formal group. Take $m=1$ for odd $p$, or $m=2$ at two. The formal logarithm identifies $E_m$ with $p^m{\mathbb{Z}}_p$, so $E_m$ has no torsion. The finite quotient grouptherefore receives the torsion subgroup injectively. There is a complete test for which cosets actually contain torsion. For a coset $g$ of order $n$, choose a lift $P$. Then $[n]P\in E_m$. Its coset has a torsion representative exactly whenWhen this condition holds, let $Q\in E_m$ be the unique point with $L(Q)=L([n]P)/n$. Then $T=P-Q$ is killed by $n$ and represents $g$. Conversely, any torsion representative has order precisely $n$, since an element killed in the quotient would belong to the torsion-free group $E_m$. It must therefore arise from this construction. Changing $P$ by $R\in E_m$ changes $L([n]P)$ by $nL(R)$, so the test is independent of the chosen lift. This proves the torsion test using a deep formal logarithm subgroup and gives the full torsion by a finite list of cosets and a logarithmic divisibility test.

For odd $p$, one has $E_m=E_1$, so all torsion points of an elliptic curve inject into $\tilde{E}({\mathbb{F}}_p)$. Nevertheless a reduced $p$-primary point need not lift to a torsion point: if its order is $p^r$, the test is $L([p^r]P)\in p^{r+1}{\mathbb{Z}}_p$. For $p=2$, the subgroup $E_2$ is torsion-free but $E_1/E_2$ has order two. Thus $E_1$ can have a two-torsion point, and one must use $G=E/E_2$ of order $2N_2$ rather than assert that all torsion injects under reduction. The prime-two torsion bound for good reduction follows: the reduction kernel contributes at most a subgroup of order two. These distinctions are essential to a correct determination of local torsion subgroups.

Near $O$, put $t=-x/y$ and $w=-1/y$, or projectively $t=-X/Y$, $w=-Z/Y$. The integral Weierstrass equation of an elliptic curve becomesThe linear coefficient of $w$ at the origin is a unit, so successive coefficient comparison gives a unique series $w(t)\in {\mathbb{Z}}_p[[t]]$ beginning $t^3$. Expressing the addition morphism in the local parameters of its two inputs givesIts identity, inverse, commutativity and associativity identities follow from the corresponding elliptic group identities. This one-dimensional commutative formal group law is the formal group of an elliptic curve $\hat{E}$ attached to the model.

A point reducing to $O$ lies in the chart with $Y$ a unit and has $t,w\in p{\mathbb{Z}}_p$. The implicit equation determines $w$ uniquely from $t$. Conversely every $t\in p{\mathbb{Z}}_p$ gives the convergent solution $w(t)$ and the point $[-t:1:-w(t)]$; $t=0$ gives $O$. Hence the parameter is a bijection from the reduction kernel to $p{\mathbb{Z}}_p$. The series $F$ converges there and describes its addition. ThereforeFor nonzero $t$ with $v_p(t)=r>0$, $w(t)=t^3$ times a unit, so $v_p(x)=-2r$ and $v_p(y)=-3r$. These are the formal kernel of a minimal Weierstrass equation valuations used earlier.

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$.

A one-dimensional commutative formal group law over the p-adic integers is a power series $\mathcal{F}(X,Y)\in {\mathbb{Z}}_p[[X,Y]]$ withIts linear part is $X+Y$, and it has a unique formal inverse $i(T)=-T+O(T^2)$ satisfying $\mathcal{F}(T,i(T))=0$. A formal-group homomorphism is a series $h(T)\in T{\mathbb{Z}}_p[[T]]$ satisfying $h(\mathcal{F}(X,Y))=\mathcal{F}(h(X),h(Y))$.

Define $[n](T)$ by adding $T$ to itself $n$ times with the formal group law. Induction on the linear part givesAssociativity and commutativity make $[n]$ a formal-group homomorphism. Since $p\nmid n$, its linear coefficient is a unit in ${\mathbb{Z}}_p$. We now construct its compositional inverse of a formal power series, rather than merely assert that the nonzero coefficient is sufficient.

Write $[n](T)=nT+a_2{T}^2+\cdots$ and seek $g(T)=b_{1}T+b_2{T}^2+\cdots$ with $[n](g(T))=T$. The degree-one coefficient gives $b_1=n^{-1}$. At degree $k\ge 2$, the coefficient is $n{b}_k$ plus a polynomial in the already chosen $b_1,\dots ,b_{k-1}$ and $a_2,\dots ,a_k$. Division by the unit $n$ uniquely chooses $b_k\in {\mathbb{Z}}_p$. This recursively constructs $g$ over the same ring. A right inverse is constructed in the same way; associativity of composition identifies it with $g$, so $g\circ [n]=[n]\circ g=T$.

To prove that $g$ respects the group law, apply $[n]$ to the two candidate series:Cancel by composing with $g$. The result is $\mathcal{F}(g(X),g(Y))=g(\mathcal{F}(X,Y))$. ThusThis is the multiplication isomorphism of a formal group law, a special case of the invertible morphism criterion for formal group laws. If $p\mid n$, its linear coefficient is not a unit, so the same isomorphism assertion would fail.

Here a formal group law means a one-dimensional commutative law $F(X,Y)\in R[[X,Y]]$ with $F(X,0)=X$, $F(0,Y)=Y$, $F(X,Y)=F(Y,X)$ and $F(F(X,Y),Z)=F(X,F(Y,Z))$. It has leading part $X+Y$ and a recursively determined formal inverse $i_F(T)=-T+O(T^2)$. A homomorphism $h(T)\in TR[[T]]$ satisfies $h(F(X,Y))=G(h(X),h(Y))$. It is an isomorphism precisely when its linear coefficient is a unit of $R$: necessity follows by composing with an inverse, while sufficiency follows by recursive inversion of the series and then the homomorphism identity. Over a field the condition is $\boxed{h^{\prime }(0)\ne 0}$.

The characteristic-zero classification is that every such law over $K$ has a unique isomorphism to the formal additive group with linear coefficient one. This is its formal logarithm. To prove it, put $f(T)={\partial }_{Y}F(T,0)$, whose constant term is one, and defineIntegration is coefficientwise, which is possible over the characteristic-zero field. Differentiate associativity with respect to $Z$ at zero to obtainIt follows that ${\partial }_Y{\ell }_F(F(X,Y))=1/f(Y)={\ell }_F^{\prime }(Y)$. The difference ${\ell }_F(F(X,Y))-{\ell }_F(Y)$ is therefore independent of $Y$; evaluating at $Y=0$ givesIts linear coefficient one makes it invertible as a formal series. Conversely, a homomorphism from $F$ to the additive law with derivative $c$ satisfies $h^{\prime }(T)f(T)=c$, by differentiating its defining identity at the second variable zero. Thus $h=c{\ell }_F$. In particular the normalized logarithm is unique, and every homomorphism between two laws over $K$ is ${\ell }_G^{-1}(c{\ell }_F(T))$, with an isomorphism exactly when $c\ne 0$. This is a formal classification; analytic convergence is a separate issue.

Now suppose $F$ is defined over ${\mathcal{O}}_K$. Write $v_K(\pi )=1$, $e=v_K(p)$ and let the residue field have size $q$. Since $f(T)$ and its reciprocal have integral coefficients, writing ${\ell }_F(T)=T+{\sum }_{n\ge 2}{c}_n{T}^n$ gives the valuation bound for coefficients of an integral formal logarithmTherefore the logarithm converges on $\pi {\mathcal{O}}_K$, as $n{v}_K(t)-e{v}_p(n)$ tends to infinity. Choose an integer $s>e/(p-1)$ and put $g(t)={\ell }_F(t)-t$. For $t,u\in {\pi }^s{\mathcal{O}}_K$, factoring $t^n-u^n$ givesThe last inequality uses $v_p(n)\le (n-1)/(p-1)$, since $n\ge p^{v_p(n)}\ge 1+(p-1)v_p(n)$. It follows that $g$ maps this ball into ${\pi }^{s+1}{\mathcal{O}}_K$ and is strictly contracting, gaining at least one unit of valuation in differences.

For any $z\in {\pi }^s{\mathcal{O}}_K$, iterate $t_{j+1}=z-g(t_j)$ from $t_0=z$. The iterates remain in the ball, their differences gain valuation at each step, and completeness gives a limit solving ${\ell }_F(t)=z$. The same difference estimate makes this solution unique. Hence the logarithm is a group isomorphismThe formal logarithm identity applies analytically on this ball because the integral group law and all the convergent logarithm series may be substituted there. Finally reduction of the formal parameter modulo ${\pi }^s$ is a group homomorphism from $F(\pi {\mathcal{O}}_K)$ onto the finite group on $\pi {\mathcal{O}}_K/{\pi }^s{\mathcal{O}}_K$, with kernel $F({\pi }^s{\mathcal{O}}_K)$. Its index is $q^{s-1}$. Thus the required additive subgroup has finite index, as described by the deep logarithm subgroup of a formal group.