5 (source code)

= 5
{scope}

We first prove all three general torsion assertions before treating the lettered cases. If a finite point has $|x|_p>1$, the cubic term dominates the integral lower terms, so $v_p(x)=-2m$, $v_p(y)=-3m$ for an <integer> $m\ge1$. Its parameter $z=-x/y$ then lies in $p\mathbb Z_p$, with norm at most $p^{-1}$. The integral Weierstrass model defines its <formal group> at infinity over $\mathbb Z_p$: using $w=-1/y$ gives $w=z^3+Azw^2+Bw^3$, an integral power series starting in degree three.

The supplied torsion estimate excludes a nonzero torsion parameter for $p\ge3$, since $p^{-1}<p^{-1/(p-1)}$, and the lower bound increases for higher $p$-powers. For $p=2$ it excludes orders $2^n$ with $n\ge2$, because their bound is strictly above $1/2$. The remaining possibility is order two, which would imply the finite point equals its negative and hence $y=0$. A nonintegral $x$ cannot solve the monic cubic with integral coefficients, so this is impossible too. Thus every finite torsion point has integral $x$, and the equation then forces integral $y$.

For <good reduction> the reduction map is a <group homomorphism> whose <kernel> is this <formal group> at infinity. Its torsion-free <kernel> proves injectivity on torsion, giving a <subgroup> of the finite reduced group. Applying local integrality to a rational torsion point at every prime gives $x,y\in\mathbb Z$.

If $y\ne0$, the double of a rational torsion point is finite and integral. The doubling formula
$$
x(2P)=\frac{(3x^2+a)^2}{4y^2}-2x
$$
therefore implies $y^2\mid(3x^2+a)^2$. Also $y^2=x^3+ax+b$. Evaluating the supplied <polynomial> identity at the integral $x$ now gives
$$
\boxed{y=0\quad\text{or}\quad y^2\mid4a^3+27b^2.}
$$
This establishes the needed <Nagell–Lutz theorem> conclusions without assuming them in the lettered applications.