Assembling Φ_ℓ from a descended integral coefficient family #
Theorem statement: ModularCurve.PhiGen.exists_modularPolynomialData_coeff_eq
(6879c911-b7bb-5d11-ba98-24b49f32a07a), by Claude, 2026-09-05.
Proof: submission a8132dcd-9397-5ba5-8dd6-ba0f06263369, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $K$ be a field containing $\mathbb{Q}$ as a subalgebra, 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}$. Three hypotheses are imposed. First, PhiGenDescends ℓ ζ c: for every $k$, the
degree-$k$ coefficient of the monic polynomial $\prod_{i \in \mathrm{Fin}(\ell+1)} (X - C(\mathrm{conj}\ \ell\ \zeta\ i))$ over $K((q))$, whose roots are the conjugate series conj ℓ ζ i
built from $\zeta$ and the coset data cosetA ℓ i, cosetB ℓ i applied to the image of the
$j$-series jq in $K((q))$, equals the image under the coefficientwise map induced by $\mathbb{Q} \to K$ of qExpand ℚ ℓ (c k), the series $c_k$ with all exponents multiplied by $\ell$. Second,
each $c_k$ has all its Laurent coefficients in $\mathbb{Z}$. Third, each $c_k$ lies in the
$\mathbb{Q}$-subalgebra of $\mathbb{Q}((q))$ generated by jq. The conclusion asserts the existence
of a ModularPolynomialData ℓ, that is a polynomial $\Phi \in (\mathbb{Z}[X])[Y]$ which is monic,
has $Y$-degree equal to $\psi(\ell) = \sum_{d \mid \ell,\ d\ \text{squarefree}} \ell/d$ (equal to
$\ell+1$ for $\ell$ prime), and satisfies $\Phi = 0$ after substituting $X \mapsto$ jq
coefficientwise and $Y \mapsto$ jqN ℓ, together with the property that for every $k$ the
$Y^k$-coefficient of $\Phi$, evaluated at $X =$ jq, is exactly $c_k$.
This is the assembly step producing the classical modular polynomial $\Phi_\ell(X,Y)$ for
$X_0(\ell)$: the coefficients of the product over the $\ell+1$ conjugates, once known to descend to
$q$-expansions with integral coefficients lying in $\mathbb{Q}[j]$, are recognised as integral
polynomials in $j$, and the resulting packet is monic of degree $\psi(\ell)$ in $Y$ and vanishes at
$(j(q),$ jqN ℓ $)$. It is used downstream for the splitting statement
ModularCurve.PhiGen.splits_of_prime, for the
weighted support bound
[ModularCurve.ModularPolynomialData.weighted_support_le]
(thm.html#ModularCurve.ModularPolynomialData.weighted_support_le),
and in
[ModularCurve.exists_modularPolynomialData_evalSymm]
(thm.html#ModularCurve.exists_modularPolynomialData_evalSymm).
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_exists_modularPolynomialData_coeff_eq.lean
<!-- Generated by add_prove2me_provenance.py -->