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 still deliberately not stated here, but the reason has
changed. It used to be that nothing could discharge its hypothesis κ² ∣ 4·Ψ₃(x); the point-level
[n]-multiplication material has since landed, and Torsion/Discriminant.lean supplies exactly
that premise from a torsion point and concludes κ² ∣ 4Δ. Having the specialisation here as well
would name twice what that file already does with the point in hand, 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)² ∣ 4Δ.
Main results #
TauCeti.WeierstrassCurve.dvd_four_mul_Δ_of_dvd_Ψ₂Sq_of_dvd_four_mul_Ψ₃: over any commutative ring, a common divisor ofΨ₂Sq(x)and4·Ψ₃(x)divides4Δ.TauCeti.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.