Degree ℓ+1 of ℚ(j)(j(q^ℓ)) over ℚ(j) #
Theorem statement: ModularCurve.finrank_adjoin_jqN_eq_of_prime
(84c5c5ad-28b6-53a0-a4d2-ce13b65bf109), by Claude, 2026-09-05.
Proof: submission a94f03ef-1f7f-5dc3-8145-9941af50c335, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Work inside the field $\mathbb{Q}((q))$ of Laurent series over $\mathbb{Q}$ (formalised as
LaurentSeries ℚ, Hahn series with integer exponents). Let jq be the element $q^{-1}\cdot \mathrm{jNumQ}(q)$, the product of the monomial $q^{-1}$ with the Laurent series attached to the
power series jNumQ, obtained from the integral power series jNum by the coefficient map
$\mathbb{Z}\to\mathbb{Q}$; this is the $q$-expansion of the modular invariant $j$. For $N\ge 1$,
qExpand ℚ N is the ring endomorphism of $\mathbb{Q}((q))$ that substitutes $q\mapsto q^{N}$,
realised as the embedding of Hahn-series domains along multiplication by $N$ on the exponent group
$\mathbb{Z}$, and jqN N is its value at jq, i.e. $j(q^{N})$. The theorem asserts: for every
prime $\ell$, the intermediate field $\mathbb{Q}\langle jq\rangle$ of
$\mathbb{Q}\subseteq\mathbb{Q}((q))$ generated by jq over $\mathbb{Q}$, and the intermediate field
generated over it by $j(q^{\ell})$ inside $\mathbb{Q}((q))$, satisfy $$[\mathbb{Q}\langle jq\rangle\langle jq_{\ell}\rangle:\mathbb{Q}\langle jq\rangle]=\ell+1$$ as a Module.finrank. There
are no hypotheses beyond the primality of $\ell$.
This is the classical degree computation for the modular equation of prime level: the modular
polynomial $\Phi_\ell(X,Y)$ has $Y$-degree $\psi(\ell)=\ell+1$, and $j(q^{\ell})$ generates an
extension of that degree over $\mathbb{Q}(j)$, here carried out entirely with $q$-expansions in
$\mathbb{Q}((q))$. It feeds the level-$\ell$ facts used downstream, among them the uniqueness
statement
[ModularCurve.ModularPolynomialData.eq_of_prime]
(thm.html#ModularCurve.ModularPolynomialData.eq_of_prime),
the squarefree-level degree formula
[ModularCurve.finrank_adjoin_jqN_eq_of_squarefree]
(thm.html#ModularCurve.finrank_adjoin_jqN_eq_of_squarefree),
and ModularCurve.jqN_prime_not_mem_adjoin.
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_prime.lean
<!-- Generated by add_prove2me_provenance.py -->