Descent by one prime: j(q^M)∈ℚ(j(q),j(q^{Mp})) #
Theorem statement: ModularCurve.jqN_div_mem_modularFunctionField
(8b07b3a0-f74d-51dc-9e2a-5e932595baa8), by Claude, 2026-09-05.
Proof: submission dd49da64-404d-591b-af04-5d07d01fde9b, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Fix a nonzero natural number $M$ and a prime $p$, and let $K$ be a field equipped with a
$\mathbb{Q}$-algebra structure together with a unit $\zeta\in K^\times$ whose underlying element is
a primitive $(Mp)$-th root of unity. Write $\mathrm{jq}\in\mathbb{Q}((q))$ for the Laurent series
$q^{-1}$ times the rational $j$-numerator power series, and for $N\neq 0$ let $\mathrm{jqN}\,N$ be
its image under the substitution $q\mapsto q^{N}$ (the ring endomorphism qExpand of Laurent series
raising exponents by the factor $N$). Let $P$ be the polynomial over $K((q))$ obtained from the
minimal polynomial of $\mathrm{jqN}\,M$ over the intermediate field
$\mathbb{Q}(\mathrm{jq})\subseteq\mathbb{Q}((q))$ by applying to each coefficient the inclusion into
$\mathbb{Q}((q))$, then the substitution $q\mapsto q^{Mp}$, then the coefficientwise map
$\mathbb{Q}\to K$. Two hypotheses are imposed on the roots of $P$ in $K((q))$: first, if $y$ is a
root and $y=\mathrm{jq}$ rescaled by $q\mapsto q^{M^{2}p}$ and twisted by a unit $w\in K^\times$
(the twist multiplying the coefficient of $q^{k}$ by $w^{k}$), then $w=1$; second, no root of $P$
equals the image in $K((q))$ of $\mathrm{jqN}(Mp^{2})$ rescaled by $q\mapsto q^{Mp}$. The conclusion
is that $\mathrm{jqN}\,M$ lies in the intermediate field of $\mathbb{Q}((q))$ generated over
$\mathbb{Q}$ by $\mathrm{jq}$ and $\mathrm{jqN}(Mp)$.
This is the descent step in the purely algebraic determination of the field generated by the $q$-expansions of $j$ and $j_N$: passing from level $Mp$ down to level $M$, $j(q^{M})$ is recovered as the unique common root of the level-$p$ modular equation evaluated at $j(q^{Mp})$ and of the minimal polynomial of $j(q^{M})$ over $\mathbb{Q}(j)$. It feeds the generation statement $\mathbb{Q}(j,j_N)$ for the function field of $X_0(N)$ and the computation of $[\mathbb{Q}(j)(j_N):\mathbb{Q}(j)]=\psi(N)$, i.e. irreducibility of the modular polynomial $\Phi_N$ over $\mathbb{Q}(j)$.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_jqN_div_mem_modularFunctionField.lean
<!-- Generated by add_prove2me_provenance.py -->