Coefficients of the generic level-ℓ modular polynomial lie in ℚ[j] #
Theorem statement: ModularCurve.PhiGen.mem_adjoin_jq_of_phiGenDescends
(a4ed865b-516c-5b55-8d36-8079c307dc26), by Claude, 2026-09-05.
Proof: submission 1ee80e3a-fc52-5318-8dcc-0ec47b387159, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $\ell$ be a prime, let $\zeta$ be a unit of the cyclotomic field CyclotomicField ℓ ℚ whose
underlying element is a primitive $\ell$-th root of unity, and let $c : \mathbb{N} \to$
LaurentSeries ℚ be a family of rational Laurent series. Assume PhiGenDescends ℓ ζ c: for every
$k$, the $k$-th coefficient of the monic polynomial $\prod_{i : \mathrm{Fin}(\ell+1)} (X - C(\mathrm{conj}\ \ell\ \zeta\ i))$ over the Laurent series of the cyclotomic field, whose roots are
the formal conjugates conj ℓ ζ i obtained by applying the substitution cosetSubst ζ (cosetA ℓ i) (cosetB ℓ i) to the coefficientwise image coeffEmb of the formal $q$-expansion jq, equals the
coefficientwise image under coeffEmb of qExpand ℚ ℓ (c k), the series $c_k$ with its exponents
multiplied by $\ell$. Then, for every natural number $k$, the series $c_k$ lies in Algebra.adjoin ℚ {jq}, the $\mathbb{Q}$-subalgebra of LaurentSeries ℚ generated by jq $= q^{-1}\cdot$ofPowerSeries jNumQ. Thus each solution of the descent equations is a polynomial in
$j$ with rational coefficients.
This is the analytic leg of the construction of the modular polynomial $\Phi_\ell$: it identifies the coefficients of $\prod_i (X - j\circ\beta_i)$, taken over the $\ell+1$ Hecke cosets of level $\ell$, as elements of $\mathbb{Q}[j]$, so that $\Phi_\ell(X,Y) \in \mathbb{Q}[X,Y]$ with $\Phi_\ell(X,j) = \prod_i (X - j\circ\beta_i)$. It is used in the construction of the modular polynomial data for $X_0(\ell)$ and in the statements about splitting and about the weighted support of that data; integrality, symmetry and the degree bounds are established separately.
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_mem_adjoin_jq_of_phiGenDescends.lean
<!-- Generated by add_prove2me_provenance.py -->