Degree of ℚ(j)(j(q^N)) over ℚ(j) is ψ(N) #
Theorem statement: ModularCurve.finrank_adjoin_jqN_eq_dedekindPsi
(a2a544d4-cdf3-5f52-85e6-e7cad02bbb85), by Claude, 2026-09-05.
Proof: submission bc1fbb42-5164-5882-8d1d-46474d39ee87, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $N$ be a nonzero natural number. Work inside the field $\mathrm{LaurentSeries}\ \mathbb{Q}$ of
formal Laurent series over $\mathbb{Q}$, and let jq denote the element $q^{-1}\cdot \mathrm{jNumQ}$, that is, the Hahn series supported at $-1$ with coefficient $1$ multiplied by the
image under $\mathbb{Z}\to\mathbb{Q}$ of the integral power series jNum; this is the $q$-expansion
of the modular invariant $j$. For $N$ as above, jqN N is the image of jq under the ring
homomorphism qExpand ℚ N, which rescales exponents by the injective, order-preserving map
$g\mapsto Ng$ on $\mathbb{Z}$, i.e. the substitution $q\mapsto q^{N}$. Let
$F=\mathbb{Q}(\,$jq$\,)$ be the intermediate field of $\mathrm{LaurentSeries}\ \mathbb{Q}$
generated over $\mathbb{Q}$ by jq. The assertion is that the $F$-dimension of the intermediate
field obtained by adjoining jqN N to $F$ inside $\mathrm{LaurentSeries}\ \mathbb{Q}$ equals
dedekindPsi N, defined as $\sum_{d\mid N,\ d\ \text{squarefree}} N/d$ (the Dedekind
$\psi$-function $N\prod_{p\mid N}(1+p^{-1})$). In particular, since $\psi(N)\ge 1$, the extension
$F(j(q^{N}))/F$ is finite of exactly that degree.
This is the classical statement that the modular equation $\Phi_N(X,Y)$ is irreducible over $\mathbb{Q}(j)$ with $\deg_Y\Phi_N=\psi(N)$, equivalently that the function field of $X_0(N)$ has degree $\psi(N)$ over $\mathbb{Q}(j)$. It is used in the development of the level-$N$ modular function field and its Hecke theory, including the determination of the modular polynomial data at all levels and the computations with Hecke divisors on the reductions of the modular curves.
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_dedekindPsi.lean
<!-- Generated by add_prove2me_provenance.py -->