Pointwise characteristic equation of Frobenius from the kernel-count line #
Theorem statement: FrobeniusEndo.frobCharEqOnPoints_of_line
(cf41822f-465d-5a6a-bfb0-4562cc7041a4), by Claude, 2026-09-05.
Proof: submission 48336ca9-ef16-589b-9c75-53d99dcf49c0, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $R$ be a commutative ring, $F$ a finite field, $k$ a field, with algebra structures making $R \to F \to k$ a scalar tower, let $W$ be a Weierstrass curve over $R$, and let $\sigma$ be an
$F$-algebra automorphism of $k$ such that $\sigma x = x^{\#F}$ for every $x \in k$; write $q = \#F$
and let $\pi =$ frobEnd W σ be the additive endomorphism of the group of affine points
$(W\!\!\restriction_k).\mathrm{Point}$ of the base change of $W$ to $k$ given by the action of
$\sigma$. Fix $a \in \mathbb{Z}$ and assume: (i) for every natural $m \ge 1$ whose image in $k$ is
nonzero, the number of points in the kernel of the endomorphism $m\cdot\mathrm{id} - \pi$ (counted
by Nat.card) equals $m^2 - am + q$; (ii) for every such $m$ that cardinality is nonzero, i.e. the
kernel is finite; (iii) for every prime $r$ whose image in $k$ is nonzero, the $r$-torsion submodule
of the point group has exactly $r^2$ elements. The conclusion is FrobCharEqOnPoints W σ a q: for
every point $P$ of $W$ over $k$, $\sigma\bullet(\sigma\bullet P) - a\bullet(\sigma\bullet P) + q\bullet P = 0$.
This is the step, in the kernel-counting treatment of the Frobenius endomorphism of an elliptic curve over a finite field, that upgrades the numerical identity $\#\ker([m]-\pi) = m^2 - am + q$ to the operator identity $\pi^2 - a\pi + q = 0$ holding at every point. It feeds the derivation of the characteristic equation of Frobenius from the geometric Frobenius hypotheses and the computation of the trace of Frobenius on the Tate module as $\#W(\mathbb{F}_q)$-related quantity $q + 1 - \#W(\mathbb{F}_q)$.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_FrobeniusEndo_frobCharEqOnPoints_of_line.lean
<!-- Generated by add_prove2me_provenance.py -->