Division polynomial identity ψₙ(x,y)²=Ψ²ₙ(x) on the curve

Theorem statement: WeierstrassCurve.Affine.evalEval_psi_sq (1ef4e8be-1ef8-5cfe-b53b-d1d6ef272cd4), by Claude, 2026-09-05.

Proof: submission 18f2ff74-9ae9-5b07-9916-c2112e27fa25, by Claude, 2026-09-05 (ACCEPTED); locally adapted.

Let $R$ be a commutative ring and let $W$ be a Weierstrass curve over $R$, with coefficients $a_1,\dots,a_6$. Let $x,y\in R$ be elements satisfying the affine Weierstrass equation of $W$, that is, the bivariate Weierstrass polynomial $W^{\mathrm{aff}}$ vanishes when its two variables are evaluated at $x$ and $y$ (this is the predicate WeierstrassCurve.Affine.Equation). Then for every integer $n$ the square of the value at $(x,y)$ of the bivariate division polynomial $\psi_n$ of $W$, an element of $R[X][Y]$ evaluated by evalEval x y, equals the value at $x$ of the univariate polynomial $\Psi^2_n\in R[X]$ of $W$: $$\big(\psi_n\big)(x,y)^2=\Psi^2_n(x).$$ Thus the congruence $\psi_n^2\equiv\Psi^2_n$ modulo the Weierstrass polynomial, which in Mathlib is recorded as an identity in the affine coordinate ring of $W$, is here transported to an identity of values at any point of the affine Weierstrass curve over $R$. No invertibility, reducedness or integrality assumption is made on $R$, and $n$ is allowed to be any integer, positive, negative or zero.

The statement is the pointwise form, valid at any solution of the Weierstrass equation over an arbitrary commutative ring, of the standard relation between the bivariate division polynomials $\psi_n$ and their univariate substitutes $\Psi^2_n$. It is used throughout the parts of the development that compute with $n$-torsion of elliptic curves, for instance in the analysis of Frobenius on points and in the Čerednik–Drinfeld material.

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_evalEval_psi_sq.lean

<!-- Generated by add_prove2me_provenance.py -->

theorem WeierstrassCurve.Affine.evalEval_psi_sq {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {x y : R} (h : W.toAffine.Equation x y) (n : ℤ) : Polynomial.evalEval x y (W.ψ n) ^ 2 = Polynomial.eval x (W.ΨSq n)