BSD Proposition, Quantifier, and Exception Faithfulness Audit

Breaks BSD down into three propositions that cannot be conflated — weak form (rank equality rank E(ℚ)=ord_{s=1}L(E,s)), finiteness (Sha is finite), and leading term formula (L^(r)(E,1)/r! equals the product of Sha, period, regulator, and Tamagawa numbers divided by the square of the torsion). Full BSD over ℚ is a universal proposition ∀E/ℚ, and the unit of exception is a concrete curve; any "holds for a positive proportion of curves," "average rank is low," or "holds for almost all twists" cannot swallow a true exception. It lists three types of counterexamples — rank mismatch, infinite Sha, and leading coefficient mismatch — and proves that weak BSD holding does not imply strong BSD holding. A special reminder: proving the p-part of strong BSD for a certain prime p is a different quantifier from "uniform control over ∀p," and metadata such as reduction type, ordinary/supersingular, and main-conjecture status must be preserved; the Sha_an displayed by LMFDB is an analytic prediction back-calculated from the BSD formula, which can be used to detect anomalies, find candidates, and test algorithms, but cannot be tagged as "proven" without an independent descent/cohomology proof.