 Torsion-free formal subgroup for a short Weierstrass equation

For an integral short equation $y^2=x^3+ax+b$, negation acts on $t=-x/y$ by $t\mapsto -t$. Thus the integral formal multiplication series is odd: $[2](t)=2t+t^{3}g(t)$. If $v_2(t)=s\ge 1$, the leading term has valuation $s+1<3s$, so successive doubling never kills a nonzero point. Odd multiplication has unit linear coefficient. Combined with the formal logarithm at odd primes, this proves torsion-freeness of the formal identity neighbourhood at every prime for a short equation. The short-model hypothesis matters at two.