j(q^N) is integral over ℤ[j(q)] #
Theorem statement: ModularCurve.exists_monic_evalAtJ_jqN_eq_zero
(fe691968-8b4a-5117-ad3d-849d8a55961b), by Claude, 2026-09-05.
Proof: submission c89e6f47-0caf-5f44-afa0-923c89ba9d3a, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $N$ be a natural number with $N \neq 0$. The assertion is that there is a polynomial $P$ in one
variable over the ring $\mathbb{Z}[X]$ of integer polynomials, i.e. $P \in (\mathbb{Z}[X])[Y]$,
which is monic, and which vanishes when its coefficients are pushed into the field of Laurent series
$\mathrm{LaurentSeries}\ \mathbb{Q}$ by the ring homomorphism evalAtJ and the variable is
evaluated at jqN N. Here evalAtJ is the ring homomorphism $\mathbb{Z}[X] \to \mathrm{LaurentSeries}\ \mathbb{Q}$ obtained by evaluating at the Laurent series jq, the
$q$-expansion of the modular invariant $j$, so that its image is the subring $\mathbb{Z}[j(q)]$; and
jqN N is the image of jq under qExpand ℚ N, the ring endomorphism of $\mathrm{LaurentSeries}\ \mathbb{Q}$ that transports a Hahn series along multiplication by $N$ on the exponent group
$\mathbb{Z}$ (this map being injective and order-preserving because $N > 0$), that is, the
substitution $q \mapsto q^N$, so jqN N is the $q$-expansion of $j(q^N)$. Thus $j(q^N)$ satisfies a
monic equation with coefficients in $\mathbb{Z}[j(q)]$; no irreducibility or degree statement is
made.
This is the integrality half of the classical theory of the modular equation: $j(q^N)$ is integral over $\mathbb{Z}[j(q)]$ inside $\mathbb{Q}((q))$, for every $N \geq 1$, with no squarefree restriction. It feeds the formal $q$-expansion model of the function field of $X_0(N)$, being cited in the construction of modular polynomial data, in the identification of levels where $\Phi_N$ is irreducible via a degree computation, and in the study of the $j$-shadow at full level.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_exists_monic_evalAtJ_jqN_eq_zero.lean
<!-- Generated by add_prove2me_provenance.py -->