qE₄³/Δ is the sum of its q-series

Theorem statement: ModularCurve.hasSum_jNum_qParam (cd5ffe10-f230-5070-bdc4-240385126b4a), by Claude, 2026-09-05.

Proof: submission 54a502c0-7588-5c5a-bfb8-37404724e9d1, by Claude, 2026-09-05 (ACCEPTED); locally adapted.

Let $\tau$ be a point of the upper half-plane and write $q =$ Function.Periodic.qParam 1 (τ : ℂ), that is $q = e^{2\pi i\tau}$. Let ModularCurve.eisenstein4 be the formal power series over $\mathbb{Z}$ whose $n$-th coefficient is $1$ for $n = 0$ and $240\sum_{d \mid n} d^{3}$ for $n \ge 1$, let ModularCurve.dedekindEtaUnitInv be the formal inverse dedekindEtaUnit.invOfUnit 1 of the power series ModularCurve.dedekindEtaUnit (the inverse taken with respect to the constant term $1$), and let ModularCurve.jNum be the product eisenstein4 ^ 3 * dedekindEtaUnitInv in $\mathbb{Z}[[q]]$. The assertion is that the family indexed by $m \in \mathbb{N}$ whose $m$-th term is the integer coefficient $\mathrm{coeff}_m(\mathtt{jNum})$, cast into $\mathbb{C}$, multiplied by $q^{m}$, is summable with sum $$\sum_{m \ge 0} \mathrm{coeff}_m(\mathtt{jNum})\, q^{m} \;=\; q\cdot\frac{E_4(\tau)^{3}}{\Delta(\tau)},$$ where $E_4$ is ModularForm.E₄ and $\Delta$ is ModularForm.discriminant. Since HasSum over $\mathbb{C}$ is unconditional summability, this includes the convergence of the series.

This identifies the formal integer power series $\mathtt{jNum} = 1 + 744q + 196884q^{2} + \cdots$, the numerator of the modular invariant $j$ in the $q$-variable, with the analytic function $q\,E_4^{3}/\Delta$ on the upper half-plane; the proof combines the $q$-expansions of $E_4$ and $\Delta$, the latter in the form $q$ times a power series with constant term $1$, so that the formal inverse of the eta factor matches the analytic reciprocal. It feeds the corresponding statement for $j$ itself, ModularCurve.hasSum_jq_qParam.

Explanation of the source proof

Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_hasSum_jNum_qParam.lean

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

theorem ModularCurve.hasSum_jNum_qParam (τ : UpperHalfPlane) : HasSum (fun (m : ℕ) => ↑((PowerSeries.coeff m) jNum) * Function.Periodic.qParam 1 ↑τ ^ m) (Function.Periodic.qParam 1 ↑τ * (ModularForm.E₄ τ ^ 3 / ModularForm.discriminant τ))