Function field generation at squarefree level #
Theorem statement: ModularCurve.functionFieldGeneration_of_squarefree
(3024c339-8925-59b6-9af7-09c343513ffd), by Claude, 2026-09-05.
Proof: submission 42bcbf2e-1dcb-55d8-8c93-45f2c31520f7, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $N$ be a natural number which is nonzero and squarefree. The conclusion is the predicate
FunctionFieldGeneration N, which asserts: for every natural number $d$ dividing $N$ and nonzero,
the Laurent series qExpand ℚ d jq belongs to the intermediate field $\mathbb{Q}(\mathtt{jq},\ \mathtt{qExpand}\ \mathbb{Q}\ N\ \mathtt{jq})$, i.e. to IntermediateField.adjoin ℚ {jq, qExpand ℚ N jq} inside the field LaurentSeries ℚ of Laurent series over $\mathbb{Q}$. Here jq is the
distinguished element of LaurentSeries ℚ serving as the $q$-expansion of the modular invariant
$j$, and for a nonzero $m$ the map qExpand ℚ m is the ring endomorphism of LaurentSeries ℚ
obtained by transporting the Hahn-series support along multiplication by $m$ on exponents, that is,
the substitution $q \mapsto q^{m}$. Thus for squarefree $N$ each $j(q^{d})$ with $d \mid N$ lies in
the subfield of $\mathbb{Q}((q))$ generated over $\mathbb{Q}$ by $j(q)$ and $j(q^{N})$.
This is the statement that, at squarefree level, the field generated by all $j(q^{d})$ for $d \mid N$ collapses to the two-generator field $\mathbb{Q}(j(q), j(q^{N}))$, the $q$-expansion model of the
function field of $X_0(N)$ over $\mathbb{Q}$. It is used in the purely algebraic determination of
$[\mathbb{Q}(j)(j_N):\mathbb{Q}(j)] = \psi(N)$ and the irreducibility of the modular polynomial, and
is cited by ModularCurve.jqN_prime_not_mem_full
and
ModularCurve.minpoly_jqN_map_eq_prod_slots.
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_of_squarefree.lean
<!-- Generated by add_prove2me_provenance.py -->