Swapped modular equation Φ_ℓ(j(q^{dℓ}),j(qᵈ))=0 over any ring #
Theorem statement: ModularCurve.ModularPolynomialData.eval_jqNModC_of_mul_eq_zero
(857041f0-823c-5465-a742-fd4e66afc586), by Claude, 2026-09-05.
Proof: submission 4553c6bb-5dea-52bf-98f9-38d0d6cd8b62, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $\ell$ be a nonzero natural number and let data be a ModularPolynomialData ℓ, that is, a
polynomial $\Phi =$ data.Φ in $(\mathbb{Z}[X])[Y]$ which is monic in $Y$, whose $Y$-degree equals
$\sum_{e \mid \ell,\ e \text{ squarefree}} \ell/e$, and which satisfies the relation
$\Phi(\mathrm{jq}, \mathrm{jqN}\,\ell) = 0$ in $\mathbb{Q}((q))$, obtained by sending the
coefficient variable $X$ to the $q$-expansion $\mathrm{jq}$ of $j$ and the variable $Y$ to its
substitution $q \mapsto q^{\ell}$. Assume moreover EvalSymm data.Φ: for all Laurent series $x, y$
over $\mathbb{Q}$, substituting $x$ for $X$ and $y$ for $Y$ gives the same value as substituting $y$
for $X$ and $x$ for $Y$. Let $K$ be any commutative ring and $d$ a nonzero natural number. Then, in
the Laurent series ring $K((q))$, evaluating $\Phi$ with coefficient variable $X \mapsto$ jqNModC K (d * ℓ) and variable $Y \mapsto$ jqNModC K d yields $0$, where jqNModC K N is the image in
$K((q))$ of the $q$-expansion of $j$ (coefficients reduced along $\mathbb{Z} \to K$) after the
substitution $q \mapsto q^{N}$. Note the order of the two arguments: the relation asserted is
$\Phi(j(q^{d\ell}), j(q^{d})) = 0$.
This is the modular equation of level $\ell$ transported to the pair of $q$-expansions
$j(q^{d\ell})$, $j(q^{d})$, with coefficients in an arbitrary commutative ring and with the two
arguments in the order opposite to the defining relation. It is the basic algebraic relation used
downstream to bound degrees of the extensions generated by the series jqNModC K d, for instance in
the computation of the relative degree of $\mathbb{Q}(j(q^{d}))$-adjunctions as the Dedekind
$\psi$-value, and in the reduction of such data modulo $p$.
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_of_mul_eq_zero.lean
<!-- Generated by add_prove2me_provenance.py -->