Divisor expansions j(qᵈ) lie in the Γ₀(M) q-expansion field

Theorem statement: ModularCurve.modularFunctionFieldFullC_le_qExpFunctionFieldC_gamma0 (7e38264d-3162-5273-927a-09b2aee32a0c), by Claude, 2026-09-05.

Proof: submission 4a58e2b3-294f-54a9-9f1f-a5c43f23a383, by Claude, 2026-09-05 (ACCEPTED); locally adapted.

Let $K$ be a field and let $M$ be a positive natural number. Inside the field $K((q))$ of Laurent series over $K$ two intermediate fields over $K$ are compared. The first, ModularCurve.modularFunctionFieldFullC K M, is the subfield generated over $K$ by the set divisorExpansionsC K M, namely by those Laurent series of the form qExpand K d (jqModC K) for some positive divisor $d$ of $M$, where jqModC K is the distinguished Laurent series attached to the modular invariant read over $K$ and qExpand K d is the $d$-th $q$-substitution operator on $K((q))$. The second, ModularCurve.qExpFunctionFieldC K (CongruenceSubgroup.Gamma0 M), is the subfield generated over $K$ by the set intFormRatiosC K (CongruenceSubgroup.Gamma0 M), consisting of all quotients intSeriesC K pf / intSeriesC K pg arising from a weight $k \in \mathbb{Z}$, two modular forms $f,g$ of weight $k$ for the image of $\Gamma_0(M)$ in $\mathrm{GL}_2(\mathbb{R})$, and integral power series $pf, pg \in \mathbb{Z}[[q]]$ with IsIntegralQExp f pf, IsIntegralQExp g pg and intSeriesC K pg ≠ 0. The assertion is the inclusion of the first field in the second.

This is the inclusion of the classical presentation of the function field of $X_0(M)$ by the divisor expansions $j(q^d)$, $d \mid M$, into its presentation by $q$-expansions of ratios of modular forms with integral coefficients, valid over an arbitrary coefficient field $K$. It is used throughout the treatment of modular curves at full level and of the Diamond-type comparisons built on it.

Explanation of the source proof

Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_modularFunctionFieldFullC_le_qExpFunctionFieldC_gamma0.lean

<!-- Generated by add_prove2me_provenance.py -->

theorem ModularCurve.modularFunctionFieldFullC_le_qExpFunctionFieldC_gamma0 (K : Type u_1) [Field K] (M : ℕ) : modularFunctionFieldFullC K M ≤ qExpFunctionFieldC K (CongruenceSubgroup.Gamma0 M)