j(q^r) is not rational in j and the j(qᵖ), p∈ S #
Theorem statement: ModularCurve.jqN_prime_not_mem_adjoin (80c9a2aa-2c5c-5aa9-ae39-f3296c43be03),
by Claude, 2026-09-05.
Proof: submission ec5f8305-42b1-5eb4-84b8-af2f2cfaa80d, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Work inside the field $\mathbb{Q}((q))$ of rational Laurent series, realised as LaurentSeries ℚ.
Here jq denotes the Laurent series $q^{-1}\cdot j_{\mathrm{num}}$, where $j_{\mathrm{num}}$ is the
integral power series jNum with its coefficients mapped into $\mathbb{Q}$, so jq is the
$q$-expansion of the modular invariant $j$; and for $N\neq 0$, jqN N is the image of jq under
the ring homomorphism qExpand ℚ N, which multiplies all exponents by $N$, i.e. the substitution
$q\mapsto q^{N}$, giving $j(q^{N})$. The data are: a finite set $S$ of natural numbers, a hypothesis
that every $p\in S$ is prime, and a further prime $r$ with $r\notin S$. The conclusion is that
$j(q^{r})$ does not lie in the intermediate field of $\mathbb{Q}((q))$ over $\mathbb{Q}$ generated
by the set consisting of jq together with all Laurent series of the form jqN p for $p\in S$
(each such $p$ being nonzero). Equivalently, $j(q^{r})\notin \mathbb{Q}\bigl(j(q),\,j(q^{p}):p\in S\bigr)$.
This is the descent step in a purely algebraic treatment of the degree of the modular equation: the successive extensions $\mathbb{Q}(j)\subseteq \mathbb{Q}(j,j(q^{p}):p\in S)$ are all proper at each new prime, which is what makes the local degree computations $[\,F(j(q^{p})):F\,]=p+1=\psi(p)$ applicable. It is used in the computation of relative degrees for adjoining several primes and for prime-square levels, and hence in identifying $[\mathbb{Q}(j)(j_N):\mathbb{Q}(j)]$ with $\psi(N)$, i.e. the 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_prime_not_mem_adjoin.lean
<!-- Generated by add_prove2me_provenance.py -->