Regularity, rationality and Galois transport for wp at torsion #
Theorem statement: ModularForm.weierstrassP_torsion_qExpansion_package
(91566695-d863-5200-bb1e-36b065994f44), by Claude, 2026-09-05.
Proof: submission 220b9575-68c5-5d5c-af1c-4a6cb65111f4, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Fix $N\in\mathbb{N}$ with $N\neq 0$ and a map $L\colon\mathbb{H}\to\mathrm{PeriodPair}$ whose
periods are $(L\,\tau).\omega_1=\tau$ and $(L\,\tau).\omega_2=1$ for every $\tau$. Put
$\zeta=e^{2\pi i/N}\in\mathbb{C}$, let $k=\mathbb{Q}(\zeta)$ be the intermediate field of
$\mathbb{C}/\mathbb{Q}$ generated by $\zeta$ with $\zeta_k\in k$ the adjoined generator, and set
$W_{a_1,a_2}(\tau)=(2\pi i)^{-2}\,\wp_{L\,\tau}\bigl((a_1\tau+a_2)/N\bigr)$ for
$a_1,a_2\in\mathbb{N}$. The conclusion is a sevenfold conjunction. First, for all $a_1,a_2<N$ not
both zero, $W_{a_1,a_2}$ is holomorphic on $\mathbb{H}$ (differentiable as a map of complex
manifolds), its extension along UpperHalfPlane.ofComplex is periodic with period $N$, it is
bounded at $i\infty$, and every coefficient of its width-$N$ $q$-expansion qExpansion N lies in
$k$. Secondly, for nonzero $(a_1,a_2),(b_1,b_2)\in[0,N)^2$, equality $W_{a_1,a_2}=W_{b_1,b_2}$ of
functions on $\mathbb{H}$ forces $(b_1,b_2)=(a_1,a_2)$ or $(b_1,b_2)=((N-a_1)\bmod N,(N-a_2)\bmod N)$. Thirdly, there is $S\colon\mathbb{N}\to\mathbb{N}\to k[\![q]\!]$ with $S_{a_1,a_2}$ pushed
forward along $k\hookrightarrow\mathbb{C}$ equal to qExpansion N (W a₁ a₂) for all such
$(a_1,a_2)$, and such that for every $s$ coprime to $N$ and every ring homomorphism $\varphi\colon k\to\mathbb{C}$ with $\varphi(\zeta_k)=\zeta^s$ one has $\varphi_*S_{a_1,a_2}=$ qExpansion N (W a₁ (s * a₂ % N)) — the transport fixes $a_1$ and multiplies $a_2$ by $s$ modulo $N$. Fourthly, a
width-change lemma: for any $f\colon\mathbb{H}\to\mathbb{C}$ which is holomorphic, bounded at
$i\infty$ and $1$-periodic after composition with UpperHalfPlane.ofComplex, the $n$-th coefficient
of qExpansion N f equals the $(n/N)$-th coefficient of qExpansion 1 f when $N\mid n$ and
vanishes otherwise. The last three assertions state that all coefficients of the width-$1$
$q$-expansions of ModularForm.E₄, ModularForm.E₆ and ModularForm.discriminant are rational
numbers.
Up to the normalisation by $E_4E_6/\Delta$, the functions $W_{a_1,a_2}$ are the Fricke functions
attached to the $N$-torsion of the analytic family $\mathbb{C}/(\mathbb{Z}\tau+\mathbb{Z})$, and the
four parts record their holomorphy and boundedness, the $\mathbb{Q}(\zeta_N)$-rationality of their
$q_N$-expansions, their separation up to negation of the index, and the effect of
$\mathrm{Gal}(\mathbb{Q}(\zeta_N)/\mathbb{Q})$ on these expansions, together with the comparison of
$q_N$- and $q$-expansions and the rationality of the coefficients of $E_4$, $E_6$ and $\Delta$. It
is the analytic input used by
WLight.frickeFunction_modularity_package and
WLight.frickeFunction_orbit_package towards the
field of modular functions of level $N$.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularForm_weierstrassP_torsion_qExpansion_package.lean
<!-- Generated by add_prove2me_provenance.py -->