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

1 Introduction

This blueprint tracks the Lean 4 formalisation (library FinShaRank2, Mathlib v4.33.1) of the paper Second derivatives of \(p\)-adic \(L\)-functions and the Shafarevich–Tate group of rank-two CM elliptic curves, arXiv:2609.08431. The curve throughout is \(E : y^2 = x^3 - 56x\) over \(\mathbb {Q}\): CM by \(\mathbb {Z}[i]\), conductor \(N = 12544\), rank \(2\), torsion \(\mathbb {Z}/2\), \(\prod _v c_v = 4\), root number \(w(E) = +1\); the primes are the split primes \(p \equiv 1 \pmod4\).

Theorem A of the paper (Theorem 3.8) is the node TheoremA (Chapter 5). Theorem B (Theorem 6.7) has no Lean counterpart; the arithmetic half of its equivalence is the node Dictionary (Chapter 6).

1.1 What is machine-checked, and what is assumed

Mathlib has no Selmer group, no Shafarevich–Tate group and no \(p\)-adic \(L\)-function. The formalisation therefore assumes the classical theorems the paper takes from the literature, as fields of one structure, ClassicalInputs, and machine-checks everything the paper deduces from them. Every theorem takes H : ClassicalInputs as an ordinary hypothesis. There is no axiom declaration in the project and no conjectural hypothesis.

Every declaration marked \leanok in a proof below is sorry-free, uses no native_decide, and is confirmed by FinShaRank2/AxiomAudit.lean to depend on no axiom beyond propext, Classical.choice and Quot.sound. The derivation of the two theorems from the classical inputs has also been checked with Lean’s comparator, as the README of the formalisation records.

1.2 Reading the graph

There are three kinds of node.

  • Classical inputs (Chapter 3), in the environment Classical input. Each is a theorem of the literature, or a standing hypothesis of the paper, stated in Lean as a field of the assumption surface. Each node names the field and the source. None has a proof in the project, and none will: they are cited. In the graph they have a green border, which means the statement is in Lean, and no green body, which means no proof is.

  • Kernel lemmas (Chapter 4) and the two theorems (Chapters 5 and 6). Each is proved in Lean, and its node has a green body. A node is dark green when everything it depends on is proved, and light green when something it depends on is a classical input. The theorems are light green: that is the statement “proved modulo the literature”, made visible.

  • Definitions (Chapter 2), drawn as boxes.

A dashed arrow from \(A\) to \(B\) means the Lean proof of \(B\) consumes \(A\). The arrows into TheoremA are the paper’s Steps 1–5 in the order the proof takes them, and the classical inputs among them are exactly the theorems the paper cites there: Mazur–Tate–Teitelbaum, Rubin, Greenberg, Mazur.

Material the paper contains but the formalisation does not attempt is listed in Chapter 8 with no theorem-like environment, so it cannot be mistaken for an oversight.