8 Not formalised

The items below are content of the paper that the formalisation does not attempt. None carries a \lean tag, and none is a node the proved theorems depend on.

Background (§2 of the paper).

The theorem of Gillard and Sinnott that the \(\mu \)-invariant of every branch of the Katz measure vanishes, and the facts about the Kronecker theta function recalled from Bannai–Kobayashi. Expository; nothing downstream depends on them.

The analytic half of Theorem B (Lemma 6.5, Proposition 6.6, Corollary 6.8).

That the unit condition is equivalent to \(v_{\mathfrak {p}}(B({\mathfrak {p}})) = 2\) for the combination \(B({\mathfrak {p}})\) of three Eisenstein–Kronecker class sums has no Lean rendering. A formalisation would begin at Lemma 6.5. The arithmetic half is Proposition 29. This is why nothing consumes the class functions of Classical input 18.

The computations (Part 2 of the paper).

The cyclotomic regulator at every split prime below \(30{,}000\) for each of the five curves, the chance model, and the evaluation of \(B({\mathfrak {p}})\). The scripts and their outputs are in code/, not in the Lean tree.

The Coates–Liang–Sujatha input (§7.3).

The vanishing of \(\mathrm{III}[p^\infty ]\) for the five curves at every split \(p {\lt} 30{,}000\), and its transfer along the \(2\)-isogeny. Cited from the literature.

The questions (Part 4).

Not a target for formalisation.