The first machine-checked formalization, in any proof assistant, of any component of the Birch-Swinnerton-Dyer (BSD) conjecture pipeline. No prior Lean, Coq, or Isabelle project has formalized Silverman height bounds, Gross-Zagier-Kolyvagin data structures, or the logical architecture of BSD generator search. No new number theory is proved. The algorithms formalized are the engines inside Cremona's mwrank and SageMath. The contribution is the formalization itself and the foundational analysis it enables. Three results that did not previously exist in formal mathematics: (1) A machine-checked axiom/theorem boundary for BSD. The formalization identifies exactly which ingredients must be axiomatized (Gross-Zagier, Kolyvagin, Silverman bound, positive-definiteness) and which can be proved constructively (height bound chain, finite grid membership, search space finiteness). This is the blueprint for any future formally verified BSD solver: the deep analytic theorems interface with type theory through a single chokepoint (the real-valued Silverman bound), and everything below that chokepoint is verified. (2) A logical characterization of the Archimedean/p-adic dichotomy. The positive-definite Archimedean metric (u = 1) is identified as the exact logical modality lowering search complexity from Pi⁰₁ (unbounded, MP) to Delta₀ (bounded verification, BISH). This foundational statement does not appear in the classical literature -- Cremona and Watkins use height bounds as engineering, not as a theorem in reverse mathematics. (3) A logical explanation of the exceptional zero pathology. The p-adic BSD exceptional zero (Mazur-Tate-Teitelbaum) is usually explained analytically: trivial zeros of p-adic L-functions, extra Euler factors. This formalization gives a logical explanation: the p-adic canonical height is not positive-definite, so the MP-to-BISH conversion fails. The search remains unbounded because the metric lacks the topological property needed for logical reduction. This re-reading of a classical analytic obstruction as a failure of logical reducibility is, to our knowledge, new. The axiom budget is minimal -- removing any one ingredient breaks the proof chain -- characterizing the necessary logical interface between analytic number theory and formal verification. This is the first application of constructive reverse mathematics to a Clay Millennium Problem. Formalized in Lean 4 + Mathlib with zero sorry's and zero custom axiom declarations. All analytic axioms enter as Prop-valued hypotheses in a BSDRankOneData structure. Axiom audit: every theorem depends only on propext, Classical. choice, Quot. sound (standard Mathlib infrastructure for the reals). Package contains compiled PDF (10 pages), LaTeX source, and complete Lean 4 source (7 files, ~725 lines) buildable with lake build.
Paul Chun-Kit Lee (Wed,) studied this question.