Non-vanishing of the Weil numerator at n-torsion #
Theorem statement: WeierstrassCurve.Affine.weilNum_ne_zero
(855010c9-f5d4-5361-8cb5-5b47dac9e5d0), by Claude, 2026-09-05.
Proof: submission 76ce5626-9855-5234-9553-e87e40386b95, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $F$ and $K$ be fields with $K$ an $F$-algebra, $K$ algebraically closed, let $W$ be a
Weierstrass curve over $F$ which is elliptic, and assume the coordinate ring of the base change
$W⁄K$ is a Dedekind domain. Let $n$ be a natural number whose image in $K$ is nonzero, and let $T$
be a point of $(W⁄K)$ with $(n : \mathbb{Z}) \cdot T = 0$. Then the element weilNum W K n T of the
coordinate ring $(W⁄K)$.CoordinateRing is nonzero. Here weilNum W K n T is, by definition, a
chosen generator of the ideal fibIdeal W K n T in case that ideal is principal, and $1$ otherwise;
and fibIdeal W K n T is the product of the place ideals placeIdeal W K P over the points $P$ in
the fibre fibSet W K n T when that set is finite, and the unit ideal $\top$ otherwise. Thus the
assertion is that the distinguished generator attached to the fibre of multiplication by $n$ above
an $n$-torsion point $T$ is not the zero element.
This is the first step in the construction of the Weil pairing via divisors: the numerator $P_T$ whose divisor is the fibre $[n]^{-1}(T)$ must be a genuine nonzero function on the curve. It is used by the statements computing valuations and local expansions of the Weil function, and in the constructions producing the pairing from a basis of the $n$-torsion.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_WeierstrassCurve_Affine_weilNum_ne_zero.lean
<!-- Generated by add_prove2me_provenance.py -->