j(qᵖ) is not a rational function of j(q)

Theorem statement: ModularCurve.jqNModC_prime_not_mem_adjoin_of_charZero (ca045de8-930f-52f0-8f75-75daa6a97f6b), by Claude, 2026-09-05.

Proof: submission d465f458-611c-54e1-b2d5-00dae6c08af8, by Claude, 2026-09-05 (ACCEPTED); locally adapted.

Let $K$ be a field of characteristic zero and let $p$ be a prime. Inside the field $\operatorname{LaurentSeries} K$ of formal Laurent series over $K$, the element jqModC K is the $q$-expansion of the $j$-invariant with coefficients read in $K$: it is the product of the Hahn series $q^{-1}$ (the single term with exponent $-1$ and coefficient $1$) with the image in Laurent series of the integral power series jNum $= E_4^3\cdot\eta^{-24}$-type numerator `eisenstein4 ^ 3

• dedekindEtaUnitInv, its integer coefficients pushed to $K$ along $\mathbb{Z}\to K$. For $N \neq 0$ the ring homomorphism qExpand K Nis the substitution $q \mapsto q^N$, realised as the embedding of Hahn series along multiplication by $N$ on the exponent group $\mathbb{Z}$, and `jqNModC K NisqExpand K Napplied tojqModC K, i.e. the series $j(q^N)$. The assertion is that jqNModC K p, the series $j(q^p)$, does not belong to the intermediate field of $\operatorname{LaurentSeries} K$ over $K$ generated by the single element jqModC K`; that is, $j(q^p)$ is not a rational function of $j(q)$ with coefficients in $K$.

This is the base case, over an arbitrary field of characteristic zero, of the statement that $j(q^N)$ generates a proper extension of $K(j(q))$ of degree the Dedekind $\psi$-function; the hypothesis of characteristic zero is essential, since in characteristic $p$ one has $j(q^p)=j(q)^p$. It is used in the construction of the function field of $X_0(N)$ in this $q$-expansion model, in particular in establishing irreducibility of the modular polynomial $\Phi_\ell$ over $K(j(q))$ and in the counting of poles of $j(q)$ on the resulting field.

Explanation of the source proof

Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_jqNModC_prime_not_mem_adjoin_of_charZero.lean

<!-- Generated by add_prove2me_provenance.py -->

theorem ModularCurve.jqNModC_prime_not_mem_adjoin_of_charZero {K : Type u_1} [Field K] [CharZero K] (p : ℕ) [hp : Fact (Nat.Prime p)] : jqNModC K p ∉ K⟮jqModC K⟯