[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]