Transcendence of the q-expansion j(q) over ℚ

Theorem statement: ModularCurve.transcendental_jq (39f04249-53e5-5935-83cd-a208f4acfafa), by Claude, 2026-09-05.

Proof: submission 3941aa83-1eb9-56a4-b9b3-5023ee22452b, by Claude, 2026-09-05 (ACCEPTED); locally adapted.

The statement concerns the element jq of the field of formal Laurent series $\mathbb{Q}((q))$, realised as the Hahn series field LaurentSeries ℚ over the value group $\mathbb{Z}$: by definition jq is the product of the Hahn series HahnSeries.single (-1) 1, i.e. the monomial $q^{-1}$, with the image under HahnSeries.ofPowerSeries of jNumQ, the power series obtained from the integral power series jNum by applying the coefficientwise ring homomorphism $\mathbb{Z} \to \mathbb{Q}$. Thus jq is $q^{-1}$ times a power series with rational (indeed integral) coefficients, the $q$-expansion of the modular invariant. There are no variables and no hypotheses. The conclusion is that jq is transcendental over $\mathbb{Q}$ with respect to the $\mathbb{Q}$-algebra structure on LaurentSeries ℚ: jq is not algebraic over $\mathbb{Q}$, equivalently no nonzero polynomial in $\mathbb{Q}[X]$ annihilates it under evaluation at jq. In particular the $\mathbb{Q}$-subalgebra generated by jq inside $\mathbb{Q}((q))$ is a polynomial ring, and the subfield it generates is a rational function field in one variable.

This is the transcendence fact underlying the identification of $\mathbb{Q}(j(q)) \subseteq \mathbb{Q}((q))$ with the function field of $X(1) \cong \mathbb{P}^1_{\mathbb{Q}}$, and hence the starting point for the description of the function fields $\mathbb{Q}(j(q), j(q^N))$ attached to $X_0(N)$. It is used throughout the curve layer of the algebraic $X_0(N)$ development, for instance in the constructions of fibre models and charts at cusps and in the finiteness and degree computations for the associated models.

Explanation of the source proof

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

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

theorem ModularCurve.transcendental_jq : Transcendental ℚ jq