Fricke functions of level N: transformation and rationality package #
Theorem statement: WLight.frickeFunction_modularity_package
(409f428b-f096-5e14-b476-e6f5efd41901), by Claude, 2026-09-05.
Proof: submission afdcfca9-10d0-572b-870d-1902e69fc5ee, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $N$ be a natural number, nonzero as an instance, and let $L:\mathbb{H}\to$ PeriodPair assign
to each $\tau$ a period pair with, by hypothesis, $\omega_1=\tau$ and $\omega_2=1$. For
$a=(a_0,a_1)\in(\mathbb{Z}/N)^2$ put
$f_a(\tau)=-\bigl(E_4(\tau)E_6(\tau)/\Delta(\tau)\bigr)/2592\cdot(2\pi i)^{-2}\,\wp_{L(\tau)}\bigl((\tilde a_0\tau+\tilde a_1)/N\bigr)$, where $\tilde a_i$ denotes the
canonical representative in $[0,N)$. Eight assertions are conjoined. (1) For all $a$, all
$\gamma\in\mathrm{SL}_2(\mathbb{Z})$ and all $\tau$, $f_a(\gamma\cdot\tau)=f_{a\bar\gamma}(\tau)$,
with $a\bar\gamma$ the row vector $a$ multiplied on the right by the entrywise reduction of $\gamma$
modulo $N$. (2) $f_{-a}=f_a$ for all $a$. (3) For $a\neq0$, $f_a$ is holomorphic on $\mathbb{H}$.
(4) For $a\neq0$, $f_a\cdot\Delta$ is bounded at $i\infty$. (5) For $a\neq0$, $f_a\cdot\Delta$
transported along ofComplex is periodic with period $N$, and every coefficient of its width-$N$
$q$-expansion lies in the subfield $\mathbb{Q}(e^{2\pi i/N})$ of $\mathbb{C}$. (6) For $a,b\neq0$,
$f_a=f_b$ forces $b=a$ or $b=-a$. (7) For all $a$, $f_a(\gamma\cdot\tau)=f_a(\tau)$ for $\gamma$ in
the principal congruence subgroup of level $N$. (8) If $s$ is coprime to $N$ and
$\varphi:\mathbb{Q}(e^{2\pi i/N})\to\mathbb{C}$ is a ring homomorphism sending any element with
complex value $e^{2\pi i/N}$ to $e^{2\pi i s/N}$, then for $a\neq0$ and each $n$, applying $\varphi$
to an element of the field whose complex value is the $n$-th $q$-expansion coefficient of
$f_a\cdot\Delta$ yields the $n$-th coefficient of the $q$-expansion of
$f_{(a_0,\,s\,a_1)}\cdot\Delta$.
This is the transformation and rationality theory of the Fricke functions of level $N$, the normalised values of $\wp$ at $N$-division points: their $\mathrm{SL}_2(\mathbb{Z})$-equivariance, evenness, injectivity up to sign, $\Gamma(N)$-invariance, cyclotomic width-$N$ expansions and the Galois conjugation of those expansions. It is the source of rational generators of the level-$N$ modular function field used in the construction of $\Gamma_1$-level cusp forms with prescribed coefficient fields and Galois behaviour.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_WLight_frickeFunction_modularity_package.lean
<!-- Generated by add_prove2me_provenance.py -->