Kernel-degree line #ker([m]-π)=m²-am+q #
Theorem statement: FrobeniusEndo.kerDeg_frobEnd_line_one (e575b5dc-c8e1-5a4a-90c9-fd4a42af88ad),
by Claude, 2026-09-05.
Proof: submission b07d107c-5f39-50ad-b44b-748de3f62fa8, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $R$ be a commutative ring, $F$ a finite field, and $k$ an algebraically closed field, equipped
with $R$-algebra structures on $F$ and $k$ and an $F$-algebra structure on $k$ forming a scalar
tower over $R$. Let $W$ be a Weierstrass curve over $R$ whose base change $W\!\;\!⁄k$ is elliptic,
and let $\sigma$ be an $F$-algebra automorphism of $k$ with $\sigma(x)=x^{q}$ for all $x\in k$,
where $q=\#F$; assume $q$ is prime. Let $m$ be a natural number with $m\ge 1$ whose image in $k$ is
nonzero. Write $\pi=$ frobEnd W σ for the additive endomorphism of the group of affine points of
$W\!\;\!⁄k$ (point at infinity included) induced by the action of $\sigma$. Then the cardinality of
the kernel of the endomorphism $m\cdot\mathrm{id}-\pi$ of that group, viewed as an integer, equals
$$m^{2}-\bigl(q+1-\#(W\!\;\!⁄F)(\text{points})\bigr)\,m+q,$$
where $\#(W\!\;\!⁄F)(\text{points})$ is Nat.card (W⁄F).Point, the number of points of the base
change of $W$ to $F$.
This is the kernel-degree identity underlying Manin's elementary proof of the Hasse bound: the function $m\mapsto\#\ker([m]-\pi)$ is given by the quadratic $m^{2}-am+q$ with $a=q+1-\#W(F)$ the trace of Frobenius. It feeds the computation of the trace of Frobenius on torsion, i.e. the statement that $\operatorname{tr}\bar\rho_{W,p}(\mathrm{Frob}_q)=q+1-\#W(F)$ at a prime of good reduction, and is cited by the determinant/trace computations for the mod $p$ representation and by the division-polynomial results on $a_p$.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_FrobeniusEndo_kerDeg_frobEnd_line_one.lean
<!-- Generated by add_prove2me_provenance.py -->