Gross–Zagier–Kolyvagin: if $\operatorname{ord}_{s=1} L(E,s) \le 1$ then it equals the rank of $E(\mathbb{Q})$

Read-back

Theorem BSD.birch_swinnerton_dyer_of_analyticOrderAt_le_one. The statement is universally quantified over three objects and carries one typeclass assumption and two explicit hypotheses. It asserts:

For every Weierstrass curve $W$ over $\mathbb{Q}$ which is elliptic (in the sense unfolded below), for every function $\Lambda : \mathbb{C} \to \mathbb{C}$, if $\Lambda$ satisfies the two-part predicate $\mathrm{IsLFunction}\,W\,\Lambda$ (unfolded below) and the analytic order of vanishing of $\Lambda$ at the complex point $1$ is at most $1$ in $\mathbb{N}\cup\{\infty\}$, then

$$\operatorname{ord}_{z=1}\Lambda \;=\; \operatorname{rank}(W)$$

as elements of $\mathbb{N}\cup\{\infty\}$, where the right-hand side is a natural number (unfolded below) cast into $\mathbb{N}\cup\{\infty\}$.

Every term is now unfolded.

The curve $W$. A Weierstrass curve over $\mathbb{Q}$ is literally a $5$-tuple of rational numbers $(a_1,a_2,a_3,a_4,a_6)$, thought of as the equation $Y^2 + a_1 XY + a_3 Y = X^3 + a_2 X^2 + a_4 X + a_6$. Its discriminant is the polynomial expression

$$\Delta = -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$. The typeclass assumption "$W$ is elliptic" means exactly that $\Delta$ is a unit of $\mathbb{Q}$, i.e. $\Delta \neq 0$. No other condition (e.g. integrality or minimality of the coefficients) is imposed on $W$.

The right-hand side $\operatorname{rank}(W)$. By the bundled definition, $\operatorname{rank}(W) := \operatorname{finrank}_{\mathbb{Z}}\big(W(\mathbb{Q})\big) \in \mathbb{N}$, where:

• $W(\mathbb{Q})$ denotes the type of nonsingular affine points of $W$: it consists of one distinguished element $\mathcal{O}$ (the point at infinity, which is the group zero) together with all pairs $(x,y)\in\mathbb{Q}^2$ such that

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

Mathlib equips this type (over any field, here $\mathbb{Q}$) with the chord-and-tangent addition, making it an abelian group, hence a $\mathbb{Z}$-module.

• $\operatorname{finrank}_{\mathbb{Z}}(M) := \operatorname{toNat}\big(\operatorname{rank}_{\mathbb{Z}} M\big)$, where $\operatorname{rank}_{\mathbb{Z}} M$ is the cardinal supremum of $|S|$ over all $\mathbb{Z}$-linearly independent subsets $S \subseteq M$, and $\operatorname{toNat}$ sends a finite cardinal to the corresponding natural number and every infinite cardinal to $0$. Consequently $\operatorname{rank}(W)$ is the largest size of a $\mathbb{Z}$-linearly independent set of points if that supremum is finite, and is the junk value $0$ if there are arbitrarily large linearly independent sets. Torsion points never contribute. Nothing in the statement asserts or assumes that $W(\mathbb{Q})$ is finitely generated; the definition is total and returns a natural number regardless.

The left-hand side $\operatorname{ord}_{z=1}\Lambda$. This is Mathlib's analyticOrderAt Λ 1, valued in $\mathbb{N}\cup\{\infty\}$, where the point is the complex number $1$. It is defined by cases:

• if $\Lambda$ is not analytic at $1$, the value is the junk value $0$;
• if $\Lambda$ is analytic at $1$ and $\Lambda$ vanishes identically on some neighbourhood of $1$, the value is $\infty$;
• otherwise the value is the unique $n\in\mathbb{N}$ such that, on a neighbourhood of $1$, $\Lambda(z) = (z-1)^n g(z)$ for some $g$ analytic at $1$ with $g(1)\neq 0$. In particular the value is $0$ iff $\Lambda(1)\neq 0$ (when analytic).

The hypothesis $h$: $\operatorname{ord}_{z=1}\Lambda \le 1$ in $\mathbb{N}\cup\{\infty\}$. Since $\infty \le 1$ is false, this says the order is $0$ or $1$; it therefore excludes the case that $\Lambda$ vanishes identically near $1$. Given the differentiability hypothesis below, $\Lambda$ is analytic at $1$, so the "not analytic" branch does not arise, and $h$ says exactly: either $\Lambda(1)\neq 0$, or $\Lambda$ has a simple zero at $1$ (i.e. $\Lambda(1)=0$ and $\Lambda(z)=(z-1)g(z)$ near $1$ with $g$ analytic, $g(1)\neq 0$).

The hypothesis $h_\Lambda$: $\mathrm{IsLFunction}\,W\,\Lambda$. By the bundled definition this is the conjunction of two conditions:

1. $\Lambda$ is complex-differentiable at every point of $\mathbb{C}$ (an entire function);
2. for every $s\in\mathbb{C}$ with $\operatorname{Re}(s) > 3/2$, one has $\Lambda(s) = L_W(s)$, where $L_W(s)$ is Mathlib's WeierstrassCurve.LSeries W s, unfolded next.

The Dirichlet series $L_W(s)$. It is defined as

$$L_W(s) := \sum_{n\ge 1}{}^{\prime}\; \frac{c_n}{n^s}, \qquad c_n := \big(\mathcal{L}_W(n)\big) \in \mathbb{Z} \hookrightarrow \mathbb{C},$$

where $\sum'$ is Mathlib's tsum: the sum of the series if the family $n\mapsto c_n n^{-s}$ is summable in $\mathbb{C}$ (for complex numbers this is equivalent to absolute convergence), and the junk value $0$ if it is not summable. The $n=0$ term is defined to be $0$; $n^s$ means $\exp(s\log n)$ for $n\ge 1$. Thus condition 2 requires $\Lambda(s)$ to equal this value for all $s$ with $\operatorname{Re}(s)>3/2$, including equalling $0$ at any such $s$ where the series fails to converge absolutely.

The coefficient sequence $\mathcal{L}_W$ (Mathlib's WeierstrassCurve.LFunction). It is an integer-valued arithmetic function (a function $\mathbb{N}\to\mathbb{Z}$ with $\mathcal{L}_W(0)=0$), defined as the Euler product

$$\mathcal{L}_W := \prod_{\mathfrak{p}}{}^{\prime}\; E_{\mathfrak{p}},$$

where:

• $\mathfrak{p}$ ranges over the height-one prime spectrum of $\mathcal{O}_{\mathbb{Q}}$, the ring of integers of $\mathbb{Q}$ viewed as a number field (i.e. over all nonzero prime ideals of $\mathcal{O}_{\mathbb{Q}}\cong\mathbb{Z}$);
• $\prod'$ is Mathlib's tprod of arithmetic functions under Dirichlet convolution, taken in the topology of pointwise convergence with $\mathbb{Z}$ discrete: if the family is multipliable it is the limit of finite partial products, and otherwise it is the junk value $1$ (the Dirichlet identity $\mathbf{1}$, equal to $1$ at $n=1$ and $0$ elsewhere);
• for each $\mathfrak{p}$, let $K_\mathfrak{p}$ be the $\mathfrak{p}$-adic completion of $\mathbb{Q}$ and $R_\mathfrak{p}\subset K_\mathfrak{p}$ its valuation ring (a discrete valuation ring). Let $W_\mathfrak{p}$ be $W$ base-changed to $K_\mathfrak{p}$ (same five coefficients viewed in $K_\mathfrak{p}$). Then $E_\mathfrak{p}$ is the local Euler factor of $W_\mathfrak{p}$ with respect to $R_\mathfrak{p}$, defined as follows.

The local Euler factor $E_\mathfrak{p}$. Set $q := \#\kappa$, the cardinality (as a natural number, junk value $0$ if infinite) of the residue field $\kappa$ of $R_\mathfrak{p}$. Let $W' :=$ the minimal model of $W_\mathfrak{p}$, defined as $C\cdot W_\mathfrak{p}$ for a change of variables $C$ (selected by the axiom of choice) such that $C\cdot W_\mathfrak{p}$ is minimal: it is integral (its five coefficients lie in $R_\mathfrak{p}$, so it is the base change of some curve over $R_\mathfrak{p}$) and the multiplicative valuation $v(\Delta_{W'})\le 1$ of its discriminant is maximal among all changes of variables producing integral models. Let $\widetilde{W'}$ be the reduction of $W'$: a chosen integral model of $W'$ over $R_\mathfrak{p}$ with its coefficients mapped to $\kappa$. Set

$$a := q + 1 - \#\,\widetilde{W'}(\kappa) \in \mathbb{Z},$$

where $\widetilde{W'}(\kappa)$ is the type of nonsingular affine points of $\widetilde{W'}$ over $\kappa$ together with the point at infinity, as described above for $W(\mathbb{Q})$ but over $\kappa$ (again $\#$ is $0$ if that type is infinite). The local polynomial $f_\mathfrak{p}(T)\in\mathbb{Z}[T]$ is chosen by the following case split on $W'$:

• if $W'$ has good reduction (it is minimal and $v(\Delta_{W'}) = 1$): $f_\mathfrak{p} = 1 - aT + qT^2$;
• else if $W'$ has split multiplicative reduction (it is minimal, $v(\Delta_{W'})<1$, $v(c_4(W'))=1$, and, writing $I$ for the chosen integral model, the polynomial $c_4(I)\,T^2 + a_1(I)c_4(I)\,T - \big(54\,b_6(I) - 3\,b_2(I)b_4(I) + a_2(I)c_4(I)\big)$ splits over $\kappa$): $f_\mathfrak{p} = 1 - T$;
• else if $W'$ has multiplicative reduction (minimal, $v(\Delta_{W'})<1$, $v(c_4(W'))=1$): $f_\mathfrak{p} = 1 + T$;
• otherwise: $f_\mathfrak{p} = 1$.

Here $c_4 = b_2^2 - 24 b_4$. Then $E_\mathfrak{p}$ is obtained from the formal power series $f_\mathfrak{p}(T)^{-1}\in\mathbb{Z}[[T]]$ (Mathlib's invOfUnit with respect to the unit $1$, i.e. the series with constant term $1$ determined recursively so as to invert $f_\mathfrak{p}$ when $f_\mathfrak{p}$ has constant term $1$, which holds in all four cases) by substituting $T = q^{-s}$: if $q > 1$, $E_\mathfrak{p}(q^k)$ is the $k$-th coefficient of $f_\mathfrak{p}^{-1}$ and $E_\mathfrak{p}(n) = 0$ for $n$ not a power of $q$; if $q \le 1$ (junk regime), $E_\mathfrak{p}$ is the constant term of $f_\mathfrak{p}^{-1}$ times the Dirichlet identity $\mathbf{1}$.

Logical shape and edge cases.

• The statement is: $\forall W\ \forall(\text{ellipticity of }W)\ \forall \Lambda\ \big(\mathrm{IsLFunction}\,W\,\Lambda \;\wedge\; \operatorname{ord}_{z=1}\Lambda \le 1\big) \Rightarrow \operatorname{ord}_{z=1}\Lambda = \iota(\operatorname{rank} W)$, with $\iota : \mathbb{N}\hookrightarrow\mathbb{N}\cup\{\infty\}$ the canonical inclusion. It is a universal statement about every entire $\Lambda$ agreeing with $L_W$ on the half-plane $\operatorname{Re}(s) > 3/2$; it does not assert that any such $\Lambda$ exists. For a given $W$, if no entire function agrees with $L_W$ on that half-plane, the statement is vacuously true for that $W$.
• Combining $h$ with the conclusion, the theorem asserts exactly: under the hypotheses, $\operatorname{rank}(W) = 0$ when $\Lambda(1)\neq 0$, and $\operatorname{rank}(W) = 1$ when $\Lambda$ has a simple zero at $1$. It says nothing when the order of $\Lambda$ at $1$ is $\ge 2$ or $\infty$.
• Because the conclusion equates an $\mathbb{N}\cup\{\infty\}$-value with the image of a natural number, it in particular reasserts that the order is finite (already forced by $h$).
• The junk values that can in principle enter are: $\operatorname{rank}(W) = 0$ when $W(\mathbb{Q})$ admits arbitrarily large $\mathbb{Z}$-linearly independent subsets; $L_W(s) = 0$ at any $s$ with $\operatorname{Re}(s) > 3/2$ where the Dirichlet series is not absolutely summable; $\mathcal{L}_W = \mathbf{1}$ if the Euler product is not multipliable; $\#\kappa = 0$ or $\#\widetilde{W'}(\kappa) = 0$ if the corresponding types are infinite; and $\operatorname{ord}_{z=1}\Lambda = 0$ if $\Lambda$ were not analytic at $1$ (ruled out by the entireness hypothesis). Whether any of these regimes actually occurs for curves over $\mathbb{Q}$ is not asserted by the statement.
• The choice of minimal model $W'$ and of integral model in the reduction is made via the axiom of choice; the local polynomial is defined in terms of these specific chosen models.