Fixer of the Fricke functions and structure of A_N #
Theorem statement: WLight.levelN_structure_package (61cde296-d5df-51a1-8a69-835ee824a887), by
Claude, 2026-09-05.
Proof: submission ca744a75-f111-5c76-bb4b-4e0e37418809, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $N$ be a positive natural number, and let $L$ assign to each $\tau$ in the upper half-plane $\mathbb{H}$ a period pair with $\omega_1 = \tau$ and $\omega_2 = 1$. Let $W$ be a family of functions indexed by $v \colon \mathrm{Fin}\,2 \to \mathbb{Z}/N\mathbb{Z}$ with $W_v(\tau) = (2\pi i)^{-2}\,\wp_{L\tau}\bigl((\tilde v_0 \tau + \tilde v_1)/N\bigr)$, where $\tilde v_i$ is the representative of $v_i$ in $[0,N)$; let $\mathrm{fricke}_v(\tau) = -\bigl(E_4(\tau)E_6(\tau)/\Delta(\tau)\bigr)/2592 \cdot W_v(\tau)$, and let $jf(\tau) = E_4(\tau)^3/\Delta(\tau)$, each pinned to these formulas by hypothesis. Put $A_N$ for the $\mathbb{C}$-subalgebra of $\mathbb{H} \to \mathbb{C}$ generated by $jf$ together with all $\mathrm{fricke}_v$ with $v \neq 0$, and let $\gamma \in \mathrm{SL}_2(\mathbb{Z})$ act on row vectors $v$ by $v \mapsto v\bar\gamma$, reduction mod $N$. Six assertions are made. First, the set of $\gamma$ with $\mathrm{fricke}_{v\bar\gamma} = \mathrm{fricke}_v$ for all $v \neq 0$ is exactly $\{\gamma : \gamma \in \Gamma(N) \text{ or } -\gamma \in \Gamma(N)\}$. Second, if $a, b \in A_N$, $b \neq 0$, and $a \cdot (b \circ \gamma) = (a \circ \gamma) \cdot b$ for every $\gamma$, then there are polynomials $p, q$ over $\mathbb{C}$ with $q \neq 0$ and $a \cdot q(jf) = b \cdot p(jf)$. Third, each $\mathrm{fricke}_v$ with $v \neq 0$ satisfies a monic equation of some degree $d$ with coefficients polynomial in $jf$. Fourth, any polynomial vanishing at $jf(\tau)$ for all $\tau$ is zero. Fifth, every element of $A_N$ is holomorphic on $\mathbb{H}$. Sixth, $A_N$ has no zero divisors.
This is the function-level form of the classical structure theory of the field of modular functions of level $N$ over $\mathbb{C}$: the Fricke functions are permuted by $\mathrm{SL}_2(\mathbb{Z})$ through $\mathrm{SL}_2(\mathbb{Z})/\pm\Gamma(N)$, their invariant fractions are rational in $j$, and the algebra they generate is a holomorphic integral domain, integral over $\mathbb{C}[j]$ with $j$ transcendental. It supports the later rationality and $q$-expansion statements for forms of level $N$, such as the description of the span of Fricke-rational products of $E_4$ and $E_6$ and the construction of algebra homomorphisms into Laurent series.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_WLight_levelN_structure_package.lean
<!-- Generated by add_prove2me_provenance.py -->