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

2 Definitions

Definition 1 The normalised second jet
✓
#

Lean declarations

  • FinShaRank2.c2tilde
  • FinShaRank2.PrimeData.c2tilde

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

\[ \tilde c_2(p) \; :=\; c_2(p) \cdot (1 - \alpha _p^{-1})^{-2} \cdot \frac{(\# E(\mathbb {Q})_{\mathrm{tors}})^2}{\prod _v c_v} . \]

This is Definition 3.2 of the paper.

Lean ▶

c2tilde is a total function of its three numerical arguments, matching the display. At an anomalous prime \(1 - \alpha _p^{-1} = 0\) and the value is a junk value; every theorem about c2tilde therefore carries the non-anomalous hypothesis explicitly. PrimeData.c2tilde applies it to the \(L\)-function, unit root and rational factor of a per-prime bundle.

Definition 2 Iwasawa invariants of a power series
✓
#

Lean declarations

  • FinShaRank2.MuZero
  • FinShaRank2.lambdaAn

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.

Lean ▶

MuZero f is \(\exists n,\ \mathrm{IsUnit}(\mathrm{coeff}\ n\ f)\) and lambdaAn f is the infimum of that set of indices, with the convention \(\inf \varnothing = 0\). The two are used together: \(\lambda \) carries information only where \(\mu = 0\).