Translation pull-back carries vanishing at 2S to S #
Theorem statement: WeierstrassCurve.Affine.valuation_transEquiv_le_self
(28ee300d-dfb9-52a4-beec-9f36ce5f8929), by Claude, 2026-09-05.
Proof: submission c3dbe358-a49a-5f53-8946-e205bbae7af6, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $R$ be a field, $W$ a Weierstrass curve over $R$, and $K$ an algebraically closed field that is
an $R$-algebra, such that the base-changed curve $W⁄K$ is elliptic and its affine coordinate ring
$(W⁄K).\mathrm{CoordinateRing}$ is a Dedekind domain. Let $S$ be a point of the affine curve $W⁄K$
with $S \ne 0$ and $S + S \ne 0$, let $h$ be an element of the function field
$(W⁄K).\mathrm{FunctionField}$ (the fraction field of the coordinate ring), and let $k$ be a natural
number. For a nonzero point $P$, placeOf W K P hP denotes the height-one prime of the coordinate
ring whose ideal is the one generated by the classes of $X - x(P)$ and $Y - y(P)$, which is maximal
because the affine coordinates of $P$ give a nonsingular point, and nonzero because the class of $X
- x(P)$ is nonzero. Writing $v_P$ for the associated adic valuation with values in
$\mathbb{Z}^{m0}$, and $\exp$ for the embedding of $\mathbb{Z}$ into that group, the hypothesis is
$v_{S+S}(h) \le \exp(-k)$, i.e. $h$ vanishes to order at least $k$ at the place of $S+S$. The
conclusion is $v_S\big(\tau_S^{*}h\big) \le \exp(-k)$, where $\tau_S^{*} =$
transEquiv W K Sis the $K$-algebra automorphism of the function field given by the translation pull-back along $S$, with inverse the pull-back along $-S$.
This is the doubling case $P = S$ of the transport of adic valuations along the translation
pull-back: pulling back by translation by $S$ moves the order of vanishing at $2S$ to an order of
vanishing at least as large at $S$. It is used in the verification of the valuation-theoretic
properties of the functions entering the Weil pairing, being cited 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_self.lean
<!-- Generated by add_prove2me_provenance.py -->