A common divisor of Ψ₂Sq(x) and 4·Ψ₃(x) divides 4Δ #
The headline is a divisibility transfer between Mathlib's division polynomials: for any
commutative ring, any x, and any d,
d ∣ Ψ₂Sq(x) and d ∣ 4·Ψ₃(x) together give d ∣ 4Δ.
Equivalently, 4Δ lies in the ideal generated by Ψ₂Sq(x) and 4·Ψ₃(x) at every x, and the
proof is an explicit Bézout certificate in the b-invariants. Its two divisibility premises are of
course assumptions; what it needs beyond them is nothing — no point of a curve, no ellipticity,
no domain or factorisation hypothesis on the ring.
The Nagell–Lutz route needs the on-curve form — with κ = ψ₂(x, y) = 2y + a₁x + a₃ Mathlib's
2-division polynomial at a point, take d = κ², which on the curve is Ψ₂Sq(x) by
evalEval_ψ₂_sq. That specialisation is deliberately not stated here: discharging its
hypothesis κ² ∣ 4·Ψ₃(x) takes a torsion point, and Torsion/Discriminant.lean uses one to prove
the nonzero branch of the disjunction κ = 0 ∨ κ² ∣ 4Δ. Stating the specialisation here as well
would name the same result twice, so this module keeps to the polynomial statement and lets its
consumer instantiate it. For a short model (a₁ = a₃ = 0, so
κ = 2y) the consumer's conclusion reads 2y = 0 ∨ (2y)² ∣ 4Δ.
Main results #
WeierstrassCurve.dvd_four_mul_Δ_of_dvd_Ψ₂Sq_of_dvd_four_mul_Ψ₃: over any commutative ring, a common divisor ofΨ₂Sq(x)and4·Ψ₃(x)divides4Δ.WeierstrassCurve.evalEval_ψ₂_sq: on the curve,ψ₂(x, y)² = Ψ₂Sq(x).
Stated over an arbitrary commutative ring: no domain, integrality or ellipticity hypothesis.
⚠ No torsion hypothesis appears here, and no part of lutz_nagell is proved. The headline is a
statement about polynomials, usable by any caller with a common divisor in hand, and
evalEval_ψ₂_sq is an unconditional on-curve evaluation. The torsion input that turns them into
the Nagell–Lutz disjunct lives in Torsion/Discriminant.lean.
This is an ingredient for the Nagell–Lutz milestone of TauCetiRoadmap/EllipticCurves/README.md,
Layer 6, item "The torsion subgroup and Nagell–Lutz", whose short-model target lutz_nagell asks
for x, y ∈ ℤ together with y = 0 ∨ y² ∣ Δ. It is the algebraic step feeding the second
disjunct of that disjunction, in the long-model form the roadmap also names
(lutz_nagell_integrality_general, "with its discriminant companion"). Establishing the full
disjunction additionally requires the torsion input above and a separate treatment of the y = 0
branch.
Provenance #
Ported from the AINTLIB NagellLutz project (github.com/CBirkbeck/AINTLIB, Apache-2.0), pinned by
that roadmap at dev/modular-curves @ 9fec8eba7652:
LutzNagell/LutzNagellTheorem/PIDMain.lean, declarations kappa_sq_eq_Psi2Sq, bezout_identity,
kappa_sq_dvd_four_delta, eval_Ψ₃ and lutz_nagell_pid_discriminant. Restated here against
Mathlib's ψ₂, Ψ₂Sq and Ψ₃ rather than the raw expressions the source carries, so no
eval_Ψ₃ bridge lemma is needed; the source's [IsDomain], [IsPrincipalIdealRing] and
[CharZero] hypotheses were already omitted there and are absent here too.
On the curve, the square of ψ₂ at a point is the univariate Ψ₂Sq at its x-coordinate.
This is Mathlib's polynomial identity ψ₂_sq — ψ₂² = C Ψ₂Sq + 4 * polynomial — evaluated at a
point where the Weierstrass polynomial vanishes.
A common divisor of Ψ₂Sq(x) and 4·Ψ₃(x) divides 4Δ.
This is the whole arithmetic content of the file. Beyond the two divisibility premises it assumes
nothing: it holds for every commutative ring, every x and every d, and no point of a curve
occurs in it. 4Δ lies in the ideal generated by Ψ₂Sq(x) and 4·Ψ₃(x) at any x, exhibited by
an explicit Bézout combination in the b-invariants.