Weak Mordell–Weil: $E(\mathbb{Q})/2E(\mathbb{Q})$ is finite

Let $E$ be an elliptic curve over $\mathbb{Q}$, given by a Weierstrass equation $y^2 + a_1xy + a_3y = x^3 + a_2x^2 + a_4x + a_6$ with rational coefficients and non-zero discriminant, and let $E(\mathbb{Q})$ be its group of rational points (the point at infinity together with the rational affine solutions, under chord–tangent addition).

Weak Mordell–Weil theorem. The subgroup $2E(\mathbb{Q}) = \{2P : P \in E(\mathbb{Q})\}$ has finite index in $E(\mathbb{Q})$; equivalently, the quotient $E(\mathbb{Q})/2E(\mathbb{Q})$ is finite.

In Lean, $2E(\mathbb{Q})$ is the range of the doubling homomorphism nsmulAddMonoidHom 2 on W.toAffine.Point, and the conclusion is AddSubgroup.FiniteIndex of that range.

Standard proofs: (i) if $E$ has a rational $2$-torsion point, via the $2$-isogeny descent map $E(\mathbb{Q}) \to \mathbb{Q}^\times/(\mathbb{Q}^\times)^2$, $(x,y) \mapsto x - e$, whose image lies in the finite subgroup generated by $-1$ and the primes dividing the discriminant; (ii) in general, via the Kummer map $E(\mathbb{Q})/2E(\mathbb{Q}) \hookrightarrow K^\times/(K^\times)^2$ with $K = \mathbb{Q}[T]/(f(T))$ the cubic algebra of the $2$-division polynomial, with image in a Selmer-type group that is finite by finiteness of class groups and finite generation of $S$-units.

Combined with the (already proved) descent theorem WeierstrassCurve.Affine.Point.addGroup_fg_of_finiteIndex, this yields Mordell's theorem BSD.mordell.