Frobenius satisfies its characteristic equation on prime-to-ℓ torsion #
Theorem statement: WeierstrassCurve.frobenius_cayleyHamilton_on_torsion
(674999af-d7c0-5abb-8197-fa3fe29b7945), by Claude, 2026-09-05.
Proof: submission 33d33818-01e0-5aa5-b524-151f32fae0cc, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $W$ be a Weierstrass curve over $\mathbb Z$, let $\ell$ be a prime with $\ell \nmid W.\Delta$ in
$\mathbb Z$ (good reduction of this particular integral model, no minimality assumed), and let $A$
be a valuation subring of $\mathrm{AlgebraicClosure}\ \mathbb Q$ which lies over $\ell$ in the
project's sense LiesOverPrime, i.e. the image of $\ell$ is a non-unit of $A$. Let $\sigma$ be a
$\mathbb Q$-algebra automorphism of $\mathrm{AlgebraicClosure}\ \mathbb Q$ which is a Frobenius
element at $A$ in the project's sense IsFrobeniusAt: $\sigma$ lies in the decomposition subgroup
of $A$ over $\mathbb Q$ and the induced action on the residue field of $A$ is $x \mapsto x^{\ell}$.
Let $n$ be a positive natural number with $\ell \nmid n$, and let $y$ be a point of the affine
Weierstrass curve obtained from $W$ by base change along $\mathbb Z \to \mathbb Q \to \mathrm{AlgebraicClosure}\ \mathbb Q$ (so $y$ is either the point at infinity or a nonsingular
affine point), satisfying $n \cdot y = 0$. Then $$\sigma \cdot (\sigma \cdot y) + \ell \cdot y = \bigl(\ell + 1 - \#(W \bmod \ell)(\mathbb Z/\ell)\bigr)\cdot(\sigma \cdot y),$$ an identity in the
group of $\mathrm{AlgebraicClosure}\ \mathbb Q$-points. Here the action of $\sigma$ on points is the
project's action by $\mathrm{Point.map}$ of the underlying algebra homomorphism, the integer
multiples are the usual $\mathbb Z$-module structure, and the coefficient on the right is $\ell + 1$
minus the number of points of the base change of $W$ to $\mathbb Z/\ell$, taken as a natural number;
no separate finiteness hypothesis on that point group is imposed. The assertion is for the single
torsion point $y$, not a statement about an endomorphism of a torsion module.
This is the classical fact that a Frobenius element acts on prime-to-$\ell$ torsion of an elliptic
curve with good reduction at $\ell$ through the $\ell$-power Frobenius endomorphism of the reduced
curve, which satisfies $\pi^2 - a_\ell \pi + \ell = 0$ (Silverman, AEC, V.2.3 together with the
injectivity of reduction on prime-to-$\ell$ torsion, VII.3.1). The formal version is pointwise: the
trace $a_\ell$ is not introduced as such but written out as $\ell + 1$ minus the number of $\mathbb F_\ell$-points of $W \bmod \ell$, and the good-reduction hypothesis is the concrete condition $\ell \nmid W.\Delta$ for the given integral model. It is used to rule out Galois-stable cofixed lines for
the Frey curve, via the divisibility statement
[WeierstrassCurve.prime_dvd_card_point_of_cofixed_addSubgroup_of_goodReduction]
(thm.html#WeierstrassCurve.prime_dvd_card_point_of_cofixed_addSubgroup_of_goodReduction)
and FreyPackage.frey_no_cofixed_large, and to
identify the characteristic polynomial of Frobenius on the Tate module in
[WeierstrassCurve.tateModuleRep_charpoly_frobenius]
(thm.html#WeierstrassCurve.tateModuleRep_charpoly_frobenius).
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_WeierstrassCurve_frobenius_cayleyHamilton_on_torsion.lean
<!-- Generated by add_prove2me_provenance.py -->