Points with square $x - e_i$ are divisible by 2

Proved

BSD.mem_two_nsmul_of_isSquare

by korbonits · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

bsdelliptic-curvesnumber-theory

Let $F$ be a field with $2 \neq 0$ and let $E/F$ be an elliptic curve whose 2-torsion polynomial splits as $\psi_2(X) = 4(X - e_1)(X - e_2)(X - e_3)$ . If $P = (x, y) \in E(F)$ is an affine point such that $x - e_1$ , $x - e_2$ , $x - e_3$ are all squares in $F$ , then $P = 2Q$ for some $Q \in E(F)$ .

This is the kernel half of the 2-descent (Silverman X.1.4, or Knapp, Elliptic Curves, Thm 4.2). Explicitly, if $x - e_i = r_i^2$ , then with suitable sign choices $Q$ has $x(Q) = x + r_1r_2 + r_1r_3 + r_2r_3$ .

Preamble

import Mathlib

Formal statement

namespace BSD
open Polynomial in
theorem mem_two_nsmul_of_isSquare {F : Type*} [Field F] [DecidableEq F] (h2 : (2 : F) ≠ 0)
    (W : WeierstrassCurve F) [W.IsElliptic] (e₁ e₂ e₃ : F)
    (hψ : W.twoTorsionPolynomial.toPoly = C 4 * (X - C e₁) * (X - C e₂) * (X - C e₃))
    (x y : F) (h : W.toAffine.Nonsingular x y)
    (h₁ : IsSquare (x - e₁)) (h₂ : IsSquare (x - e₂)) (h₃ : IsSquare (x - e₃)) :
    ∃ Q : W.toAffine.Point, 2 • Q = .some x y h := by sorry
end BSD

Source

Silverman, The Arithmetic of Elliptic Curves (2nd ed.), Ch. X, Prop. 1.4 and Ch. VIII, Prop. 1.5–1.6 (proof of the weak Mordell–Weil theorem via the Kummer pairing, full 2-torsion case)

View graph

Points with square x−eix - e_ix−ei​ are divisible by 2

Points with square $x - e_i$ are divisible by 2