Level-N modular functions as fractions over ℂ[j,fᵥ]

Theorem statement: WLight.exists_levelFraction_of_stable_family (490607a5-50bf-5b84-bea7-42d3fd2f1404), by Claude, 2026-09-05.

Proof: submission 786cc53b-f5ea-5b92-be39-5aab5f10fc60, by Claude, 2026-09-05 (ACCEPTED); locally adapted.

Let $N$ be a positive natural number. Fix a family of period pairs $L : \mathbb{H} \to \mathtt{PeriodPair}$ normalised by $\omega_1(L\tau) = \tau$ and $\omega_2(L\tau) = 1$ for all $\tau$; a family $W$ indexed by $v \in (\mathbb{Z}/N)^2$ with $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 lift of $v_i$ to $\mathbb{Z}$; a family $\mathtt{fricke}$ with $\mathtt{fricke}_v(\tau) = -\big(E_4(\tau)E_6(\tau)/\Delta(\tau)\big)/2592 \cdot W_v(\tau)$; and a function $jf$ with $jf(\tau) = E_4(\tau)^3/\Delta(\tau)$. Let $S$ be a set of functions $\mathbb{H} \to \mathbb{C}$ such that every $G \in S$ is holomorphic (differentiable as a map of complex manifolds), every $G \in S$ satisfies $G \cdot \Delta^m$ bounded at $i\infty$ for some $m \in \mathbb{N}$, $S$ is closed under precomposition with the action of each $\gamma \in \mathrm{SL}_2(\mathbb{Z})$ on $\mathbb{H}$, and every $G \in S$ satisfies $G(\gamma\tau) = G(\tau)$ for all $\gamma$ in the principal congruence subgroup of level $N$ and all $\tau$. Then for every $F \in S$ there exist $a, b : \mathbb{H} \to \mathbb{C}$, both lying in the $\mathbb{C}$-subalgebra of functions generated by $jf$ together with the functions $\mathtt{fricke}_v$ for $v \neq 0$, with $b$ not the zero function and $F \cdot b = a$.

This is the function-level form of the classical statement that every modular function of level $N$ is a rational function of $j$ and the Fricke functions $f_v$: the conclusion is a single fraction identity $F \cdot b = a$ with numerator and denominator in the polynomial algebra $\mathbb{C}[j, f_v : v \neq 0]$, no field of fractions being formed, and $b \neq 0$ only as a function (it may vanish at isolated points). It feeds the rationality statements for $q$-expansion coefficients of forms on $\Gamma_1(N)$ and the spanning results for Fricke-rational combinations of $E_4$ and $E_6$ powers.

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_levelFraction_of_stable_family.lean

<!-- Generated by add_prove2me_provenance.py -->

theorem WLight.exists_levelFraction_of_stable_family (N : ℕ) [NeZero N] (L : UpperHalfPlane → PeriodPair) (hL : ∀ (τ : UpperHalfPlane), (L τ).ω₁ = ↑τ ∧ (L τ).ω₂ = 1) (W : (Fin 2 → ZMod N) → UpperHalfPlane → ℂ) (hW : ∀ (v : Fin 2 → ZMod N) (τ : UpperHalfPlane), W v τ = ((2 * ↑Real.pi * Complex.I) ^ 2)⁻¹ * (L τ).weierstrassP ((↑(v 0).val * ↑τ + ↑(v 1).val) / ↑N)) (fricke : (Fin 2 → ZMod N) → UpperHalfPlane → ℂ) (hfricke : ∀ (v : Fin 2 → ZMod N) (τ : UpperHalfPlane), fricke v τ = -(ModularForm.E₄ τ * ModularForm.E₆ τ / ModularForm.discriminant τ) / 2592 * W v τ) (jf : UpperHalfPlane → ℂ) (hjf : ∀ (τ : UpperHalfPlane), jf τ = ModularForm.E₄ τ ^ 3 / ModularForm.discriminant τ) (S : Set (UpperHalfPlane → ℂ)) (hhol : ∀ G ∈ S, MDiff G) (hpb : ∀ G ∈ S, ∃ (m : ℕ), UpperHalfPlane.IsBoundedAtImInfty (G * ModularForm.discriminant ^ m)) (hst : ∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ), ∀ G ∈ S, (G ∘ fun (x : UpperHalfPlane) => γ • x) ∈ S) (hinv : ∀ G ∈ S, ∀ γ ∈ CongruenceSubgroup.Gamma N, ∀ (τ : UpperHalfPlane), G (γ • τ) = G τ) {F : UpperHalfPlane → ℂ} (hF : F ∈ S) : ∃ (a : UpperHalfPlane → ℂ) (b : UpperHalfPlane → ℂ), a ∈ Algebra.adjoin ℂ (insert jf {g : UpperHalfPlane → ℂ | ∃ (v : Fin 2 → ZMod N), v ≠ 0 ∧ g = fricke v}) ∧ b ∈ Algebra.adjoin ℂ (insert jf {g : UpperHalfPlane → ℂ | ∃ (v : Fin 2 → ZMod N), v ≠ 0 ∧ g = fricke v}) ∧ b ≠ 0 ∧ F * b = a