We use two precise facts about the formal group of an elliptic curve. At a prime of good reduction, its kernel of reduction of an elliptic curve is identified by the uniformizer with the group . For odd this group is torsion-free. To see the second fact, the integral invariant differential of a formal group law has the form , with . Integrating constructs the formal logarithm
It is a group homomorphism to the additive group. For and ,
when is odd. Hence the series converges and , so it is injective. The target has no nonzero torsion. Therefore reduction is injective on the entire rational torsion subgroup at an odd prime of good reduction, including its -primary part.
For the present elliptic curve, , so every odd is a prime of good reduction. If , the Legendre symbol of is . The values and cancel in the sum of the Legendre symbols of , yielding
The rational torsion subgroup injects into each of these groups, so it is finite and its order divides every such .
For any odd prime , the Dirichlet theorem on primes in arithmetic progressions supplies infinitely many with and . Discard the finitely many dividing . Since , it cannot divide . Similarly choose , again avoiding ; then , so .
There are already four rational 2-torsion points,
which are distinct because a squarefree integer is nonzero. Thus
Its order is four. In fact the argument works for every nonzero integer ; squarefreeness is not needed for this torsion conclusion.
Here a formal group means a one-dimensional commutative formal group law. Over a ring , it is a formal power series satisfying
In particular, terms of total degree at least . A formal inverse with is obtained recursively. An isomorphism of formal group laws from to is a series with invertible linear coefficient and
Its compositional inverse exists over by coefficient recursion.
For , all these series converge on ; the operations preserve that set and make it the group . Use the uniformizer and normalize the valuation by , and write .
We explicitly construct its formal logarithm. Define
Then put
This is a formal series over with linear coefficient . Differentiating associativity in its last variable at gives
It follows that the -derivative of is , the same as that of . Evaluating at therefore proves
The differential is the invariant differential of a formal group law.
Choose an integer . In degree , the coefficient of has valuation at least . Thus the scaled series
has
Here , and the coefficient valuations tend to infinity. Consequently with a convergent integral power series on . Such a series is -Lipschitz. For any , the equation is equivalent to , a strict contraction, to which the contraction mapping theorem applies on the complete ring . It has exactly one solution.
The deep logarithm subgroup of a formal group is obtained as follows. The formal group exponential is the formal compositional inverse of , obtained recursively; equivalently it solves , with . The preceding contraction, applied to the scaled series, constructs its convergent inverse on and agrees with that formal inverse. This supplies the required convergence sketch for as well as a bijectivity proof for the logarithm.
The integral formal law and inverse preserve , so this is a subgroup. The logarithm identity and bijectivity give
Reduction of the formal law modulo has kernel . Its underlying image set is , which has size , where . Thus this subgroup has finite index, explicitly .