The congruent number curves are quadratic twists of y² = x³ − x

Lax712553.QuadraticTwist · concepts/Lax712553/QuadraticTwist.lean · lax-712553

proven

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    The congruent number curve of nn is En:y2=x3n2xE_n : y^2 = x^3 - n^2 x. For a prime pp, the trace of Frobenius ap(En)=p+1#En(Fp)a_p(E_n) = p + 1 - \#E_n(\mathbb{F}_p) is the character sum xFpχ(x3n2x)-\sum_{x \in \mathbb{F}_p} \chi(x^3 - n^2 x), where χ\chi is the quadratic character of Fp\mathbb{F}_p with χ(0)=0\chi(0) = 0: each xx contributes 1+χ(f(x))1 + \chi(f(x)) points. This concept defines apa_p by that sum.

    The statement is the quadratic twist formula: for every prime pp and every integer nn not divisible by pp,

    ap(En)=χ(n)ap(E1),a_p(E_n) = \chi(n)\, a_p(E_1),

    so every EnE_n is the quadratic twist of E1:y2=x3xE_1 : y^2 = x^3 - x by nn. The identity is exact at the level of character sums; it is the substitution x=ntx = n t, a bijection of Fp\mathbb{F}_p because nn is invertible, together with χ(n3)=χ(n)\chi(n^3) = \chi(n).

    Concept map
    1 concept
    100%
    Proven claimThis concept
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
    2
    3/-!
    4---
    5title: The congruent number curves are quadratic twists of y² = x³ − x
    6type: theorem
    7---
    8The congruent number curve of nn is En:y2=x3n2xE_n : y^2 = x^3 - n^2 x. For a prime pp,
    9the trace of Frobenius ap(En)=p+1#En(Fp)a_p(E_n) = p + 1 - \#E_n(\mathbb{F}_p) is the character
    10sum xFpχ(x3n2x)-\sum_{x \in \mathbb{F}_p} \chi(x^3 - n^2 x), where χ\chi is the quadratic
    11character of Fp\mathbb{F}_p with χ(0)=0\chi(0) = 0: each xx contributes 1+χ(f(x))1 + \chi(f(x))
    12points. This concept defines apa_p by that sum.
    13
    14The statement is the quadratic twist formula: for every prime pp and every
    15integer nn not divisible by pp,
    16
    17ap(En)=χ(n)ap(E1),a_p(E_n) = \chi(n)\, a_p(E_1),
    18
    19so every EnE_n is the quadratic twist of E1:y2=x3xE_1 : y^2 = x^3 - x by nn. The
    20identity is exact at the level of character sums; it is the substitution
    21x=ntx = n t, a bijection of Fp\mathbb{F}_p because nn is invertible, together with
    22χ(n3)=χ(n)\chi(n^3) = \chi(n).
    23-/
    24
    25namespace Lax712553.QuadraticTwist
    26
    27/-- The trace of Frobenius of `E_n : y² = x³ − n² x` at the prime `p`, as the
    28character sum `−∑_x χ(x³ − n² x)`. -/
    29noncomputable def a_p (n : ℤ) (p : ℕ) [Fact p.Prime] : ℤ :=
    30 -∑ x : ZMod p, quadraticChar (ZMod p) (x ^ 3 - (n : ZMod p) ^ 2 * x)
    31
    32/-- The quadratic twist formula `a_p(E_n) = χ(n) a_p(E_1)` for `p ∤ n`. -/
    33axiom a_p_twist (n : ℤ) (p : ℕ) [Fact p.Prime] (hn : (n : ZMod p) ≠ 0) :
    34 a_p n p = quadraticChar (ZMod p) (n : ZMod p) * a_p 1 p
    35
    36end Lax712553.QuadraticTwist
    37
    Show Proof
    Builds on

    none

    Used by

    none

    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…