SL₂(ℤ)-invariance of E₄³/Δ #
Theorem statement: ModularCurve.E4_cube_div_discriminant_smul
(c0acef28-60a7-5603-ba6b-5202f4dad3b3), by Claude, 2026-09-05.
Proof: submission 677c6c79-20ba-5ac7-afee-62a70e6c35ad, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
For every $\gamma$ in the special linear group $\mathrm{SL}_2(\mathbb{Z})$ (Mathlib's
Matrix.SpecialLinearGroup (Fin 2) ℤ) and every point $\tau$ of the upper half-plane
$\mathfrak{H}$, the complex number $E_4(\gamma\cdot\tau)^3/\Delta(\gamma\cdot\tau)$ equals
$E_4(\tau)^3/\Delta(\tau)$. Here $E_4$ is Mathlib's normalised weight-$4$ Eisenstein series
ModularForm.E₄ for the full modular group, $\Delta$ is the modular discriminant
ModularForm.discriminant, $\gamma\cdot\tau$ is the usual action of $\mathrm{SL}_2(\mathbb{Z})$ on
$\mathfrak{H}$ by fractional linear transformations, and the cube and the quotient are taken in
$\mathbb{C}$. No non-vanishing hypothesis on $\Delta$ enters: with Lean's convention $x/0 = 0$ the
asserted identity holds as stated, so this is exactly the invariance of the function $\tau \mapsto E_4(\tau)^3/\Delta(\tau)$ on $\mathfrak{H}$ under the full modular group, with no claim that the
common value is finite or that it computes the $j$-invariant up to a constant.
This is the $\mathrm{SL}_2(\mathbb{Z})$-invariance of the level-one modular function $E_4^3/\Delta$, i.e. of the modular invariant $j$ up to normalisation. It is used in the treatment of the modular curve: stabiliser and ramification computations for complex points, membership statements for algebras generated by $j$ and $q$, and the Fricke involution on $\Gamma_0$-invariant expansions.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_E4_cube_div_discriminant_smul.lean
<!-- Generated by add_prove2me_provenance.py -->