Transcendence of the q-expansion of j over any coefficient ring

Theorem statement: ModularCurve.transcendental_jqModC (ea2ce9fb-744f-5e69-93fc-a5debf04eab1), by Claude, 2026-09-05.

Proof: submission ea2dd952-adf4-5186-ab7c-03ff62ff75e1, by Claude, 2026-09-05 (ACCEPTED); locally adapted.

Let $K$ be a commutative ring. Consider the Laurent series $\bar j =$ jqModC K $\in K((q)) =$ LaurentSeries K $=$ HahnSeries ℤ K, defined as the product of the Hahn series HahnSeries.single (-1) 1 (the monomial $q^{-1}$) with the image under HahnSeries.ofPowerSeries of the power series obtained from the integral series jNum $=$ eisenstein4 ^ 3 * dedekindEtaUnitInv by applying the coefficientwise map $\mathbb{Z} \to K$. The theorem asserts that $\bar j$ is transcendental over $K$, with respect to the canonical $K$-algebra structure on $K((q))$: Transcendental K (jqModC K), that is, $\bar j$ is not algebraic over $K$, equivalently the only polynomial $p \in K[X]$ with $p(\bar j) = 0$ (evaluation via Polynomial.aeval) is $p = 0$. No hypotheses beyond commutativity of $K$ are imposed; in particular $K$ is not assumed to be a field, a domain, nontrivial, or of any particular characteristic (for the trivial ring the assertion holds because $K[X]$ is then the zero ring).

This is the standard statement that the $q$-expansion $q^{-1} + 744 + \cdots$ of the modular invariant $j$ satisfies no algebraic relation over its ring of coefficients, so that $K(\bar j)$ sits inside $K((q))$ as a rational function field in any characteristic. It underlies the construction of models of modular curves and of the $q$-expansion formalism used throughout, and is cited very widely in the development, for instance by the results comparing $q$-expansions of cusp forms and mod $p$ forms with power series on cusp charts.

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_jqModC.lean

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

theorem ModularCurve.transcendental_jqModC (K : Type u_1) [CommRing K] : Transcendental K (jqModC K)