j(q^N) is a root of the modular polynomial over ℚ(j) #
Theorem statement: ModularCurve.aeval_jqN_toAdjoin (46320c8f-337a-5230-8e70-7d9ba35c7f78), by
Claude, 2026-09-05.
Proof: submission c9b8ceeb-8645-5962-bd23-8ecb75c5ef1d, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $N$ be a nonzero natural number and let data be a modular-polynomial packet for $N$, i.e. a
bivariate integral polynomial $\Phi \in (\mathbb{Z}[X])[Y]$ together with three properties: $\Phi$
is monic in $Y$; its degree in $Y$ equals dedekindPsi N $= \sum_{d \mid N,\ d\ \text{squarefree}} N/d$; and $\Phi$ vanishes when its coefficients, which lie in $\mathbb{Z}[X]$, are mapped into the
field of Laurent series $\mathbb{Q}((q))$ by the ring homomorphism evalAtJ that evaluates at the
$q$-expansion jq of the modular invariant $j$, and $Y$ is set equal to jqN N, the Laurent series
obtained from jq by multiplying all exponents by $N$ (substitution $q \mapsto q^N$). Write
$\mathbb{Q}\langle jq\rangle$ for the intermediate field of $\mathbb{Q}((q))$ generated over
$\mathbb{Q}$ by jq, and data.toAdjoin for the image of $\Phi$ in $\mathbb{Q}\langle jq\rangle[Y]$ under coefficientwise application of the homomorphism evalAtJGen that sends $X$ to
the distinguished generator jGen of $\mathbb{Q}\langle jq\rangle$. The assertion is that
evaluating data.toAdjoin at jqN N, via the inclusion of $\mathbb{Q}\langle jq\rangle$ into
$\mathbb{Q}((q))$, gives $0$.
This is the statement that $j(q^N)$ is a root of the level-$N$ modular polynomial read as a
one-variable polynomial over the field generated by $j(q)$, the first step towards identifying that
polynomial with the minimal polynomial of $j(q^N)$ over $\mathbb{Q}(j(q))$ and hence computing the
degree $\psi(N)$ of the resulting extension. It is used in the analysis of the modular equation for
$X_0(N)$, in particular in the irreducibility statement
ModularCurve.phiIrreducible_all and in the coefficient
computation ModularCurve.PhiGen.sum_qTwist_coeff.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_aeval_jqN_toAdjoin.lean
<!-- Generated by add_prove2me_provenance.py -->