Finiteness of ker([m]-π) on W(k) #
Theorem statement: FrobeniusEndo.kerDeg_frobEnd_line_one_ne_zero
(ebfaccc3-8d45-57a7-9bc9-c94126b990f6), by Claude, 2026-09-05.
Proof: submission 65f715f6-f7be-5d44-a8ed-01e0a4709675, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $R$ be a commutative ring, $F$ a finite field, and $k$ an algebraically closed field with
decidable equality, equipped with $R$-algebra structures on $F$ and on $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$ to $k$ is elliptic, and let $\sigma : k \simeq_{\mathrm{alg}[F]} k$ be an $F$-algebra
automorphism of $k$ satisfying $\sigma(x) = x^{\#F}$ for every $x \in k$; assume $\#F$ is prime. Let
$m$ be a natural number with $1 \le m$ whose image in $k$ is nonzero. Writing $\pi =$ frobEnd W σ
for the additive endomorphism of the group of affine points $(W⁄k).\mathrm{Point}$ induced by the
action of $\sigma$, the conclusion is that kerDeg (frobEnd W σ) m 1 is nonzero, where kerDeg ψ m n denotes Nat.card of the kernel of the pencil $m \cdot \mathrm{id} - n \cdot \psi$; thus the
cardinality of the kernel of $[m] - \pi$ on $(W⁄k).\mathrm{Point}$ is nonzero, i.e. (this kernel
being nonempty) that kernel is finite.
The assertion is the finiteness half of the standard count of $\ker([m] - \pi)$ for the $\#F$-power Frobenius $\pi$ on an elliptic curve over an algebraically closed field, the statement that $[m] - \pi$ is a nonzero separable isogeny in Manin's route to the Hasse bound. It serves as the positivity input for the passage between divisibility of $\#\ker([m]-\pi)$ by the residue characteristic and vanishing of $\det(\bar m - \bar\rho(\pi))$, and is used in the computation of the characteristic polynomial of Frobenius on points, in the determinant–trace identification for Galois representations over algebraically closed fields, and in the analysis of coefficients of division polynomials.
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_ne_zero.lean
<!-- Generated by add_prove2me_provenance.py -->