Conditional BSD Implications with Twelve Explicit Debt Assumptions

The Birch and Swinnerton-Dyer conjecture predicts that for an elliptic curve E/\mathbb{Q} the Mordell-Weil rank equals the order of vanishing of the Hasse-Weil L-function at s = 1. It also predicts that the leading Taylor coefficient is expressed by an explicit formula involving the real period, regulator, Shafarevich-Tate group, Tamagawa numbers, and torsion. This remains an open Millennium Prize problem. This paper presents a machine-checked dependency graph for selected implications around BSD. The release-scoped proof environment contains 181 kernel implications and 187 hypotheses. Twelve A_* declarations expose conjectural statements or abstraction bridges. A dependency-closed Lean 4 export compiles with zero sorry, but cited mathematical results and curve data remain Lean axioms. Compilation verifies the encoded implications, not the imported number theory. The principal contribution is formal packaging: a common typed interface, explicit dependency management, worked curve instances, reproducible exports, and a trust budget. No new number-theory theorem is claimed. The development does not prove BSD, does not resolve a Clay problem, and does not establish a generic unconditional result in rank at least two. The trust boundary is intentionally larger than in the previous draft. Besides the global BSD rank, formula, and Sha-finiteness assumptions, separate bridges cover low-rank Sha finiteness, GRH/CM Sha packages, rank-zero and rank-one formulas, a universal rank upper bound, Tian's family statement, a Selmer/analytic-rank equality, and a CM rank-one formula. Published p-adic and Iwasawa results have object types and hypotheses absent from this interface. The previous ordered-real "p-adic" phases have therefore been removed rather than marketed as formalizations. The load-bearing capstones are conditional compositions: the proposition ShaPFinite E plus A_selmer_eq_an_rank_bridge implies the rank identity; A_bsd_formula_rank0_bridge implies the rank-zero leading-term formula; and A_bsd_formula_rank1_bridge implies the rank-one leading-term formula. Per-curve conclusions are only as strong as their exported database, descent, and package assumptions. Phase 30 is only a definitional renaming of analytic rank and the leading coefficient; it has no independent spectral theorem or number-theoretic content. It is retained as an interface sketch and excluded from the novelty claim. The worked examples 32a2 and 37a1 illustrate the dependency graph. Their numerical and database inputs are hypotheses. The 37a1 leading-term capstone is explicitly conditional on A_bsd_formula_rank1_bridge; the CM rank-one package is likewise disclosed as an exported cited assumption rather than called unconditional. The scope is explicitly not a proof of BSD. The twelve explicit debt assumptions are listed in §1.3. In particular, A_sha_finite asserts ShaPFinite E for every curve E; it has proposition-valued semantics and is not a positivity claim about a real number. Th Maturity: Working Paper. Target venue: Experimental Mathematics. Part of The Latent research program. Related papers in this program: Universal.