Root number squares to one

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 root number is an involution's eigenvalue: w ∈ {1, −1} and w² = 1.

Proposition

(1 : Int) * 1 = 1 ∧ (-1 : Int) * (-1) = 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_squares_to_one

Proved in the same file

• Sigma is an involution
• Central point is the fixed point
• Root number one iff rank even
• Parity is an involution

All machine-checked theorems