The Birch and Swinnerton-Dyer Conjecture and LPO: Archimedean Polarization as Constructive Escape from the u-Invariant Obstruction (Paper 48, Constructive Reverse Mathematics Series)

Paper 48, Constructive Reverse Mathematics Series Description: We apply Constructive Reverse Mathematics to calibrate the logical strength of the Birch and Swinnerton-Dyer (BSD) conjecture for elliptic curves over Q. Four theorems (B1-B4) constitute the calibration. Theorem B1 proves that deciding L (E, 1) = 0 (the analytic rank question) is equivalent to the Limited Principle of Omniscience for R. Theorem B2 shows the Neron-Tate height pairing provides a positive-definite inner product on E (Q) tensor R, an Archimedean polarization available because positive-definite forms exist in all dimensions over R. Theorem B3 proves the regulator det > 0 using only BISH (no omniscience). Theorem B4 proves the p-adic height pairing cannot be positive-definite for rank >= 5 (since u (Qₚ) = 4), explaining the Mazur-Tate-Teitelbaum exceptional zero pathology. The central finding: BSD is the first conjecture in the five-conjecture atlas where the Archimedean polarization is available. Papers 45-47 proved it is blocked at every finite prime. The analytic side of BSD calibrates at LPO; the algebraic side is BISH. All results are formalized in Lean 4 over Mathlib with 0 errors, 0 sorry, and 9 custom axioms. Bundle includes LaTeX source, compiled PDF, and full Lean 4 formalization.