[proofplan]
We prove finite generation by the standard height descent for elliptic curves over $\mathbb{Q}$. The weak Mordell-Weil theorem gives finiteness of the quotient $E(\mathbb{Q})/2E(\mathbb{Q})$, and the logarithmic height on $E(\mathbb{Q})$ has finite sublevel sets, quadratic growth under doubling, and controlled change under translation by any fixed finite set of rational points. These facts imply, by a group-theoretic descent lemma with the translation estimate included as an explicit hypothesis, that finitely many representatives of the quotient together with finitely many bounded-height points generate all of $E(\mathbb{Q})$.
[/proofplan]
[step:Record the weak Mordell-Weil and height inputs]
Let $G := E(\mathbb{Q})$ denote the abelian group of rational points on $E$ under the chord-and-tangent law. We use the following two standard inputs for elliptic curves over $\mathbb{Q}$.
First, the [weak Mordell-Weil theorem](/page/Weak%20Mordell-Weil%20Theorem) for multiplication by $2$ says that the quotient abelian group $G/2G$ is finite. Choose a finite set $R \subset G$ whose image under the quotient map $G \to G/2G$ is all of $G/2G$.
Second, let
\begin{align*}
h_E: G &\to \mathbb{R}_{\geq 0}
\end{align*}
be a logarithmic height associated to a fixed Weierstrass model of $E$. The standard [height theory of elliptic curves](/page/Height%20on%20Elliptic%20Curves) gives the following properties. For every real number $B \geq 0$, the sublevel set
\begin{align*}
G_{\leq B} := \{P \in G : h_E(P) \leq B\}
\end{align*}
is finite. There is a constant $C_E \geq 0$, depending only on $E$ and the chosen height, such that for every $P \in G$,
\begin{align*}
h_E(2P) \geq 4h_E(P) - C_E.
\end{align*}
Here $2P$ denotes the double of $P$ in the abelian group $G$. Finally, for the finite representative set $R$, there is a constant $D_R \geq 0$, depending only on $E$, the chosen height, and $R$, such that for every $P \in G$ and every $r \in R$,
\begin{align*}
h_E(P-r) \leq 2h_E(P) + D_R.
\end{align*}
[/step]
[step:Prove the abstract descent lemma]
[claim:Finite quotient plus a doubling height implies finite generation]
Let $G$ be an abelian group, let
\begin{align*}
h: G &\to \mathbb{R}_{\geq 0}
\end{align*}
be a function, and suppose that the following four conditions hold:
1. There is a finite set $R \subset G$ whose image under the quotient map $G \to G/2G$ is all of $G/2G$.
2. For every real number $B \geq 0$, the set $\{g \in G : h(g) \leq B\}$ is finite.
3. There is a constant $C \geq 0$ such that $h(2g) \geq 4h(g)-C$ for every $g \in G$.
4. There is a constant $D \geq 0$ such that $h(g-r) \leq 2h(g)+D$ for every $g \in G$ and every $r \in R$.
Then $G$ is finitely generated.
[/claim]
[proof]
Use the finite set $R \subset G$ and the constants $C,D \geq 0$ supplied by the hypotheses. Define
\begin{align*}
M := \max\left(\left\{\frac{C+D}{2}, C, D\right\} \cup \{h(r) : r \in R\}\right),
\end{align*}
which is finite because $R$ is finite. Define the finite set
\begin{align*}
S := R \cup \{g \in G : h(g) \leq M\}.
\end{align*}
The set $S$ is finite by the finite-sublevel hypothesis on $h$.
We prove that $S$ generates $G$. Suppose, for contradiction, that some element of $G$ is not in the subgroup generated by $S$. Among all such elements, choose $g \in G$ with $h(g)$ minimal. This choice is justified because the sublevel sets of $h$ are finite: if non-generated elements exist, choose one such element $g_0$; then the set of non-generated elements with height at most $h(g_0)$ is a nonempty finite set, so $h$ attains a minimum on it.
Since $R$ maps onto $G/2G$, there exist $r \in R$ and $g_1 \in G$ such that
\begin{align*}
g = r + 2g_1.
\end{align*}
Equivalently, $2g_1 = g-r$. Since $r \in R \subset S$, if $g_1$ belonged to the subgroup generated by $S$, then $g = r + 2g_1$ would also belong to that subgroup. Therefore $g_1$ is not generated by $S$.
Because $g$ is not generated by $S$ and every element of $S$ is generated by $S$, we have $g \notin S$, hence $h(g)>M$. The doubling inequality applied to $g_1$ and the translation estimate applied to the pair $(g,r)$ give
\begin{align*}
4h(g_1)-C \leq h(2g_1) = h(g-r) \leq 2h(g)+D.
\end{align*}
Therefore
\begin{align*}
h(g_1) \leq \frac{2h(g)+C+D}{4}.
\end{align*}
Since $h(g)>M \geq (C+D)/2$, we have $C+D < 2h(g)$, and the preceding inequality yields
\begin{align*}
h(g_1) < h(g).
\end{align*}
This contradicts the minimal choice of $g$, because $g_1$ is also not generated by $S$. Hence no non-generated element exists, and $G$ is generated by the finite set $S$.
[/proof]
[/step]
[step:Apply the descent lemma to $E(\mathbb{Q})$]
Apply the claim to the abelian group $G = E(\mathbb{Q})$, the height function $h = h_E$, and the finite representative set $R \subset G$ chosen above. The weak Mordell-Weil theorem supplies the finite representative set for $G/2G$. The height theorem for elliptic curves over $\mathbb{Q}$ supplies finite sublevel sets, the quadratic growth estimate under doubling with constant $C_E$, and the translation estimate with constant $D_R$. Therefore the claim gives that $E(\mathbb{Q})$ is generated by a finite subset of $E(\mathbb{Q})$.
Thus the rational points $E(\mathbb{Q})$ form a finitely generated abelian group under the chord-and-tangent group law.
[/step]
