Mordell's theorem: $E(\mathbb{Q})$ is a finitely generated abelian group

Read-back

Declaration. BSD.mordell is a theorem (a proposition, currently with a placeholder proof) whose statement is: for every Weierstrass curve $W$ over the field $\mathbb{Q}$ of rational numbers satisfying the typeclass hypothesis "$W$ is elliptic", the abelian group of nonsingular affine-coordinate points of $W$ (including the point at infinity) is finitely generated as a $\mathbb{Z}$-module. Nothing from the bundle Definitions.Def_BSD (BSD.IsLFunction, BSD.rank) is used; every notion below is the Mathlib one.

Binders and hypotheses.

1. $W$ — an explicit, universally quantified variable of type WeierstrassCurve ℚ. Literally, $W$ is any ordered quintuple of rational numbers

$$W = (a_1, a_2, a_3, a_4, a_6) \in \mathbb{Q}^5,$$

thought of as the equation

$$Y^2 + a_1 XY + a_3 Y \;=\; X^3 + a_2 X^2 + a_4 X + a_6 .$$

There is no hypothesis that the $a_i$ are integers, that the model is minimal, reduced, or in short Weierstrass form, or anything else about the coefficients beyond item 2.

2. [W.IsElliptic] — a typeclass (Prop-valued) hypothesis whose single field asserts that the discriminant $\Delta(W)$ is a unit of the coefficient ring. Over the field $\mathbb{Q}$, "unit" means exactly $\Delta(W) \neq 0$. Here $\Delta$ is the specific polynomial in the $a_i$ defined in Mathlib (with the LMFDB sign convention):

$$b_2 = a_1^2 + 4a_2,\quad b_4 = 2a_4 + a_1 a_3,\quad b_6 = a_3^2 + 4a_6,\quad b_8 = a_1^2 a_6 + 4a_2 a_6 - a_1 a_3 a_4 + a_2 a_3^2 - a_4^2,$$ $$\Delta(W) = -\,b_2^2\, b_8 \;-\; 8\, b_4^3 \;-\; 27\, b_6^2 \;+\; 9\, b_2 b_4 b_6 .$$

This hypothesis is satisfiable (e.g. $a_1=a_2=a_3=a_6=0,\ a_4=-1$ gives $\Delta = 64 \ne 0$), so the theorem is not vacuous; conversely, quintuples with $\Delta = 0$ are simply excluded from the statement.

No other hypotheses appear. In particular the theorem is only about points with coordinates in $\mathbb{Q}$ itself; no field extension or base change is involved.

The set of points $W^{\mathrm{aff}}(\mathbb{Q})$. W.toAffine is literally the same quintuple $W$, merely relabelled as "a Weierstrass curve viewed in affine coordinates" (the conversion is a definitional identity). Its type of points, W.toAffine.Point, is an inductive type with exactly two kinds of elements:

• a single distinguished element $O$ (the "point at infinity", the constructor with no data); and
• for each pair $(x, y) \in \mathbb{Q}\times\mathbb{Q}$ together with a proof $h$ that $(x,y)$ is nonsingular on $W$, one element $P = (x, y)$. Two such elements are equal iff their $x$ and $y$ agree (the proof component is irrelevant by proof irrelevance).

Here "$(x,y)$ is nonsingular on $W$" is the conjunction of two conditions:

$$\text{(Equation)}\qquad y^2 + a_1 x y + a_3 y - \bigl(x^3 + a_2 x^2 + a_4 x + a_6\bigr) = 0,$$ $$\text{(Nonsingularity)}\qquad a_1 y - \bigl(3x^2 + 2a_2 x + a_4\bigr) \neq 0 \quad\text{or}\quad 2y + a_1 x + a_3 \neq 0,$$

i.e. the point lies on the curve and at least one of the two partial derivatives $\partial_X, \partial_Y$ of the defining polynomial is nonzero there. So singular rational points on the cubic are literally excluded from the type. (Mathlib separately proves that, under the hypothesis $\Delta(W)\ne 0$ of item 2 and over a nontrivial ring, the Equation alone already implies Nonsingularity, so in the presence of item 2 the type consists of $O$ together with all rational solutions $(x,y)$ of the Weierstrass equation.)

The type is never empty: $O$ always belongs to it, even if the equation has no rational solutions.

The group structure. The additive commutative group structure on W.toAffine.Point that the statement uses is Mathlib's instance WeierstrassCurve.Affine.Point.instAddCommGroup, which exists because $\mathbb{Q}$ is a field with decidable equality. Concretely it is the chord–tangent law given by explicit formulas:

• $0 := O$.
• Negation: $-O = O$ and $-(x,y) = (x,\; -y - a_1 x - a_3)$.
• Addition: $O + P = P + O = P$. For $P_1 = (x_1,y_1)$, $P_2 = (x_2,y_2)$: if $x_1 = x_2$ and $y_1 = -y_2 - a_1 x_2 - a_3$ (i.e. $P_1 = -P_2$), then $P_1 + P_2 = O$; otherwise $P_1 + P_2 = (x_3, y_3)$ with

$$\ell = \begin{cases} \dfrac{y_1 - y_2}{x_1 - x_2} & x_1 \ne x_2,\\[1.2ex] \dfrac{3x_1^2 + 2a_2 x_1 + a_4 - a_1 y_1}{2y_1 + a_1 x_1 + a_3} & x_1 = x_2, \end{cases}\qquad x_3 = \ell^2 + a_1\ell - a_2 - x_1 - x_2,$$ $$y_3 = -\bigl(\ell (x_3 - x_1) + y_1\bigr) - a_1 x_3 - a_3 .$$

Associativity and commutativity are theorems in Mathlib (proved via the ideal class group of the affine coordinate ring); the statement being audited simply inherits this structure. The $\mathbb{Z}$-module structure is the canonical one on any additive commutative group: $n\cdot P$ is $P$ added to itself $n$ times for $n \ge 0$ and $(-n)\cdot P = -(n\cdot P)$.

The conclusion Module.Finite ℤ W.toAffine.Point. By definition, this is the proposition that the top submodule of the $\mathbb{Z}$-module $W^{\mathrm{aff}}(\mathbb{Q})$ is finitely generated, i.e.

$$\exists\, S \subseteq W^{\mathrm{aff}}(\mathbb{Q}) \text{ finite},\qquad \operatorname{span}_{\mathbb{Z}} S \;=\; W^{\mathrm{aff}}(\mathbb{Q}),$$

equivalently: there exist finitely many points $P_1,\dots,P_n$ (with $n \ge 0$) such that every point of $W^{\mathrm{aff}}(\mathbb{Q})$ can be written as $m_1 P_1 + \dots + m_n P_n$ with $m_i \in \mathbb{Z}$. Mathlib records that for an additive commutative group this is the same as being a finitely generated group.

What the statement does and does not say. In full:

For every $(a_1,a_2,a_3,a_4,a_6) \in \mathbb{Q}^5$ with $\Delta \neq 0$ (formula above), the abelian group consisting of the point at infinity together with all rational solutions $(x,y)$ of $Y^2 + a_1XY + a_3Y = X^3 + a_2X^2 + a_4X + a_6$ that satisfy the nonsingularity condition, under the chord–tangent addition above, is finitely generated.

The statement makes no claim about the rank of this group, its torsion, the number of generators, or any structure theorem; the degenerate case in which the group is $\{O\}$ (no rational affine points) is included and is trivially finitely generated (take $S = \varnothing$ or $S=\{O\}$). It says nothing about curves with $\Delta = 0$, about points over any field other than $\mathbb{Q}$, or about any projective/Jacobian coordinate model.