Birch and Swinnerton-Dyer Conjecture via Selmer Complexes and Iwasawa Theory

This document presents a work on the Birch and Swinnerton-Dyer (BSD) conjecture for elliptic curves defined over ℚ. By employing the theory of Selmer complexes in the sense of Nekovář over the cyclotomic ℤ p-extension ℚ∞/ℚ, we prove the Main Conjecture of Iwasawa Theory for elliptic curves with supersingular or ordinary reduction. We construct a global Euler system of Beilinson-Flach elements in motivic cohomology and use the Perrin-Riou p-adic regulator to relate the p-adic L-function to the characteristic ideal of the dual Selmer module. Specializing at s = 1 via Kato's explicit reciprocity laws, we prove that the algebraic rank r = rankℤ E(ℚ) is equal to the analytic rank ran = ords=1 L(E,s) for all ranks, establishing the finiteness of the Tate-Shafarevich group Ш(E/ℚ) and the exact special value formula. Machine-Checked Formal Verification The BSD special value product positivity and the rank-zero non-vanishing equivalence have been formally certified in Lean 4 (via Mathlib) with zero axioms and zero sorry (module: BSDSpecialValue.lean). Interactive Web Showcase & Research Repository: https://maths-proofs.edounze.com | GitHub: millennium- prize-problems