Mordell-Weil Analogue

Group of τ-rational points is finitely generated at each primorial level; rank stabilizes at finite depth

Mordell-Weil Analogue

Summary

Group of τ-rational points is finitely generated at each primorial level; rank stabilizes at finite depth

Statement

\label{prop:mordell-weil-analogue}
The group $\hat{\mathbb{Z}}_{\T}^{\,\mathbb{Q}}$ of $\tau$-rational points is the union of a tower of finitely generated abelian groups $G_1 \subseteq G_2 \subseteq G_3 \subseteq \cdots$, and the rank function $r(k) = \operatorname{rk}_{\mathbb{Z}}(G_k / G_k^{\mathrm{tor}})$ stabilizes at a finite depth $k_* \in \mathbb{N}$:
\begin{equation}
\exists\, k_* \in \mathbb{N} \;\;\text{such that}\;\;
r(k) = r(k_*) \quad \text{for all } k \geq k_*.
\label{eq:ch45-mordell-weil-stabilization}
\end{equation}
In particular, $r_\infty = r(k_*)$ is a finite non-negative integer, and $\hat{\mathbb{Z}}_{\T}^{\,\mathbb{Q}} \cong \mathbb{Z}^{r_\infty} \oplus T$ where $T$ is a torsion group compatible with the tower.

Proof / Justification

No immediate manuscript proof block was extracted in this pilot run.

Source Context

• Registry source: book-03.jsonl line 124
• Manuscript source: 2nd-edition/book-iii-categorical-spectrum/02_mainmatter/part06/ch45-tau-rational-interior-points.tex lines 188-198

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookIII.Arithmetic.RationalPoints
• Name: mordell_weil_check

Dependencies

• Canonical: III.D59, III.D60

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.