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

6 The height dictionary

Proposition 29 Analytic–arithmetic dictionary
✓
#

Uses

Lean declarations

  • FinShaRank2.prop_dictionary

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.

Lean ▶

Both directions are a rewrite along the two identifications of Classical input 15 and the equivalence of Classical input 14. No non-anomality hypothesis is needed: this route never converts between \(\tilde c_2\) and \(c_2\).