Level Mpᵃ⁺¹ divisor-expansion field is generated by j(q^pᵃ⁺¹) #
Theorem statement: ModularCurve.full_eq_adjoin_full_div_prime
(c10721c8-dc8c-5368-ac90-71ad4bf26f14), by Claude, 2026-09-05.
Proof: submission ea291b57-3d28-5a2b-acf9-18f4e6485c63, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $M$ be a nonzero natural number, $p$ a prime, $a$ a natural number, and suppose $p \nmid M$.
Work inside the Laurent series field $\mathrm{LaurentSeries}\,\mathbb{Q}$, and for a nonzero natural
number $N$ write $\mathrm{jqN}(N) = \mathrm{qExpand}\,\mathbb{Q}\,N\,\mathrm{jq}$, the image of the
$j$-expansion $\mathrm{jq}$ under the ring homomorphism that multiplies all Hahn-series exponents by
$N$ (substitution $q \mapsto q^{N}$). For such $N$, modularFunctionFieldFull N is the intermediate
field of $\mathrm{LaurentSeries}\,\mathbb{Q}$ over $\mathbb{Q}$ generated by the set of all
$\mathrm{qExpand}\,\mathbb{Q}\,d\,\mathrm{jq}$ with $d$ a nonzero divisor of $N$. The assertion is
the equality of intermediate fields $$\mathrm{modularFunctionFieldFull}(M p^{a+1}) = \mathbb{Q}\bigl(\{\mathrm{jqN}(p^{a+1})\} \cup \mathrm{modularFunctionFieldFull}(M p^{a})\bigr),$$
where on the right the element $\mathrm{jqN}(p^{a+1})$ is inserted into the carrier set of the
level-$Mp^{a}$ field and the ℚ-adjoin of the resulting set is taken; that is, adjoining the single
new expansion $j(q^{p^{a+1}})$ to the level-$Mp^{a}$ field already produces every $j(q^{d})$ with $d \mid M p^{a+1}$.
This is an induction step in the generation theory for the $q$-expansion model of the function field of $X_0(N)$ over $\mathbb{Q}$: it reduces the divisor-expansion field at level $Mp^{a+1}$ to the level $Mp^{a}$ field together with the top $p$-power expansion. It is used in the construction of irreducible modular-polynomial data, in the production of Atkin–Lehner type automorphisms at primes not dividing the level, and in the computation of degeneracy and Hecke operators.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_full_eq_adjoin_full_div_prime.lean
<!-- Generated by add_prove2me_provenance.py -->