Weak Birch and Swinnerton-Dyer conjecture: $L(E,1) = 0$ if and only if $E(\mathbb{Q})$ is infinite

Read-back

Quantification and hypotheses. The statement is universally quantified over a Weierstrass curve $W$ over $\mathbb{Q}$, i.e. an arbitrary 5-tuple of rational numbers $(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,$$

together with one typeclass hypothesis, "$W$ is elliptic", which literally means: the discriminant

$$\Delta(W) = -b_2^2 b_8 - 8 b_4^3 - 27 b_6^2 + 9 b_2 b_4 b_6$$

(with $b_2 = a_1^2 + 4a_2$, $b_4 = 2a_4 + a_1 a_3$, $b_6 = a_3^2 + 4a_6$, $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$) is a unit of $\mathbb{Q}$, i.e. $\Delta(W) \neq 0$. No integrality, minimality, or reducedness condition is imposed on the coefficients $a_i$ themselves. The bundled definition rank (the $\mathbb{Z}$-module finrank of the point group) is not referenced by this theorem.

The claim. For every such $W$ there exists a function $\Lambda : \mathbb{C} \to \mathbb{C}$ satisfying the following three conditions simultaneously:

1. (Entire.) $\Lambda$ is complex-differentiable at every point of $\mathbb{C}$.
2. (Agreement on a half-plane.) For every $s \in \mathbb{C}$ with $\operatorname{Re} s > \tfrac32$ (strict inequality), $\Lambda(s) = L_W(s)$, where $L_W$ is the Mathlib "L-series of $W$" unfolded below.
3. (Bi-implication at $s=1$.) $\Lambda(1) = 0$ if and only if the type $W(\mathbb{Q})$ of affine nonsingular points of $W$ (unfolded below) is infinite, i.e. is not in bijection with $\{0,\dots,n-1\}$ for any $n \in \mathbb{N}$.

Conditions 1 and 2 together are the bundle's predicate $\mathrm{IsLFunction}(W, \Lambda)$; condition 3 is a separate conjunct. Nothing else is asserted about $\Lambda$: no functional equation, no order of vanishing, no growth condition, no uniqueness claim. (Since two entire functions agreeing on the open half-plane $\operatorname{Re} s > \tfrac32$ coincide, any two functions satisfying 1–2 are equal; so the existential, if satisfiable at all, singles out at most one $\Lambda$, and condition 3 is then a statement about that unique function.)

Unfolding $W(\mathbb{Q})$ (the type W.toAffine.Point). toAffine is the identity on the curve data. A point is either

• the single formal symbol $\mathcal{O}$ (the "point at infinity"), or
• a pair $(x, y) \in \mathbb{Q}^2$ that is nonsingular, meaning both

$$y^2 + a_1 x y + a_3 y - (x^3 + a_2 x^2 + a_4 x + a_6) = 0$$

and at least one of the partial derivatives is nonzero:

$$a_1 y - (3x^2 + 2a_2 x + a_4) \neq 0 \quad\text{or}\quad 2y + a_1 x + a_3 \neq 0.$$

Points with equal coordinates are equal (the nonsingularity proof is irrelevant to identity). Since $\Delta(W) \neq 0$ over the field $\mathbb{Q}$, every affine solution of the equation is automatically nonsingular, so $W(\mathbb{Q}) = \{\mathcal{O}\} \cup \{(x,y) \in \mathbb{Q}^2 : \text{equation holds}\}$. Only $\mathbb{Q}$-rational coordinates are included. "Infinite" is the negation of "finite" for this type.

Unfolding $L_W(s)$ (W.LSeries s). This is built in stages, each a total function with junk values where the mathematics is undefined.

(a) Primes. The product runs over the height-one prime spectrum of the ring of integers $\mathcal{O}_{\mathbb{Q}}$ of $\mathbb{Q}$ regarded as a number field, i.e. over the nonzero prime ideals $\mathfrak{p}$ of $\mathcal{O}_{\mathbb{Q}} \cong \mathbb{Z}$; these correspond to the rational primes $p$. For each $\mathfrak{p}$ let $K_{\mathfrak{p}}$ be the $\mathfrak{p}$-adic completion of $\mathbb{Q}$, $R_{\mathfrak{p}}$ its valuation subring (the ring of integers of the completion), and $\kappa_{\mathfrak{p}} = R_{\mathfrak{p}}/\mathfrak{m}$ its residue field. Set $q_{\mathfrak{p}} := |\kappa_{\mathfrak{p}}|$ computed with Nat.card, which returns $0$ if the residue field were infinite (here it is finite of size $p$).

(b) Minimal model and reduction at $\mathfrak{p}$. Base-change $W$ to $K_{\mathfrak{p}}$ (apply the inclusion $\mathbb{Q} \hookrightarrow K_{\mathfrak{p}}$ to each $a_i$), and let $W'_{\mathfrak{p}}$ be a minimal Weierstrass equation for it: a curve of the form $C \cdot W$ for a chosen admissible change of variables $C = (u, r, s, t)$ over $K_{\mathfrak{p}}$ ($u$ a unit) such that $C \cdot W$ is integral (all five coefficients lie in $R_{\mathfrak{p}}$) and the multiplicative valuation of its discriminant is maximal among all integral $C \cdot W$ (multiplicative valuation, with values in $\mathbb{Z}^{\times}\cup\{0\}$ written multiplicatively, so "larger" means fewer factors of $\mathfrak{p}$). The choice of $C$ is made by a choice function; the statement refers to whatever choice that is. The reduction $\tilde W_{\mathfrak{p}}$ is obtained by choosing (again by a choice function) an integral model of $W'_{\mathfrak{p}}$ with coefficients in $R_{\mathfrak{p}}$ and reducing those coefficients modulo $\mathfrak{m}$ to get a Weierstrass curve over $\kappa_{\mathfrak{p}}$.

The reduction types are predicates on the minimal equation $W'_{\mathfrak{p}}$ (each includes minimality as a hypothesis), with $v$ the multiplicative valuation on $K_{\mathfrak{p}}$ normalised so that $v(x) \le 1$ for integral $x$ and $v(x) = 1$ exactly for units:

• good reduction: $v(\Delta(W'_{\mathfrak{p}})) = 1$;
• multiplicative reduction: $v(\Delta(W'_{\mathfrak{p}})) < 1$ and $v(c_4(W'_{\mathfrak{p}})) = 1$, where $c_4 = b_2^2 - 24 b_4$;
• split multiplicative reduction: multiplicative reduction, and additionally, writing $I$ for the chosen integral model, the polynomial

$$c_4(I)\,T^2 + a_1(I) c_4(I)\,T - \bigl(54\, b_6(I) - 3\, b_2(I) b_4(I) + a_2(I) c_4(I)\bigr)$$

with coefficients reduced modulo $\mathfrak{m}$ splits (factors into linear factors) over $\kappa_{\mathfrak{p}}$;

• (additive reduction, $v(\Delta) < 1$ and $v(c_4) < 1$, is not named in the definition below; it falls into the final "else" branch.)

(c) Local polynomial. Define $f_{\mathfrak{p}}(T) \in \mathbb{Z}[T]$ by the following case split, evaluated in order:

$$f_{\mathfrak{p}}(T) = \begin{cases} 1 - a_{\mathfrak{p}} T + q_{\mathfrak{p}} T^2 & \text{if } W'_{\mathfrak{p}} \text{ has good reduction},\\ 1 - T & \text{else, if } W'_{\mathfrak{p}} \text{ has split multiplicative reduction},\\ 1 + T & \text{else, if } W'_{\mathfrak{p}} \text{ has multiplicative reduction},\\ 1 & \text{otherwise},\end{cases}$$

where $a_{\mathfrak{p}} := q_{\mathfrak{p}} + 1 - \bigl|\tilde W_{\mathfrak{p}}(\kappa_{\mathfrak{p}})\bigr|$ as an integer, and $\bigl|\tilde W_{\mathfrak{p}}(\kappa_{\mathfrak{p}})\bigr|$ is the Nat.card of the point type of the reduced curve over $\kappa_{\mathfrak{p}}$ — the same notion of "point" as above: the point at infinity together with the nonsingular affine solutions in $\kappa_{\mathfrak{p}}^2$ (singular affine solutions of the reduced equation are excluded from the count; Nat.card returns $0$ for an infinite type). Note that $a_{\mathfrak{p}}$ is computed unconditionally (also in the bad-reduction branches) but only used in the good-reduction branch.

(d) Local Euler factor as a Dirichlet series. Let $g_{\mathfrak{p}}(T) = \sum_{k \ge 0} c_{\mathfrak{p},k} T^k \in \mathbb{Z}[[T]]$ be the formal power-series inverse of $f_{\mathfrak{p}}(T)$ relative to the unit $1$ (the constant term of $f_{\mathfrak{p}}$ is $1$ in every branch, so this is the genuine reciprocal $1/f_{\mathfrak{p}}(T)$). The local Euler factor is the arithmetic function $E_{\mathfrak{p}} : \mathbb{N} \to \mathbb{Z}$ given, when $q_{\mathfrak{p}} > 1$, by

$$E_{\mathfrak{p}}(n) = \begin{cases} c_{\mathfrak{p},k} & \text{if } n = q_{\mathfrak{p}}^{\,k} \text{ for some } k \ge 0,\\ 0 & \text{otherwise,}\end{cases}$$

and, as a junk value when $q_{\mathfrak{p}} \le 1$, by the arithmetic function that is $c_{\mathfrak{p},0} = 1$ at $n = 1$ and $0$ elsewhere.

(e) Global Dirichlet coefficients. The arithmetic function $L_W^{\mathrm{coef}} : \mathbb{N} \to \mathbb{Z}$ (W.LFunction) is the unconditional infinite product $\prod'_{\mathfrak{p}} E_{\mathfrak{p}}$ taken in the ring of integer-valued arithmetic functions under Dirichlet convolution, with respect to the topology of pointwise convergence in the discrete topology on $\mathbb{Z}$. If this family is not multipliable in that sense, the product takes the junk value $1$ (the arithmetic function equal to $1$ at $n=1$ and $0$ elsewhere). Arithmetic functions vanish at $n=0$ by definition.

(f) The series. Coerce $L_W^{\mathrm{coef}}$ into $\mathbb{C}$ and set

$$L_W(s) := \sum_{n=1}^{\infty} \frac{L_W^{\mathrm{coef}}(n)}{n^{s}},$$

where $n^s$ is the complex power of the natural number $n$ cast to $\mathbb{C}$, the $n = 0$ term is defined to be $0$, and the sum is Mathlib's tsum: it equals the limit of the finite partial sums over finite subsets when the family $n \mapsto L_W^{\mathrm{coef}}(n)/n^s$ is summable (for $\mathbb{C}$ this is absolute convergence), and takes the junk value $0$ when it is not summable. Thus, at any $s$ with $\operatorname{Re} s > \tfrac32$ where the Dirichlet series fails to converge absolutely, condition 2 forces $\Lambda(s) = 0$ there.

Degenerate readings the quantifiers permit. Condition 2 constrains $\Lambda$ only on $\operatorname{Re} s > \tfrac32$; on the rest of $\mathbb{C}$ (including $s = 1$) it is constrained only by entireness. If $L_W$ happened to vanish identically on that half-plane (for instance through the junk values in (e) or (f)), then $\Lambda \equiv 0$ satisfies conditions 1–2, $\Lambda(1) = 0$ holds, and condition 3 collapses to the bare assertion that $W(\mathbb{Q})$ is infinite. Conversely, if $L_W$ on the half-plane admits no entire extension, no $\Lambda$ exists and the statement is false for that $W$. The theorem asserts existence for every $W$ over $\mathbb{Q}$ with $\Delta(W) \ne 0$, with no further restriction.