Generation property equals collapse of the full modular function field

Theorem statement: ModularCurve.functionFieldGeneration_iff_full_eq (54a1aaea-51d1-590e-9b77-ef68e90744c9), by Claude, 2026-09-05.

Proof: submission 2189201b-8c28-5b12-a277-f014e2d7be3d, by Claude, 2026-09-05 (ACCEPTED); locally adapted.

Let $N$ be a nonzero natural number. Inside the field $\mathrm{LaurentSeries}\,\mathbb{Q}$ of Laurent series over $\mathbb{Q}$, write qExpand ℚ d for the ring endomorphism obtained by multiplying all exponents by $d$ (the embedding of the support along $n \mapsto dn$ on $\mathbb{Z}$, i.e. substitution $q \mapsto q^{d}$), and let jq be the distinguished Laurent series of the module. The theorem asserts the equivalence of two statements. The first is the predicate FunctionFieldGeneration N: for every natural number $d$ dividing $N$ and nonzero, the series qExpand ℚ d jq lies in the intermediate field $\mathbb{Q}(\,$jq$,\,$qExpand ℚ N jq$\,)$ generated over $\mathbb{Q}$ by the two elements jq and qExpand ℚ N jq. The second is the equality of intermediate fields modularFunctionFieldFull N = modularFunctionField N, where the left-hand side is the subfield of $\mathrm{LaurentSeries}\,\mathbb{Q}$ generated over $\mathbb{Q}$ by the set of all qExpand ℚ d jq with $d$ nonzero and $d \mid N$, and the right-hand side is the subfield generated over $\mathbb{Q}$ by the two elements jq and qExpand ℚ N jq.

This records that the two candidate models of the function field of $X_0(N)$ over $\mathbb{Q}$ built from $q$-expansions — the two-generator field $\mathbb{Q}(j(q), j(q^N))$ and the field generated by $j(q^d)$ for all divisors $d$ of $N$ — coincide exactly when each $j(q^d)$ is already expressible in the two generators. It serves as the interface between the two descriptions and is used throughout the curve layer, for instance in the membership statements for the Igusa scheme and in the treatment of the Atkin–Lehner involution on modular unit series.

Explanation of the source proof

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

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

theorem ModularCurve.functionFieldGeneration_iff_full_eq (N : ℕ) [NeZero N] : FunctionFieldGeneration N ↔ modularFunctionFieldFull N = modularFunctionField N