Nonvanishing of the Weil function g_T for T ∈ E[n] #
Theorem statement: WeierstrassCurve.Affine.weilFun_ne_zero
(999c93b5-5236-5294-9ada-65ba22f44d87), by Claude, 2026-09-05.
Proof: submission e65112f7-f540-5cfd-8a71-dd2eefdb600b, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $F$ and $K$ be fields with $K$ an $F$-algebra, $K$ algebraically closed, and let $W$ be a
Weierstrass curve over $F$ which is elliptic, such that the affine 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$ annihilated by $n$, i.e. $(n : \mathbb{Z}) \bullet T = 0$. The assertion
is that the element weilFun W K n T of the function field of $W⁄K$ is nonzero. By definition this
element is the quotient, in the function field, of the images of weilNum W K n T and weilNum W K n 0 under the map from the coordinate ring, where for an integer $m$ and a point $S$ the element
weilNum W K m S is a chosen generator of the ideal fibIdeal W K m S of the coordinate ring when
that ideal is principal, and $1$ otherwise. Thus the conclusion says that the numerator attached to
$T$ and the denominator attached to the zero point are both nonzero, so that their ratio is a
nonzero element of $K(E)$.
This is the first step in the construction of the Weil pairing on $n$-torsion: the function $g_T = P_T/P_O$ of Silverman's treatment is a well-defined nonzero element of the function field, so that
its divisor and its behaviour under translation and under field automorphisms can be analysed. It is
used by the statements comparing weilFun along algebra homomorphisms, under translation by torsion
points, and under isomorphisms of the underlying curve.
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_weilFun_ne_zero.lean
<!-- Generated by add_prove2me_provenance.py -->