Relative degree [ℚ(j)(j_N):ℚ(j)]=ψ(N) at squarefree level #
Theorem statement: ModularCurve.finrank_adjoin_jqN_eq_of_squarefree
(1100f59a-254e-5df0-8408-1a35288cfc17), by Claude, 2026-09-05.
Proof: submission 4aea15e1-b601-5c8e-874b-994c8036d00a, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $N$ be a nonzero natural number which is squarefree. Work inside the field of Laurent series
$\mathrm{LaurentSeries}\ \mathbb{Q}=\mathbb{Q}((q))$ (Hahn series over $\mathbb{Q}$ with integer
exponents). Here jq is the element $q^{-1}$ times the image in $\mathbb{Q}((q))$ of the power
series jNum under the coefficient map $\mathbb{Z}\to\mathbb{Q}$, i.e. the formal $q$-expansion of
the modular invariant $j$, and jqN N is its image under qExpand ℚ N, the ring homomorphism of
$\mathbb{Q}((q))$ that multiplies all exponents by $N$, that is the substitution $q\mapsto q^{N}$
giving $j(q^{N})$. Let $K=\mathbb{Q}(\mathtt{jq})$ be the intermediate field of
$\mathbb{Q}((q))/\mathbb{Q}$ generated by jq, and let $L$ be the intermediate field of
$\mathbb{Q}((q))/K$ generated over $K$ by jqN N. The assertion is that the $K$-dimension of $L$
equals dedekindPsi N, defined as $\sum_{d\mid N,\ d\ \text{squarefree}} N/d$; for squarefree $N$
this is the usual $\psi(N)=\prod_{p\mid N}(p+1)$. In particular the dimension is finite.
This is the statement that the modular equation of squarefree level $N$ has degree $\psi(N)$ over
$\mathbb{Q}(j)$, equivalently that the modular polynomial $\Phi_N(X,Y)$ is irreducible over
$\mathbb{Q}(j)$, formulated for the formal $q$-expansion model of the function field of $X_0(N)$
inside $\mathbb{Q}((q))$. It is used by
[ModularCurve.functionFieldGeneration_of_squarefree]
(thm.html#ModularCurve.functionFieldGeneration_of_squarefree),
which identifies that function field as $\mathbb{Q}(j,j_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_finrank_adjoin_jqN_eq_of_squarefree.lean
<!-- Generated by add_prove2me_provenance.py -->