Dependencies

\(L(E,1)/\Omega _E = 0\).

This is the hypothesis \(L(E,1) = 0\) of the paper’s theorems. For the curve \(y^2 = x^3 - 56x\) it is an exact computation on modular symbols (Stein–Wuthrich, Math. Comp. 82 (2013), §12), and it follows from \(\operatorname{rank}E(\mathbb {Q}) = 2\) and the theorem of Gross–Zagier and Kolyvagin. In Lean it is the field AnalyticData.msymb_zero.

Let \({\mathfrak {f}}\) be the conductor of \(\psi _E\), \(\varepsilon \) its unit character, \(f_0\) a generator of \({\mathfrak {f}}\), and for \(g \in ({\mathcal{O}_K}/{\mathfrak {f}})^\times \) put \(t_g := g\, \Omega _\infty /f_0\). The divisor is \(D_E := \mathrm{Cl}_{\mathfrak {f}}(K) = ({\mathcal{O}_K}/{\mathfrak {f}})^\times /\mu _K\), and for \(a \ge 0\), \(b \ge 1\) the class function \(r_{a,b}\) on \(D_E\) is

This is Definition 5.1 of the paper.

Bannai–Kobayashi, op. cit., (15) and Thm. 1.17 for the coefficients \(e^*_{a,b}\), Thm. 2.9 and Cor. 2.11 for algebraicity. In Lean the structure EKPackage: a coefficient field K, a value field L, a finite nonempty set D of points, six functions r at the indices with \(a + b \le 3\), and a valuation on L at each rational prime. The truncation to six indices is the formalisation’s own.

This is the exception announced above: no theorem of the project reads a value of r. The class functions enter the paper through the analytic half of Theorem B, which is not formalised (Chapter 8). The node is kept so that the assumption surface shown here is the whole of ClassicalInputs.

With \(\operatorname{rank}E(\mathbb {Q}) = 2\), the Pontryagin dual of \(0 \to E(\mathbb {Q}) \otimes \mathbb {Q}_p/\mathbb {Z}_p \to \mathrm{Sel}_{p^\infty }(E/\mathbb {Q}) \to \mathrm{III}(E/\mathbb {Q})[p^\infty ] \to 0\) is an exact sequence of \(\mathbb {Z}_p\)-modules

Exactness is Pontryagin duality applied to the descent sequence; the target \(\mathbb {Z}_p^2\) is the rank, which for \(y^2 = x^3 - 56x\) is a \(2\)-descent with saturation (§7.1 of the paper). In Lean the fields SelmerData.\(\iota \)_inj, SelmerData.\(\pi \)_surj and SelmerData.mw_sha_exact.

For \(p \equiv 1 \pmod4\) there is \(\pi \in \mathbb {Z}[i]\) with \(\pi \bar\pi = p\) and \(a_p = \pi + \bar\pi = 2\, \mathrm{Re}(\pi )\).

Deuring’s theorem. In Lean the field AnalyticData.ap_from_CM, with \(\pi \) a Gaussian integer of norm \(p\).

With \(w(E) = +1\), there is a unit \(U \in \Lambda ^\times \) with \(U(0) = 1\) and

Cited from Mazur–Tate–Teitelbaum, op. cit. In Lean the field AnalyticData.funct_eq states the existence of \(U\), with the substitution \((1+T)^{-1} - 1\) rendered as Lp.subst \(\sigma \).

Let \(L^{\mathrm{K}}(T) \in W[[T]]\) be the Katz branch of the previous node and \(M_2({\mathfrak {p}})\) the second moment of §6.1 of the paper. Then

This is Proposition 6.2(1) of the paper.

Bannai–Kobayashi, op. cit., Prop. 3.3 and Thm. 3.7, with de Shalit II §4. The integral formula for \(c_2(L^{\mathrm{K}})\) as a second moment (Proposition 6.1 of the paper) is not carried in Lean; only this congruence is, as the field KatzData.grading_congr: \(\exists \, \kappa _0 \in W^\times ,\ p^2\bigl(\kappa _0 \cdot \mathrm{coeff}_2\, L^{\mathrm{Katz}} - \texttt{m2core}\bigr) \in (p^3)\).

\(a_p^2 \le 4p\).

Hasse’s theorem. In Lean the field AnalyticData.hasse.

For a good ordinary prime \(p\) with unit root \(\alpha _p\),

Cited from Mazur–Tate–Teitelbaum, Invent. Math. 84 (1986), 1–48. In Lean the field AnalyticData.interp states the identity in \(\mathbb {Q}_p\) between the constant coefficient of \(L_p\) and the modular symbol.

Let \(L^{\mathrm{Katz}}_{\mathfrak {p}}(T)\) be the restriction of the Katz measure \(\mu _{{\mathfrak {f}}{\mathfrak {p}}^\infty }\) to the cyclotomic line through the central character of \(\psi _E\). Then

for some \(c_p \in \overline{\mathbb {Q}}_p^\times \) and some unit power series \(u(T)\) over the ring of integers of a finite extension of \(\mathbb {Q}_p\), and \(v_p(c_p) = 0\) for every split \(p \notin S_{\mathrm{cmp}}\), where \(S_{\mathrm{cmp}} := \{ p : p \mid 6N\, \operatorname{N}{\mathfrak {f}}\} \cup \operatorname {supp}(\omega _E)\) and \(\omega _E\) is the period ratio. This is Lemma 3.5 of the paper.

Bannai–Kobayashi, Duke Math. J. 153 (2010), Cor. 3.12, with de Shalit, Iwasawa theory of elliptic curves with complex multiplication (1987), II §4, for the local terms. In Lean the field KatzData.comparison: after base change to the coefficient ring \(W\), \(L_p = c \cdot u(T) \cdot L^{\mathrm{Katz}}\) with \(c \in W^\times \) and \(u\) a unit series. The conclusion \(v_p(c_p) = 0\) is part of the field’s type, for the primes \(S_{\mathrm{cmp}}\) does not exclude; for \(y^2 = x^3 - 56x\) the period ratio is supported on \(\{ 2, 7\} \), so \(S_{\mathrm{cmp}}\) contains no split prime.

\(X/TX \cong \mathrm{Sel}_{p^\infty }(E/\mathbb {Q})^\vee \) as \(\mathbb {Z}_p\)-modules.

Mazur, Invent. Math. 18 (1972), in the form of an isomorphism, which is what the hypotheses of Theorem A give: \(p\) is a good ordinary prime, \(E(\mathbb {Q})[p] = 0\), and \(p \nmid \prod _v c_v\). In Lean the field IwasawaData.control is the \(\mathbb {Z}_p\)-linear equivalence.

\(X = \mathrm{Sel}_{p^\infty }(E/\mathbb {Q}_\infty )^\vee \) has no nonzero finite \(\Lambda \)-submodule.

Greenberg, Iwasawa theory for elliptic curves, LNM 1716 (1999), Prop. 4.14, which applies because \(X\) is \(\Lambda \)-torsion and \(E(\mathbb {Q})[p] = 0\). In Lean the field IwasawaData.no_finite_submodule.

For a split prime \(p\) with \(\prod _v c_v/(\# E(\mathbb {Q})_{\mathrm{tors}})^2 = 1\),

and \(\tilde c_2(p) \in \mathbb {Z}_p^\times \) if and only if the cyclotomic \(p\)-adic height pairing on \(E(\mathbb {Q})\) is nondegenerate, \(v_p(\operatorname{Reg}_\gamma ) = 0\), and \(\mathrm{III}(E/\mathbb {Q})[p^\infty ] = 0\). This is display (7) of the paper.

Schneider, Invent. Math. 79 (1985), Thms. 2 and 2\('\), and Perrin-Riou, Invent. Math. 109 (1992), §§3.4.2–3.4.3, in the form of Stein–Wuthrich, Math. Comp. 82 (2013), Thm. 6.1, under Rubin’s main conjecture. In Lean the fields HeightData.spr_padicBSD (the norm identity) and HeightData.spr_nondeg (the equivalence), both stated for the height layer’s own values c2norm and shaOrd; the next node ties those values to the analytic jet and to \(\mathrm{III}\).

The value c2norm of the height layer is \(\tilde c_2(p)\), and shaOrd is a \(p\)-adic unit if and only if \(\mathrm{III}(E/\mathbb {Q})[p^\infty ] = 0\).

These are not theorems of the literature. They are the two equations that weld the height layer to the analytic and Selmer layers, and the Dictionary depends on them. In Lean the fields PrimeData.c2norm_tie and PrimeData.shaOrd_tie. The height layer keeps its own values so that the witness of Theorem 31 can be constructed.

Let \(X = \mathrm{Sel}_{p^\infty }(E/\mathbb {Q}_\infty )^\vee \). There are \(n\), elements \(f_1, \dots , f_n \in \Lambda \) and a \(\Lambda \)-linear map \(X \to \prod _i \Lambda /(f_i)\) with finite kernel and cokernel, such that \(\prod _i f_i\) and \(L_p(E,T)\) generate the same ideal.

The pseudo-isomorphism is the structure theorem for finitely generated \(\Lambda \)-modules, Washington, Introduction to Cyclotomic Fields, 2nd ed., Thm. 13.12. The identification of the characteristic ideal with \((L_p)\) is Rubin, Invent. Math. 103 (1991), Thm. 12.3, through Yager’s identification of the two-variable characteristic ideal with the Katz measure restricted to the cyclotomic line. In Lean the field IwasawaData.rubin_structure states the conjunction.

For every split prime \(p \notin S_E\), \(a_p \not\equiv 1 \pmod p\); and \((\# E(\mathbb {Q})_{\mathrm{tors}})^2 / \prod _v c_v = 1\).

The first is the clause \(S_{\mathrm{an}} \subseteq S_E\) of the paper’s definition (8) of the excluded set. The second is the arithmetic of Table 1: \(2^2/4 = 1\). In Lean the fields ClassicalInputs.notAnomalous and ClassicalInputs.torsSqOverTam_eq. What the first assumes beyond the proved Lemma 21 is the single value \(a_5 \ne -4\).

At a good ordinary prime, \(X^2 - a_pX + p\) has a root \(\alpha _p \in \mathbb {Z}_p^\times \).

Hensel’s lemma at a good ordinary prime. In Lean the field AnalyticData.alpha_root states the equation for the unit \(\alpha \).

For \(f \in \Lambda = \mathbb {Z}_p[[T]]\), \(\mu (f) = 0\) means some coefficient of \(f\) is a \(p\)-adic unit, and \(\lambda (f)\) is the least index of a unit coefficient.

For \(p\) split with \(\alpha _p\) the unit root of \(X^2 - a_pX + p\), and \(L_p(E,T) = c_0(p) + c_1(p)\, T + c_2(p)\, T^2 + \cdots \), set

This is Definition 3.2 of the paper.

1. Let \(R\) be a commutative ring and \(A, B \in R[[T]]\) with \(c_0(B) = c_1(B) = 0\). Then \(c_2(AB) = A(0)\, c_2(B)\).

2. For \(p \notin S_E\) split, \(c_2(p)\) is a \(p\)-adic unit if and only if \(c_2(L^{\mathrm{K}})\) is.

This is Lemma 6.3 of the paper.

Let \(R\) be a commutative ring in which \(2x = 0\) implies \(x = 0\), let \(f, U \in R[[T]]\) with \(f(0) = 0\) and \(U(0) = 1\), and suppose \(f\bigl((1+T)^{-1} - 1\bigr) = U\, f\). Then the coefficient of \(T\) in \(f\) is \(0\).

Let \(E/\mathbb {Q}\) have complex multiplication by \(\mathbb {Z}[i]\) and let \(p \equiv 1 \pmod4\) be a prime of good reduction. Then \(a_p\) is even, and \(p\) is anomalous for \(E\) if and only if \(p = 5\) and \(a_5 = -4\). This is Lemma 2.2 of the paper, for split \(p\).

Let \(X\) be a finitely generated \(\Lambda \)-module with no nonzero finite submodule, and suppose there is a \(\Lambda \)-linear map \(X \to \prod _i \Lambda /(f_i)\) with finite kernel and cokernel such that \(\prod _i f_i\) and \(T^2\) generate the same ideal. If \(\dim _{\mathbb {Q}_p}(X/TX) \otimes \mathbb {Q}_p \ge 2\), then \(TX = 0\) and \(X \cong \mathbb {Z}_p^2\).

Let \(0 \to A \xrightarrow {\iota } S \xrightarrow {\pi } \mathbb {Z}_p^2 \to 0\) be an exact sequence of finitely generated \(\mathbb {Z}_p\)-modules with \(S \cong \mathbb {Z}_p^2\). Then \(A = 0\) and \(\mathrm{rank}_{\mathbb {Z}_p} S = 2\).

Let \(f \in \Lambda \) with \(c_0(f) = c_1(f) = 0\) and \(c_2(f) \in \mathbb {Z}_p^\times \). Then \(f = T^2 u\) for a unit \(u \in \Lambda ^\times \); hence \(\mu (f) = 0\), \(\lambda (f) = 2\), and \(f\) and \(T^2\) generate the same ideal.

Assume \(L(E,1) = 0\) and \(w(E) = +1\). Then for every good ordinary prime \(p\), writing \(L_p(E,T) = c_0(p) + c_1(p)\, T + c_2(p)\, T^2 + \cdots \),

This is Lemma 3.1 of the paper.

Let \(W\) be a local integral domain with maximal ideal \((\varpi )\), let \(\kappa _0 \in W^\times \), and let \(c, m \in W\) with \(\varpi ^2(\kappa _0 c - m) \in (\varpi ^3)\). Then \(c\) is a unit if and only if the residue of \(m\) is nonzero. Applied to the grading congruence: \(v_p(c_2(L^{\mathrm{K}})) = 0\) if and only if the criterion class \(\mathfrak {c}({\mathfrak {p}}) := p^{-2}M_2({\mathfrak {p}}) \bmod \mathfrak {m}_W\) is nonzero. This is Proposition 6.2(2) of the paper.

Let \(E/\mathbb {Q}\) have CM by the maximal order \({\mathcal{O}_K}\) of an imaginary quadratic field \(K\), with \(\operatorname{rank}E(\mathbb {Q}) = 2\), \(L(E,1) = 0\) and \(w(E) = +1\), and let \(p \notin S_E\) be a split prime of good reduction. The following are equivalent:

1. \(\tilde c_2(p) \in \mathbb {Z}_p^\times \);

2. the cyclotomic \(p\)-adic height pairing on \(E(\mathbb {Q})\) is nondegenerate with \(v_p(\operatorname{Reg}_\gamma ) = 0\), and \(\mathrm{III}(E/\mathbb {Q})[p^\infty ] = 0\).

This is Proposition 4.2 of the paper, and the equivalence (1) \(\iff \) (2) of Theorem B.

Let \(p = {\mathfrak {p}}\bar{\mathfrak {p}}\) be a split prime of good reduction with \(p \nmid \prod _v c_v \cdot \# E(\mathbb {Q})_{\mathrm{tors}}\), not anomalous. Then \(\tilde c_2(p) \in \mathbb {Z}_p^\times \) if and only if \(c_2(p) \in \mathbb {Z}_p^\times \). This is Proposition 3.3 of the paper.

ClassicalInputs does not by itself entail \(\mathrm{III}(E/\mathbb {Q})[p^\infty ] = 0\): there is a second instance ToySha : ClassicalInputs at which \(\mathrm{III}[p^\infty ] \ne 0\), \(\mu _{\mathrm{an}} \ne 0\) and \(\lambda _{\mathrm{an}} \ne 2\) at every split prime, and at which the computed \(5\)-adic expansion of \(c_2(5)\) is false. The unit condition, not the interface, is what excludes this world.

There is an instance ToyTrivial : ClassicalInputs, with every field discharged in a toy world (\(S = \varnothing \), \(D_E\) a single point, \(L_p = T^2\)) and no incomplete proof. So ClassicalInputs is consistent and the theorems are not vacuously true.

Let \(E/\mathbb {Q}\) have CM by the maximal order \({\mathcal{O}_K}\) of an imaginary quadratic field \(K\), with \(\operatorname{rank}E(\mathbb {Q}) = 2\), \(L(E,1) = 0\) and \(w(E) = +1\). Let \(p = {\mathfrak {p}}\bar{\mathfrak {p}}\ge 5\) be a split prime of good reduction with \(p \notin S_E\) and \(\tilde c_2(p) \in \mathbb {Z}_p^\times \). Then:

1. \(\mu _{\mathrm{an}}({\mathfrak {p}}) = 0\) and \(\lambda _{\mathrm{an}}({\mathfrak {p}}) = 2\);

2. \(\operatorname{corank}_{\mathbb {Z}_p}\, \operatorname{Sel}_{p^\infty }(E/\mathbb {Q}) = 2\);

3. \(\mathrm{III}(E/\mathbb {Q})[p^\infty ] = 0\).

This is Theorem 3.8 of the paper.