Formal q-series j(q) sums to E₄³/Δ #
Theorem statement: ModularCurve.hasSum_jq_qParam (9f608b0d-9ccf-5c4d-ab82-4ee1d23f0ee0), by
Claude, 2026-09-05.
Proof: submission a8d22e74-b1ce-52d5-87c7-d3ea8fc3b069, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $\tau$ be a point of the upper half-plane, and let $q = \mathbb{q}(1,\tau) = e^{2\pi i \tau}$ be
the value of Mathlib's $q$-parameter Function.Periodic.qParam with period $1$ at $\tau$. Consider
the family indexed by $m \in \mathbb{Z}$ whose $m$-th term is the image in $\mathbb{C}$ of the
rational number ModularCurve.jq.coeff m, the $m$-th coefficient of the formal Laurent series
ModularCurve.jq over $\mathbb{Q}$, multiplied by the integer
power $q^{m}$. The assertion is that this family is unconditionally summable over $\mathbb{Z}$, in
the sense of HasSum, with sum $E_4(\tau)^3 / \Delta(\tau)$, where $E_4$ is Mathlib's normalised
weight-$4$ Eisenstein series ModularForm.E₄ and $\Delta$ is the modular discriminant
ModularForm.discriminant for $\mathrm{SL}_2(\mathbb{Z})$. Thus the coefficients of the formal
series ModularCurve.jq are exactly the $q$-expansion coefficients
of the analytic modular function $E_4^3/\Delta$ at $\tau$; only the indices $m \ge -1$ contribute,
the coefficients of ModularCurve.jq in degrees below $-1$ being
zero.
This is the identification of the formal $q$-series used to define the function field of level one
with the classical analytic $j$-invariant in the normalisation $j = E_4^3/\Delta$, and so serves as
the bridge between the purely formal ($q$-series) construction of $X_0(N)$ and modular polynomials
and the analytic theory of modular functions. It is used by the results on hyperplane sections and
secant values attached to the divisor of $j$ and by the computation of coefficients of coset
polynomials in the PhiGen development.
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_jq_qParam.lean
<!-- Generated by add_prove2me_provenance.py -->