Pole order at most ℓ+1 for descended coefficients #
Theorem statement: ModularCurve.PhiGen.PhiGenDescends.poleOrderLE
(78c5f2e1-bde3-532a-9293-958c72dc0121), by Claude, 2026-09-05.
Proof: submission 1742ce90-b7aa-54a0-941e-667b9883825d, 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 : \mathbb{N} \to \mathbb{Q}((q))$ be a family of Laurent series
over $\mathbb{Q}$. Assume PhiGenDescends ℓ ζ c, that is: for every $k \in \mathbb{N}$, the
coefficient of $X^k$ in the monic polynomial $\prod_{i \in \mathrm{Fin}(\ell+1)} (X - \mathrm{conj}\,\ell\,\zeta\,i)$ over $K((q))$, whose roots are the $\ell+1$ conjugate Laurent series
conj ℓ ζ i produced by the coset substitution cosetSubst applied to the coefficientwise image of
the series jq in $K((q))$, coincides with
$\mathrm{coeffEmb}_K(\mathrm{qExpand}_{\mathbb{Q},\ell}(c_k))$; here
$\mathrm{qExpand}_{\mathbb{Q},\ell}$ is the ring homomorphism of $\mathbb{Q}((q))$ multiplying all
exponents by $\ell$, and $\mathrm{coeffEmb}_K$ applies $\mathbb{Q} \to K$ to each coefficient. Then
for every $k \in \mathbb{N}$ one has PoleOrderLE (c k) (ℓ + 1), i.e. the coefficient of $q^{m}$ in
$c_k$ vanishes for every integer $m < -(\ell+1)$: each $c_k$ has a pole of order at most $\ell+1$ at
$q = 0$.
This is the pole bound for the coefficient family descending the product over the $\ell+1$
conjugates, the series whose coefficients give the modular equation of level $\ell$; the bound
$\ell+1$ results from the bound $\ell^2+\ell$ on the product's coefficients together with the
substitution multiplying exponents by $\ell$. It feeds the support bound
[ModularCurve.ModularPolynomialData.weighted_support_le]
(thm.html#ModularCurve.ModularPolynomialData.weighted_support_le)
and the construction of modular polynomial data in
[ModularCurve.PhiGen.exists_modularPolynomialData_coeff_eq]
(thm.html#ModularCurve.PhiGen.exists_modularPolynomialData_coeff_eq),
as well as
[ModularCurve.PhiGen.evalSymm_of_coeff_evalAtJ_eq]
(thm.html#ModularCurve.PhiGen.evalSymm_of_coeff_evalAtJ_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_poleOrderLE.lean
<!-- Generated by add_prove2me_provenance.py -->