Existence of an irreducible symmetric modular polynomial Φ_ℓ #
Theorem statement: ModularCurve.exists_phiIrreducible_evalSymm
(66befd22-55d2-533d-a261-ddb7399e4802), by Claude, 2026-09-05.
Proof: submission d69154cc-2187-5d53-8545-df3b03f29595, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $\ell$ be a prime. The assertion is that there exists a term data of the structure
ModularPolynomialData ℓ, that is, a polynomial $\Phi =$ data.Φ in $(\mathbb{Z}[X])[Y]$ which is
monic, whose degree in $Y$ equals dedekindPsi ℓ, the sum of $\ell/d$ over the squarefree divisors
$d$ of $\ell$ (so $\ell+1$), and which satisfies $\Phi.\mathrm{eval}_2(\mathrm{evalAtJ}, \mathrm{jqN}\ \ell) = 0$, where evalAtJ is the ring homomorphism $\mathbb{Z}[X] \to$
LaurentSeries ℚ evaluating a coefficient polynomial at the Laurent series jq, and jqN ℓ is the
Laurent series of that name; and such that this same packet has both of the following two
properties. First, PhiIrreducible data: the polynomial data.toAdjoin, obtained from $\Phi$ by
mapping its coefficients through evalAtJGen into the intermediate field
$\mathbb{Q}\langle\mathrm{jq}\rangle$ generated by jq, is irreducible over that field. Second,
EvalSymm data.Φ: for all Laurent series $x, y$ over $\mathbb{Q}$, evaluating $\Phi$ by
substituting $x$ into the coefficient polynomials and $y$ into the outer variable gives the same
result as substituting $y$ into the coefficients and $x$ into the outer variable.
This is the existence, for each prime $\ell$, of the classical modular polynomial $\Phi_\ell(X,Y)$
relating $j(q)$ and $j(q^\ell)$, in the strong form in which irreducibility over $\mathbb{Q}(j)$ and
the symmetry $\Phi_\ell(X,Y)=\Phi_\ell(Y,X)$ hold for one and the same packet; the pair of
properties is what pins the packet down. It feeds the uniqueness statement
[ModularCurve.ModularPolynomialData.eq_of_prime]
(thm.html#ModularCurve.ModularPolynomialData.eq_of_prime),
the construction of the Fricke involution
ModularCurve.exists_isFrickeAut, and the existence of
a monic relation
[ModularCurve.exists_monic_evalAtJ_jqN_eq_zero]
(thm.html#ModularCurve.exists_monic_evalAtJ_jqN_eq_zero).
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_exists_phiIrreducible_evalSymm.lean
<!-- Generated by add_prove2me_provenance.py -->