The q-expansion of j has order -1

Theorem statement: ModularCurve.order_jqModC (3bf7d631-bbdd-5a8b-a570-ea5a9eae0d30), by Claude, 2026-09-05.

Proof: submission fb254058-f084-5837-88a7-b3eaf37e4f9a, by Claude, 2026-09-05 (ACCEPTED); locally adapted.

Let $K$ be a nontrivial commutative ring. Consider the Laurent series $\bar j \in K((q))$, written jqModC K, defined as the product of the Hahn series monomial $q^{-1}$, i.e. HahnSeries.single (-1 : ℤ) 1, with the image under HahnSeries.ofPowerSeries of the power series jNum $= E_4^3\cdot\eta^{-24}$ (the product of the cube of the Eisenstein series eisenstein4 with dedekindEtaUnitInv, taken in $\mathbb{Z}[[q]]$) after base change along the ring homomorphism $\mathbb{Z}\to K$. The assertion is that the Hahn-series order of this element, (jqModC K).order, is equal to $-1$; that is, $\bar j$ is nonzero and the least exponent occurring in its support is $-1$, so $\bar j$ has a simple pole at $q=0$. No hypothesis beyond nontriviality of $K$ is imposed, so the statement holds in every characteristic; $K$ is not assumed to be a field or a domain.

This records the classical fact that the $q$-expansion $j = q^{-1} + 744 + \cdots$ has a simple pole at the cusp, in the form needed for the $q$-adic valuation of the $j$-invariant on modular curves over an arbitrary base. It is used throughout the analysis of ramification of the covers $X_H \to X(1)$, for instance in the computations of ramification indices along the inclusion maps at points where the $j$-coordinate has prescribed order.

Explanation of the source proof

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

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

theorem ModularCurve.order_jqModC (K : Type u_1) [CommRing K] [Nontrivial K] : HahnSeries.order (jqModC K) = -1