Integrality over ℂ[j] of pole-bounded level-N quotients #
Theorem statement: WLight.exists_monicRel_j_of_mdifferentiable_levelFraction
(384ea021-4486-5798-8a93-9d7cb91a90f0), by Claude, 2026-09-05.
Proof: submission 179980d2-28fa-5428-819a-d48ea8decd60, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Fix a natural number $N \neq 0$. Let $L$ assign to each $\tau \in \mathbb{H}$ a period pair, subject to $(L\tau).\omega_1 = \tau$ and $(L\tau).\omega_2 = 1$; let $W$ be a family of functions on $\mathbb{H}$ indexed by $v \in (\mathbb{Z}/N)^2$ pinned pointwise by $W_v(\tau) = (2\pi i)^{-2}\,\wp_{L\tau}\big((\tilde v_0\tau + \tilde v_1)/N\big)$, where $\tilde v_i$ denotes the natural-number representative of $v_i$; let $\mathrm{fricke}$ be pinned pointwise by $\mathrm{fricke}_v(\tau) = -\big(E_4(\tau)E_6(\tau)/\Delta(\tau)\big)/2592 \cdot W_v(\tau)$; and let $jf$ be pinned pointwise by $jf(\tau) = E_4(\tau)^3/\Delta(\tau)$. Let $a, b, F : \mathbb{H} \to \mathbb{C}$, with $a$ and $b$ both lying in the $\mathbb{C}$-subalgebra of the pointwise ring of functions $\mathbb{H} \to \mathbb{C}$ generated by $jf$ together with all $\mathrm{fricke}_v$ for $v \neq 0$, with $b$ not the zero function, with $F$ holomorphic on $\mathbb{H}$ (as a map of complex manifolds), with $F \cdot b = a$ pointwise, and with the pole bound: for every $\gamma \in \mathrm{SL}_2(\mathbb{Z})$ there is $m \in \mathbb{N}$ such that $\tau \mapsto F(\gamma \cdot \tau)\,\Delta(\tau)^m$ is bounded as $\operatorname{im}\tau \to \infty$. Then there exist $d \in \mathbb{N}$ and polynomials $p_0,\dots,p_{d-1} \in \mathbb{C}[X]$ with $F(\tau)^d + \sum_{i<d} p_i(jf(\tau))\,F(\tau)^i = 0$ for all $\tau \in \mathbb{H}$.
This is the integrality half of the classical fact that a holomorphic modular function of level $N$ whose poles are confined to the cusps is integral over $\mathbb{C}[j]$; here the pole bound on all $\mathrm{SL}_2(\mathbb{Z})$-translates of $F$ is assumed rather than deduced from membership in the level-$N$ modular function field, so the statement is weaker than the classical one and each consumer verifies the bound for its own $F$. It is used in the study of $q$-expansion coefficients and rationality of Fricke functions on modular curves, and its proof cites the level-one hauptmodul package and the modularity package for the Fricke functions $\mathrm{fricke}_v$.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_WLight_exists_monicRel_j_of_mdifferentiable_levelFraction.lean
<!-- Generated by add_prove2me_provenance.py -->