j-series lies in the integral form ratios over any K, Γ #
Theorem statement: ModularCurve.jqModC_mem_intFormRatiosC
(ba43d59b-e15b-5d68-810c-9c701699d584), by Claude, 2026-09-05.
Proof: submission 5306c1cb-d541-58ef-979c-6dd8b0dfe090, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $K$ be a field and let $\Gamma$ be an arbitrary subgroup of $\mathrm{SL}_2(\mathbb{Z})$. Write
$\bar\jmath =$ ModularCurve.jqModC K for the Laurent series
over $K$ given by $X^{-1}$ (the Hahn series single (-1) 1) times the image in $K[[X]]$ of the
integral power series jNum $=$ eisenstein4$^3 \cdot$ dedekindEtaUnitInv, the coefficients
being reduced along $\mathbb{Z} \to K$. The assertion is that $\bar\jmath$ belongs to
intFormRatiosC K Γ, i.e. that there are an integer $k$, two modular forms $f, g$ of weight $k$ for
the image of $\Gamma$ in $\mathrm{GL}_2(\mathbb{R})$, and two power series $p_f, p_g \in \mathbb{Z}[[X]]$ such that $p_f$ and $p_g$, mapped to $\mathbb{C}[[X]]$, are the $q$-expansions
(with respect to period $1$) of $f$ and of $g$ respectively, such that the reduction of $p_g$ to a
Laurent series over $K$ is nonzero, and such that $\bar\jmath$ equals the quotient of the reductions
of $p_f$ and $p_g$ in $K((X))$. The witnesses are $k = 12$, $f$ the restriction to $\Gamma$ of
$E_4^3$ and $g$ the restriction to $\Gamma$ of the discriminant, with $p_f =$ eisenstein4$^3$ and
$p_g = X \cdot$ dedekindEtaUnit.
This is the classical identity $j = E_4^3/\Delta$, recorded in the shape needed here: the formal $q$-expansion of the modular invariant, read over an arbitrary coefficient field, is a ratio of $q$-expansions of two weight-$12$ forms with integral expansions on any subgroup of $\mathrm{SL}_2(\mathbb{Z})$. It supplies the transcendental element inside the $q$-expansion function field of a modular curve over $K$, and is used throughout the treatment of modular curves and their function fields, including in positive characteristic.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_jqModC_mem_intFormRatiosC.lean
<!-- Generated by add_prove2me_provenance.py -->