Descent closure: F_N = F_N^{full} from one-prime steps #
Theorem statement: ModularCurve.modularFunctionField_eq_full_of
(4cd6f92a-c178-5239-b610-1c75c886bc3f), by Claude, 2026-09-05.
Proof: submission e37f23f1-9452-511f-a3b0-5c5c2ac408cf, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Work inside the Laurent series field $\mathbb{Q}((q))$, where for a nonzero natural number $d$ the
ring homomorphism ModularCurve.qExpand ℚ d substitutes $q \mapsto q^{d}$ (it reindexes exponents by multiplication by $d$), jq is the $q$-expansion of the modular
$j$-invariant, and jqN d is its image qExpand ℚ d jq, i.e. $j(q^{d})$. For a nonzero natural
number $N$, modularFunctionField N denotes the intermediate field $\mathbb{Q}(j(q), j(q^{N}))$
obtained by adjoining the two elements jq and qExpand ℚ N jq to $\mathbb{Q}$, while
modularFunctionFieldFull N is the intermediate field obtained by adjoining the whole set of
expansions $j(q^{d})$ for all nonzero divisors $d$ of $N$. The theorem fixes such an $N$ and assumes
two families of hypotheses, indexed by the factorisations of $N$ as $N = M p$ with $M$ nonzero and
$p$ prime: first, that $j(q^{M})$ lies in modularFunctionField N; second, that
modularFunctionField M = modularFunctionFieldFull M. Its conclusion is that modularFunctionField N = modularFunctionFieldFull N, that is, $\mathbb{Q}(j(q), j(q^{N}))$ already contains $j(q^{d})$
for every divisor $d$ of $N$.
This is the assembling step of the generation theorem for the function field of $X_0(N)$ over $\mathbb{Q}$: it propagates, along the divisor lattice, the statement that all expansions $j(q^{d})$ with $d \mid N$ are generated by $j(q)$ and $j(q^{N})$. It is used in the induction that yields the generation statement at all levels and, with it, the degree computation $[\mathbb{Q}(j)(j_N):\mathbb{Q}(j)] = \psi(N)$ and the irreducibility of the modular polynomial $\Phi_N$.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_modularFunctionField_eq_full_of.lean
<!-- Generated by add_prove2me_provenance.py -->