Uniqueness of prime-level modular polynomial data #
Theorem statement: ModularCurve.ModularPolynomialData.eq_of_prime
(8104e31e-e7e5-576b-83ff-95b68463f328), by Claude, 2026-09-05.
Proof: submission f0162e94-64db-5958-bc3d-e85754b88568, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $p$ be a prime. A term of the structure ModularPolynomialData p consists of a polynomial $\Phi \in (\mathbb{Z}[Y])[X]$ together with three properties: $\Phi$ is monic (in $X$), its $X$-degree
equals dedekindPsi p, defined as $\sum_{d \mid p,\ d \text{ squarefree}} p/d$, and $\Phi$ vanishes
when its coefficients in $\mathbb{Z}[Y]$ are mapped into the Laurent series field $\mathbb{Q}((q))$
by the ring homomorphism evalAtJ, namely evaluation at the Laurent series jq, and $X$ is set
equal to jqN p; here jq and jqN p are the $q$-expansion models of the modular function $j$ and
of $j$ at $q^p$. The theorem asserts that for any two such terms $d$ and $d'$ one has $d = d'$: the
data at prime level are unique, hence in particular their underlying polynomials $\Phi$ agree. No
further hypotheses are imposed.
This is the uniqueness half of the statement that the classical modular polynomial $\Phi_p(X,Y)$ is
pinned down, at prime level, by being monic of $X$-degree $\psi(p)$ with $\Phi_p(j(q^p), j(q)) = 0$.
It is used to transfer properties established for one particular construction of the level-$p$
modular polynomial (irreducibility over $\mathbb{Q}(j)$, symmetry of the two variables, separability
of the reduction) to an arbitrary term of ModularPolynomialData p, and in the analysis of the
fibres of the associated curve in characteristic $p$.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_ModularPolynomialData_eq_of_prime.lean
<!-- Generated by add_prove2me_provenance.py -->