Root number one iff rank even
NOT A NOVELTY CLAIM. This is a machine-checked formalisation, decided by the Lean 4 kernel and depending on no axiom. It is dated and citable. Prior art, where it exists, is cited below. No discovery is claimed.
THE PARITY EQUIVALENCE. w = (−1)^rank says: w = 1 exactly when the rank is even. Checked for ranks 0..7, both directions.
Proposition
(∀ r ∈ [0, 2, 4, 6], sign r = 1) ∧ (∀ r ∈ [1, 3, 5, 7], sign r = -1)Proof
By decide in bsd.lean. The kernel reduces the proposition and reports no axiom dependency.
Sources and identifiers
- Lean source · src/pair/formal/proofs/bsd.lean
- Typeset paper · src/research/lean-theorems.tex
- Repository deposit · doi:10.5281/zenodo.21787144
- Author · ORCID 0009-0000-7312-9778
- Deposit record ·
bsd--root_number_one_iff_rank_even