Relative degree ψ(N) of the field of divisor q-expansions #
Theorem statement: ModularCurve.relfinrank_full_eq_dedekindPsi
(cab9a0f3-98f2-5f8b-b199-b15d58eaf279), by Claude, 2026-09-05.
Proof: submission 538a4427-4bf3-52eb-94f1-b15c7aaed5eb, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $N$ be a natural number assumed nonzero. Inside the field $\mathbb{Q}((q))$ of formal Laurent
series over $\mathbb{Q}$, let $jq$ denote the series $q^{-1}$ times the image under
$\mathbb{Z}\to\mathbb{Q}$ of the integral power series jNum, i.e. the $q$-expansion of the modular
invariant $j$. Write $\mathbb{Q}(jq)$ for the intermediate field IntermediateField.adjoin ℚ {jq},
and let modularFunctionFieldFull N be the intermediate field of $\mathbb{Q}((q))/\mathbb{Q}$
generated by the set of all substitutions $q\mapsto q^{d}$ applied to $jq$, namely $\{\,$qExpand ℚ d jq $: d\neq 0,\ d\mid N\,\}$, so the field generated over $\mathbb{Q}$ by the expansions
$j(q^{d})$ for the positive divisors $d$ of $N$. The assertion is that the relative degree, in the
sense of IntermediateField.relfinrank, of modularFunctionFieldFull N over $\mathbb{Q}(jq)$
equals dedekindPsi N, defined as the sum $\sum_{d\mid N,\ d\ \text{squarefree}} N/d$; since $d=1$
divides $N$, the smaller field is contained in the larger one, so this is the degree
$[\mathbb{Q}(j(q^{d}):d\mid N):\mathbb{Q}(j(q))]$, and the sum is the Dedekind $\psi$-function
$N\prod_{p\mid N}(1+p^{-1})$.
This is the degree statement equivalent to the irreducibility of the modular polynomial $\Phi_N$ over $\mathbb{Q}(j)$, here in the relative-degree form for subfields of $\mathbb{Q}((q))$ generated by $q$-expansions. It underlies the function-field description of the modular curves $X_0(N)$ and is used in the subsequent degree computations and in the analysis of places and their prolongations along $j$ and $j(q^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_relfinrank_full_eq_dedekindPsi.lean
<!-- Generated by add_prove2me_provenance.py -->