Unit leading coefficient of Φ_N(X,X) for non-square N #
Theorem statement: ModularCurve.ModularPolynomialData.isUnit_leadingCoeff_diag_of_not_isSquare
(4bb1346a-3137-5367-bd86-316bfef9d9ed), by Claude, 2026-09-05.
Proof: submission 275c90a1-2f8f-5135-bc89-8293fe48778f, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $N$ be a natural number with $N \neq 0$ which is not a square (no $r$ with $N = r\cdot r$), and
let data be an element of ModularCurve.ModularPolynomialData N,
that is: a polynomial $\Phi =$ data.Φ in $(\mathbb{Z}[X])[Y]$ together with the three properties
recorded in that structure — $\Phi$ is monic in $Y$; its degree in $Y$ equals dedekindPsi N,
defined as $\sum_{d \mid N,\ d \text{ squarefree}} N/d$; and $\Phi$ annihilates the pair consisting
of the $q$-expansion of $j$ and that of $j(q^N)$, in the sense that evaluating $\Phi$ at $Y =$ jqN N with coefficients mapped by the ring homomorphism evalAtJ $\colon \mathbb{Z}[X] \to$
LaurentSeries ℚ sending $X$ to jq gives $0$. The assertion is that the diagonal specialisation
obtained by substituting $Y \mapsto X$ while leaving the coefficient ring $\mathbb{Z}[X]$ untouched,
namely $\Phi(X,X) \in \mathbb{Z}[X]$, has leading coefficient a unit of $\mathbb{Z}$, i.e. $\pm 1$;
in particular $\Phi(X,X)$ is not the zero polynomial.
This is the integrality statement underlying Kronecker's congruence: the diagonal of the modular
polynomial of non-square level has unimodular leading term, the non-square hypothesis excluding the
tie between the Hermite slots with $a = d$ (and the degenerate level $N=1$, where $\Phi_1(X,X) = 0$). It is used in the derivation of the corresponding statement for isUnit_leadingCoeff_diag, and
in the Weierstrass-curve lemmas separating $j$-invariants of an elliptic curve and of its quotient
by a cyclic isogeny, respectively producing a reduction with prescribed behaviour over an
algebraically closed residue field.
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_isUnit_leadingCoeff_diag_of_not_isSquare.lean
<!-- Generated by add_prove2me_provenance.py -->