Formal descent data give q-expansions of the Hecke coset polynomial #
Theorem statement: ModularCurve.PhiGen.PhiGenDescends.hasSum_cosetPoly_coeff
(d4b12e57-059a-5aba-9259-be91e6f4b8ab), by Claude, 2026-09-05.
Proof: submission 6906357b-f645-5e50-a6ef-62a6b647d1a1, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Fix a natural number $\ell$ assumed prime, a unit $\zeta$ of CyclotomicField ℓ ℚ together with a
proof hζ that $\zeta$ is a primitive $\ell$-th root of unity, and a family $c : \mathbb{N} \to$
LaurentSeries ℚ of rational Laurent series. Assume ModularCurve.PhiGen.PhiGenDescends ℓ ζ c, i.e. for every $k$ the $k$-th coefficient of the polynomial
$\prod_{i : \mathrm{Fin}(\ell+1)} (X - C(\mathrm{conj}\,\ell\,\zeta\,i))$ over Laurent series with
coefficients in the cyclotomic field equals the image under coeffEmb of qExpand ℚ ℓ (c k), the
series obtained from $c_k$ by multiplying all exponents by $\ell$; here
$\mathrm{conj}\,\ell\,\zeta\,i$ is cosetSubst ζ (cosetA ℓ i) (cosetB ℓ i) applied to the
coefficientwise image of the Laurent series ModularCurve.jq, the
formal stand-ins for the $\ell+1$ Hecke conjugates of $j$. Then for every $k : \mathbb{N}$ and every
$\tau$ in the upper half-plane, the family indexed by $m \in \mathbb{Z}$ whose $m$-th term is the
rational number $\mathrm{coeff}_m(c_k)$, viewed in $\mathbb{C}$, times $q^m$ with $q =$
Function.Periodic.qParam 1 τ $= e^{2\pi i \tau}$, is summable with sum the $k$-th coefficient of
the polynomial
$$\bigl(X - C\,\tilde j(\beta_\infty \tau)\bigr)\prod_{b : \mathrm{Fin}\,\ell}\bigl(X - C\,\tilde j(\beta_b \tau)\bigr) \in \mathbb{C}[X],$$
where $\tilde j = E_4^3/\Delta$ in the normalisation ModularForm.E₄ and
ModularForm.discriminant, $\beta_\infty =$ heckeDiagMatrix ℓ $= \begin{pmatrix}\ell&0\\0&1\end{pmatrix}$ and $\beta_b =$ heckeMatrix ℓ b $= \begin{pmatrix}1&b\\0&\ell\end{pmatrix}$ act on the upper half-plane through
$\mathrm{GL}_2(\mathbb{R})$.
This is the analytic–formal bridge for the modular polynomial of level $\ell$: it identifies a
formal solution of the descent equations for the Hecke coset product with the $q$-expansion,
convergent on the upper half-plane, of the corresponding elementary symmetric function of the values
$\tilde j(\beta_i\tau)$. It is used by
[ModularCurve.PhiGen.mem_adjoin_jq_of_phiGenDescends]
(thm.html#ModularCurve.PhiGen.mem_adjoin_jq_of_phiGenDescends)
to place these symmetric functions in the algebra generated by $j$.
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_hasSum_cosetPoly_coeff.lean
<!-- Generated by add_prove2me_provenance.py -->