1
Introduction
▶
1.1
What is machine-checked, and what is assumed
1.2
Reading the graph
2
Definitions
3
The classical inputs
▶
3.1
The \(p\)-adic \(L\)-function
3.2
The standing hypotheses of the paper
3.3
Iwasawa theory and descent
3.4
\(p\)-adic heights
3.5
The Katz measure
3.6
The Eisenstein–Kronecker data
4
Kernel lemmas
5
Theorem A
6
The height dictionary
7
Non-vacuity of the assumption surface
8
Not formalised
▶
Background (§2 of the paper).
The analytic half of Theorem B (Lemma 6.5, Proposition 6.6, Corollary 6.8).
The computations (Part 2 of the paper).
The Coates–Liang–Sujatha input (§7.3).
The questions (Part 4).
Dependency graph
Second derivatives of \(p\)-adic \(L\)-functions and the Shafarevich–Tate group of rank-two CM elliptic curves: formalization blueprint
Barinder S. Banwait
1
Introduction
1.1
What is machine-checked, and what is assumed
1.2
Reading the graph
2
Definitions
3
The classical inputs
3.1
The \(p\)-adic \(L\)-function
3.2
The standing hypotheses of the paper
3.3
Iwasawa theory and descent
3.4
\(p\)-adic heights
3.5
The Katz measure
3.6
The Eisenstein–Kronecker data
4
Kernel lemmas
5
Theorem A
6
The height dictionary
7
Non-vacuity of the assumption surface
8
Not formalised
Background (§2 of the paper).
The analytic half of Theorem B (Lemma 6.5, Proposition 6.6, Corollary 6.8).
The computations (Part 2 of the paper).
The Coates–Liang–Sujatha input (§7.3).
The questions (Part 4).