Degree formula for the Frobenius pencil [m]-π #
Theorem statement: FrobeniusEndo.kerDeg_frobEnd_line_one_pos_and_eq
(b61d4902-cce5-5815-808f-f69879ba6811), by Claude, 2026-09-05.
Proof: submission ee2032d3-f4e7-5c3f-8097-7dfac7b5d355, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $R$ be a commutative ring, $F$ a finite field, and $k$ a field with decidable equality, equipped
with $R$- and $F$-algebra structures forming a scalar tower $R \to F \to k$, with $k$ algebraically
closed (these and the remaining typeclass assumptions are routine). 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$ such that $\sigma x = x^{\#F}$ for all $x \in k$; assume $q := \#F$ is prime. Write $\pi =$
frobEnd W σ for the additive endomorphism of the group of points $(W_{/k})$.Point induced by the
action of $\sigma$, and for integers $m,n$ let kerDeg π m n be the cardinality of the kernel of
the additive map $m \cdot \mathrm{id} - n \cdot \pi$. Then for every natural number $m \ge 1$ whose
image in $k$ is nonzero, the kernel of $[m] - \pi$ is finite and nonempty in the sense that kerDeg π m 1 $> 0$, and, as an identity of integers,
$$\#\ker([m]-\pi) = m^2 - \bigl(q + 1 - \#\ker([1]-\pi)\bigr)m + q.$$
This is the degree computation underlying Manin's elementary proof of Hasse's theorem: the pencil
$[m] - \pi$ has degree $m^2 - am + q$ with trace $a = q + 1 - \#\ker([1]-\pi)$, the latter kernel
being the group of $F$-rational points. It feeds the determination of the trace and determinant of
Frobenius on $p$-torsion, and is used by
FrobeniusEndo.kerDeg_frobEnd_line_one and
[FrobeniusEndo.kerDeg_frobEnd_line_one_ne_zero]
(thm.html#FrobeniusEndo.kerDeg_frobEnd_line_one_ne_zero).
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_pos_and_eq.lean
<!-- Generated by add_prove2me_provenance.py -->