Vanishing of descended coefficients above degree ℓ+1 #
Theorem statement: ModularCurve.PhiGen.PhiGenDescends.c_eq_zero
(51d81ec6-fd61-5d61-b37b-89a26b0b5480), by Claude, 2026-09-05.
Proof: submission 3445e94f-4148-58e8-a035-05e3e123d6c1, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $K$ be a field equipped with a $\mathbb{Q}$-algebra structure, let $\ell$ be a prime, let
$\zeta$ be a unit of $K$, and let $c \colon \mathbb{N} \to \mathrm{LaurentSeries}\,\mathbb{Q}$ be a
family of rational Laurent series. Assume PhiGenDescends ℓ ζ c, that is: for every $k \in \mathbb{N}$, the coefficient of $X^k$ in the polynomial $\prod_{i \in \mathrm{Fin}(\ell+1)} \bigl(X
- \mathrm{C}(\mathtt{conj}\ \ell\ \zeta\ i)\bigr)$ over $\mathrm{LaurentSeries},K$ — where the
$i$-th root
conj ℓ ζ iis the coset substitution determined by $\zeta$ and the datacosetA ℓ i,cosetB ℓ iapplied to the image ofjqunder the coefficientwise mapcoeffEmb Kinduced by $\mathbb{Q} \to K$ — equalscoeffEmb K (qExpand ℚ ℓ (c k)), the image in $\mathrm{LaurentSeries}\,K$ of the $\ell$-fold $q$-expansion rescaling of $c\,k$ (the ring endomorphism of Laurent series multiplying all exponents by $\ell$). Then for every $k$ with $\ell + 1 < k$ one has $c\,k = 0$.
This records that a family of rational Laurent series descending the product of the $\ell+1$
conjugates is supported in degrees at most $\ell+1$, the product being a monic polynomial of degree
$\ell+1$; it is the degree bound used in the construction of the modular polynomial data, and it is
cited by
[ModularCurve.PhiGen.exists_modularPolynomialData_coeff_eq]
(thm.html#ModularCurve.PhiGen.exists_modularPolynomialData_coeff_eq).
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_PhiGen_PhiGenDescends_c_eq_zero.lean
<!-- Generated by add_prove2me_provenance.py -->