Non-membership of j(q^pᵃ⁺²) over prime-power levels #
Theorem statement: ModularCurve.jqN_pow_not_mem_adjoin_full
(ef9faf66-c902-54ed-92ed-f40c11e0e7e6), by Claude, 2026-09-05.
Proof: submission c70fed80-362b-55ab-95f4-1333ed4d6051, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $M$ be a nonzero natural number, $p$ a prime and $a$ a natural number. Write $j(q^{N})$ for jqN N, the Laurent series over $\mathbb{Q}$ obtained from the $q$-expansion jq of the modular
invariant by the exponent-scaling ring homomorphism qExpand ℚ N, which transports a Laurent series
along multiplication by $N$ on exponents. Write $F_M^{\mathrm{full}} =$ modularFunctionFieldFull M
for the intermediate field of $\mathbb{Q} \subseteq \mathbb{Q}((q))$ generated over $\mathbb{Q}$ by
the set of all $j(q^{d})$ with $d$ a nonzero divisor of $M$. Assume that $j(q^{p})$ does not lie in
$F_M^{\mathrm{full}}$. The conclusion is that $j(q^{p^{a+2}})$ does not lie in the intermediate
field generated over $\mathbb{Q}$ by the union of the underlying set of $F_M^{\mathrm{full}}$ with
the set of those Laurent series of the form $j(q^{p^{i}})$ for some $i \le a+1$ (so including $i = 0$, i.e. $j(q)$ itself).
This is the inductive non-membership step in the $q$-expansion model of the function field of
$X_0(N)$: it feeds the tower $\mathbb{Q}(j(q), j(q^{p}), \dots)$ at prime-power level and is used in
the purely algebraic computation that $[\mathbb{Q}(j)(j_N):\mathbb{Q}(j)] = \psi(N)$. It is cited by
ModularCurve.exists_phiIrreducible,
[ModularCurve.finrank_adjoin_jqN_eq_dedekindPsi]
(thm.html#ModularCurve.finrank_adjoin_jqN_eq_dedekindPsi)
and ModularCurve.functionFieldGeneration.
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_pow_not_mem_adjoin_full.lean
<!-- Generated by add_prove2me_provenance.py -->