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.

\(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.

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 \).

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 \).

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

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

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\).

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\).

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.

\(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.

\(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.

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 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 \(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.

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)\).

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.