Modular equation Φ_ℓ(j(qᵈ),j(q^{dℓ}))=0 over any base ring #
Theorem statement: ModularCurve.ModularPolynomialData.eval_jqNModC_mul_eq_zero
(ab724e6a-4529-5d24-9a04-8ca86401ed38), by Claude, 2026-09-05.
Proof: submission 06a8b185-979e-5851-afda-578c5c1f8736, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $\ell \ge 1$ and let data be a modular-polynomial datum of level $\ell$, that is, a
two-variable integral polynomial $\Phi =$ data.Φ $\in (\mathbb{Z}[X])[Y]$ which is monic in $Y$,
whose degree in $Y$ equals $\psi(\ell) = \sum_{d \mid \ell,\ d \text{ squarefree}} \ell/d$, and
which satisfies $\Phi(j(q), j(q^{\ell})) = 0$ in the field of rational Laurent series
$\mathbb{Q}((q))$, the evaluation being: coefficients in $\mathbb{Z}[X]$ sent to $\mathbb{Q}((q))$
by $X \mapsto$ the $q$-expansion $j(q)$, and $Y \mapsto$ its image under the exponent-scaling ring
endomorphism $q \mapsto q^{\ell}$. Let $K$ be any commutative ring and $d \ge 1$. Write jqNModC K d for the Laurent series over $K$ obtained from $q^{-1}$ times the image in $K[[q]]$ of the
integral power series part of $j$ by multiplying all exponents by $d$, i.e. for the reduction to $K$
of the $q$-expansion of $j(q^{d})$. Then $\Phi$ evaluated with coefficients in $\mathbb{Z}[X]$
mapped to $K((q))$ by $X \mapsto$ jqNModC K d and with $Y \mapsto$ jqNModC K (d * ℓ) is $0$ in
$K((q))$.
This is the classical modular equation $\Phi_\ell(j(q^{d}), j(q^{d\ell})) = 0$, transported from its defining identity over $\mathbb{Q}$ to the Laurent series ring over an arbitrary commutative ring $K$ and to an arbitrary scaling $q \mapsto q^{d}$ of the variable. It is the basic algebraic relation used throughout the treatment of modular curves in characteristic $p$, for instance in computing the relative degree of $K(j(q^{d}))$-extensions generated by $j(q^{d\ell})$ and in the localisation arguments for the reduction of $X_0$.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_ModularPolynomialData_eval_jqNModC_mul_eq_zero.lean
<!-- Generated by add_prove2me_provenance.py -->