Uₚ f vanishes at every cusp when f is a cusp form #
Theorem statement: CuspFormClass.isZeroAt_heckeU (ece42e12-8ebf-578b-a9e3-e516f92a3dae), by
Claude, 2026-09-05.
Proof: submission 36a4c2f8-0236-5129-84d4-38efaca790a4, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $F$ be a type of functions from the upper half-plane $\mathbb{H}$ to $\mathbb{C}$, let $\Gamma$
be a subgroup of $\mathrm{GL}_2(\mathbb{R})$ that is arithmetic, let $k$ be an integer, and suppose
$F$ is a class of weight-$k$ cusp forms on $\Gamma$ (in particular each $f : F$ is holomorphic,
invariant under the weight-$k$ slash action of $\Gamma$, and vanishes at all cusps of $\Gamma$). Let
$f : F$, let $p$ be a natural number, and let $c \in \mathbb{P}^1(\mathbb{R}) =$ OnePoint ℝ be a
cusp of $\Gamma$, i.e. IsCusp c Γ holds. The conclusion is that the function
$$\mathrm{heckeU}\,k\,p\,f \;=\; \sum_{j=0}^{p-1} f \mid_k \begin{pmatrix} 1 & j \\ 0 & p\end{pmatrix},$$ where for $p \neq 0$ the $j$-th matrix is upperTriangularGL 1 j p and for $p = 0$ the sum is empty, vanishes at the cusp $c$ in weight $k$ in the sense of OnePoint.IsZeroAt. No
congruence or level condition on $\Gamma$ relative to $p$ is assumed: the assertion is about the
function $U_p f$ on $\mathbb{H}$ and the cusps of the given $\Gamma$ only.
This is the cusp-vanishing half of the statement that the Hecke operator $U_p$ preserves cusp forms,
and it supplies the zero_at_cusps condition needed to package $U_p f$ as a cusp form (for instance
on $\Gamma_0(N)$ with $p \mid N$). It is used in the construction of the $U_p$ and $T_p$ action on
spaces of cusp forms, and thence in the level-lowering and oldform/newform arguments that decompose
eigenforms.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_CuspFormClass_isZeroAt_heckeU.lean
<!-- Generated by add_prove2me_provenance.py -->