Second derivatives of \(p\)-adic \(L\)-functions and the Shafarevich–Tate group of rank-two CM elliptic curves: formalization blueprint

5 Theorem A

Theorem 28 Theorem A
✓

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.

Lean ▶

prop_consequence takes \(H : \texttt{ClassicalInputs}\), a split prime \(p \notin H.S\), and the unit condition at \(p\), and concludes the four statements on the Pontryagin-dual side: MuZero, lambdaAn = 2, finrank SelDual = 2 and Subsingleton ShaDual. The curve-level hypotheses are carried by \(H\) and not restated.

The proof follows the paper’s steps. Proposition 22 turns the unit condition into \(c_2(p) \in \mathbb {Z}_p^\times \). Lemma 20 gives \(c_0 = c_1 = 0\). Lemma 23 gives \(L_p = T^2 u\), hence (1), and the characteristic ideal \((T^2)\). Mazur’s control theorem (12) and the surjection of the descent sequence (13) give \(\mathrm{rank}\, (X/TX) \ge 2\). Rubin’s structure statement (10) and the absence of finite submodules (11) feed Lemma 24, which gives \(\mathrm{Sel}_{p^\infty }(E/\mathbb {Q})^\vee \cong \mathbb {Z}_p^2\) through the control isomorphism. Lemma 25 on the descent sequence gives (2) and (3).