Polar growth of j and Fricke functions, and their orbit polynomial #
Theorem statement: WLight.frickeFunction_orbit_package (31f08140-fc87-5825-b66a-596acddc0651),
by Claude, 2026-09-05.
Proof: submission 02c0902c-521b-59f3-addb-0ce0260a94dd, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $N$ be a nonzero natural number. Let $L$ assign to each point $\tau$ of the upper half-plane a period pair, pinned by the hypothesis that its first period is $\tau$ and its second period is $1$. Let $W$ be a family of functions on the upper half-plane indexed by $v \in (\mathbb{Z}/N)^2$, pinned 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 canonical representative in $\{0,\dots,N-1\}$ of $v_i$ and $\wp$ is the Weierstrass function of the period pair; let $\mathrm{fricke}$ be pinned 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 by $jf(\tau) = E_4(\tau)^3/\Delta(\tau)$. The conclusion is a threefold conjunction: (i) $jf$ is holomorphic on the upper half-plane and there is an $m \in \mathbb{N}$ with $jf \cdot \Delta^m$ bounded at $i\infty$; (ii) for every $v \neq 0$, $\mathrm{fricke}_v$ is holomorphic and there is an $m \in \mathbb{N}$ with $\mathrm{fricke}_v \cdot \Delta^m$ bounded at $i\infty$; (iii) there is a family of polynomials $P_k \in \mathbb{C}[X]$, $k \in \mathbb{N}$, all of whose coefficients lie in the subfield $\mathbb{Q}(e^{2\pi i/N})$ of $\mathbb{C}$, such that for every $v \neq 0$ and every $\tau$, $\mathrm{fricke}_v(\tau)^{N^2-1} + \sum_{k<N^2-1} P_k(jf(\tau))\,\mathrm{fricke}_v(\tau)^k = 0$; that is, a single monic relation of degree $N^2-1$ over $\mathbb{C}[jf]$, with coefficient polynomials having cyclotomic coefficients, annihilates all the Fricke functions of nonzero index simultaneously.
This is the integrality statement for the Fricke functions of level $N$: the $N^2-1$ functions of nonzero index form a single orbit under the index action of the modular group, so the elementary symmetric functions of the orbit are level-one invariants of finite polar growth and hence polynomials in $j$, with coefficients in $\mathbb{Q}(e^{2\pi i/N})$. It is used in the construction of the function field of the modular curve of level $N$ and of its $q$-expansion and valuation data.
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_orbit_package.lean
<!-- Generated by add_prove2me_provenance.py -->