Nagell–Lutz integrality #
Over ℤ, a nonzero torsion point of a Weierstrass curve has integral coordinates — unless it has
order exactly two, where the honest bound is that 4x and 8y are integral. Over the fraction
field K of a general unique factorisation domain R the same holds given squarefreeness of
the right factor: Squarefree (2 : R) when 4 divides the order, or squarefreeness of an odd
prime divisor of it. An arbitrary squarefree factor will not do — at order 6, Squarefree 2
supplies neither branch. That hypothesis is what the ℤ statement discharges for free, and it is
not removable in general. This file is the assembly: Torsion/Basic.lean proves the cases a
squarefree hypothesis makes accessible, Descent.lean pulls a conclusion back from a multiple of a
point to the point itself, and what remains is the case analysis that connects them.
The split is on the order m of the point, and m ≠ 1, m ≠ 2 put it in the range where
Mathlib's Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt applies: either 4 ∣ m, or m has
an odd prime factor p. In the first case (m / 4) • P is killed by 4 but not by 2 and the
order-four theorem applies; in the second (m / p) • P is nonzero and killed by p, so the
odd-index theorem does. Descent along m / 4 resp. m / p returns the conclusion at P. The
excluded case m = 2 need not be integral; there den_dvd_four_of_order_two bounds the
denominator of x instead, and ψ₂ vanishing bounds y.
Squarefreeness is a hypothesis rather than a typeclass, and it is guarded by m ≠ 2. The
order-two disjunct needs none of it, and an unguarded hypothesis would be unsatisfiable for
two-torsion points over any R in which 2 ramifies — Squarefree (2 : ℤ[i]) is false, since
2 = -i(1 + i)². Points of odd order over such an R are unaffected, since the hypothesis only
ever concerns primes dividing that point's own order; the guard is what keeps the order-two case
usable rather than what rescues the theorem. Over ℤ it costs nothing, which is why the
specialisation below carries no arithmetic hypothesis at all.
Main results #
WeierstrassCurve.isInteger_or_order_two_of_torsion: the statement over a UFDR. Its squarefreeness hypothesis is guarded byaddOrderOf P ≠ 2and asks only for the one branch the proof consumes, not for every prime factor.WeierstrassCurve.isInteger_or_order_two_of_torsion_of_squarefree: the same conclusion from a uniform hypothesis — squarefreeness at every prime factor of the order. That is strictly stronger, and therefore not weaker to prove; it is simply the form a caller usually already has, because it needs no knowledge of which branch the order falls into.WeierstrassCurve.isInteger_or_order_two_of_torsion_rat: theℤ/ℚspecialisation, assuming only that the point is torsion.WeierstrassCurve.isInteger_four_mul_x_and_eight_mul_y_of_order_two: the order-two bound on its own, from a Jacobian two-torsion hypothesis and needing no squarefreeness at all.
Roadmap #
New mathematics: TauCetiRoadmap/EllipticCurves/README.md:821 — "The torsion subgroup and
Nagell–Lutz", route "division polynomials" (:830–:831). Lines :823–:827 state this
theorem for an integral long Weierstrass model: over ℚ, "a nonzero torsion point has
x, y ∈ ℤ unless it has order exactly 2, where the honest bound is 4x, 8y ∈ ℤ". The
discriminant companion and the short-model form (:828–:830) are separate targets.
Provenance #
Ported from J. Xu and D. K. Angdinata's AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0,
main @ 1c1c74664e40071c2c2165bc55ca2616a67ccd6b), from two files of
projects/NagellLutz/LutzNagell/LutzNagellTheorem/, both byte-identical at 9fec8eba7652 — the
revision the roadmap pins for this project (README:1072) — verified by blob hash, so the
citations hold at either.
PIDMain.lean supplies the statement shape: nsmul_eq_zero_affine_to_jac (:48),
exists_some_of_ne_zero (:60), integrality_of_odd_prime_factor (:83),
integrality_of_four_dvd_order (:110) and lutz_nagell_integrality_pid (:145), which is
already stated over a general base in IsLocalization.IsInteger terms.
GeneralMain.lean supplies the order-two conclusion. Its lutz_nagell_integrality_general
(:112) ends in 4x, 8y integral, which is the form the roadmap asks for, where the PID
theorem ends in the weaker denominator bound den(x) ∣ 4. That file states the theorem over ℚ
only, so isInteger_or_order_two_of_torsion_rat is its statement and
isInteger_or_order_two_of_torsion generalises it.
Three adaptations. The base ring is a UFD rather than the source's principal ideal domain of
characteristic zero, matching Torsion/Basic.lean — no ideal is ever formed here, and CharZero is
unused. The squarefreeness hypothesis is guarded by addOrderOf P ≠ 2, which the source
leaves unguarded; see the note above on why an unguarded form is unsatisfiable over a ramifying
base — for two-torsion points, that is; a point of odd order never invokes Squarefree (2 : R).
And the arithmetic of the case split is not ported at all: both sources derive
4 ∣ m from "no odd prime factor" by hand, roughly a dozen lines each, but that is exactly
Mathlib's Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt, so the split is one rcases.
The order-two exception. A two-torsion point need not have integral coordinates, but
4x and 8y are always integral. No squarefreeness is needed: the bound is a denominator
estimate, not a factorisation argument.
Nagell–Lutz integrality. A nonzero torsion point either has integral coordinates, or has
order exactly two, in which case 4x and 8y are integral.
The squarefreeness hypothesis is guarded by addOrderOf P ≠ 2: the order-two disjunct is
proved by a denominator bound that needs no squarefreeness at all, and demanding it there would
make the order-two case unusable over any R in which 2 ramifies — ℤ[i] has 2 = -i(1+i)²,
so Squarefree (2 : ℤ[i]) is false and no two-torsion point could meet an unguarded hypothesis.
Odd-order points over the same R are unaffected. Over ℤ the guard costs nothing, since a
rational prime is squarefree there.
Nagell–Lutz integrality, in the form most callers want. Same conclusion as
isInteger_or_order_two_of_torsion, but asking for squarefreeness at every prime factor of the
order rather than at the one branch the proof consumes.
That hypothesis is strictly stronger — only one branch is ever used — so it is not a weaker thing
to prove. It is exported because it is usually the one a caller already has: establishing it needs
no knowledge of which branch the order falls into, whereas the sharp form does. Both are exported
for that reason, bridged by Algebra/Squarefree.lean's
Nat.four_dvd_or_exists_odd_prime_and_dvd_of_squarefree. The guard
addOrderOf P ≠ 2 is on both: the order-two disjunct is proved without squarefreeness, and
requiring it there would make the statement vacuous over a base in which 2 ramifies.
Nagell–Lutz over ℚ, the form the roadmap asks for: for an integral long Weierstrass
model, a nonzero torsion point has integral coordinates unless it has order exactly 2, where the
honest bound is 4x, 8y ∈ ℤ.
No squarefreeness hypothesis survives here. Over ℤ a rational prime is squarefree, so the
guard in the general statement discharges outright — which is why that statement carries the
hypothesis rather than a CharZero/unramified typeclass: the generality is free at ℤ and only
costs something over rings where a rational prime ramifies.