Translation pull-back does not decrease order of vanishing #
Theorem statement: WeierstrassCurve.Affine.valuation_transEquiv_le
(ad31d186-5c24-5816-927f-6dcd74404a24), by Claude, 2026-09-05.
Proof: submission e783caec-da40-5dbd-9034-6f16cd704ad1, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $R$ be a field, $W$ a Weierstrass curve over $R$, and $K$ a field which is an $R$-algebra,
assumed algebraically closed, with $W$ elliptic and the coordinate ring of the affine base change
$W⁄K$ a Dedekind domain. Let $P$ and $S$ be points of $(W⁄K)$, both different from the point at
infinity, with $P.\mathrm{xc} \neq S.\mathrm{xc}$ (distinct $x$-coordinates, so $P \neq \pm S$) and
$P + S \neq 0$. For a point $Q \neq 0$, placeOf W K Q denotes the height-one prime of the
coordinate ring of $W⁄K$ cut out by the ideal CoordinateRing.XYIdeal at $(Q.\mathrm{xc}, Q.\mathrm{yc})$, which is maximal, hence prime, and nonzero. Let $h$ be an element of the function
field of $W⁄K$ and $k$ a natural number. The assertion is: if the adic valuation of $h$ at placeOf W K (P + S) hPS is at most $\exp(-k)$ in $\mathbb{Z}_{m0}$, then the adic valuation of
$(\mathrm{transEquiv}\ W\ K\ S)\,h$ at placeOf W K P hP is at most $\exp(-k)$; here transEquiv W K S is the $K$-algebra automorphism of the function field built from transPull W K S with inverse
transPull W K (-S), the pull-back along translation by $S$. Equivalently, $\operatorname{ord}_P(h \circ \tau_S) \geq \operatorname{ord}_{P+S}(h)$.
This records how orders of vanishing transform under the pull-back by translation on the function
field of an elliptic curve: a function vanishing to order at least $k$ at $P+S$ pulls back to one
vanishing to order at least $k$ at $P$ (equality in fact holds, the translation being an
automorphism, but only the inequality is asserted). It is used in the construction and verification
of the properties of the Weil pairing, in particular by
[WeierstrassCurve.Affine.valuation_transEquiv_weilFun]
(thm.html#WeierstrassCurve.Affine.valuation_transEquiv_weilFun).
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_valuation_transEquiv_le.lean
<!-- Generated by add_prove2me_provenance.py -->