This blueprint accompanies the Lean formalization of On monic abelian cubic polynomials, by Shubhrajit Bhattacharya and Andrew O’Desky. It follows our November 2026 revision, which extends the trace-one results of the arXiv version to arbitrary trace.

The paper’s labelled statements appear below. Each has links to its Lean statement and proof, followed by a short explanation of the argument. The numbering here is local to the blueprint; the TeX labels retained in the source identify the corresponding results in the paper.

Our proof uses Poisson summation and the critical-line mean-square estimate of Chandrasekharan and Narasimhan. Both are explicit hypotheses in Lean. The comparison with Santens’s theorem and the alternative ideal count use the additional inputs listed in the last chapter.

For the strip estimate, Lean uses the residue theorem in place of Titchmarsh’s result. For the coefficient sum, it uses Perron’s formula and contour shifting in place of Alberts’s theorem. We describe these arguments at the corresponding places. For the moduli theorem, we formalize the rational-point correspondence used in counting; the assertion over general bases is not formalized.

The dependency graph is extracted from the Lean proofs. Alongside the paper’s results, it shows selected supporting lemmas used by several proofs. An arrow follows a dependency in Lean, possibly through other helpers omitted from the graph. Green nodes have formalized statements and proofs, relative to any literature inputs shown. Nodes for assumed inputs have formalized statements and no proofs. The correspondence record gives further details.