Registry · Proposition III.P27 tau-effective formalized

III.P27 — BSD Three-Ingredient Proof

BSD coherence follows from rank stabilization, L-value stabilization, and E₁ Mutual Determination equality

Book III Part 6 Ch. 47

Dependency Graph

Depends on (1)

III.T35

Depended on by (1)

III.R25

Lean Formalization

Module: TauLib.BookIII.Arithmetic.BSD

Symbol: bsd_three_ingredient_check