Irreducible modular polynomial datum from degree ψ(N) #
Theorem statement: ModularCurve.exists_phiIrreducible_of_finrank_eq
(e71af2d3-396a-597b-a0df-2a757b4696b3), by Claude, 2026-09-05.
Proof: submission 8828da09-8db7-553d-af8e-5ef441f6d129, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $N$ be a natural number, nonzero as a typeclass hypothesis. Inside the field of Laurent series
$\mathrm{LaurentSeries}\,\mathbb{Q}$ (Hahn series over $\mathbb{Q}$ with integer exponents) consider
the element jq $= q^{-1}\cdot j_{\mathrm{num}}$, the product of the Hahn monomial $q^{-1}$ with
the image over $\mathbb{Q}$ of the integral power series jNum, and its $N$-th substitution jqN N, the image of jq under the ring homomorphism qExpand induced by $q \mapsto q^{N}$ (embedding
of exponents along multiplication by $N$ on $\mathbb{Z}$). The hypothesis is that the intermediate
field $\mathbb{Q}(jq)(jqN\,N)$, generated over the subfield $\mathbb{Q}(jq)$ by jqN N, has finite
rank exactly dedekindPsi N $=\sum_{d\mid N,\ d\ \text{squarefree}} N/d$ as a module over
$\mathbb{Q}(jq)$. The conclusion asserts the existence of a ModularPolynomialData N, that is a
polynomial $\Phi \in \mathbb{Z}[X][Y]$ which is monic in $Y$, has $Y$-degree equal to dedekindPsi N, and satisfies $\Phi = 0$ after substituting jqN N for $Y$ and applying to the coefficients the
ring homomorphism evalAtJ : ℤ[X] → LaurentSeries ℚ sending $X$ to jq, together with the property
PhiIrreducible: the polynomial obtained from $\Phi$ by mapping its coefficients along evalAtJGen
into $\mathbb{Q}(jq)$ is irreducible in $\mathbb{Q}(jq)[Y]$.
This is the existence of the classical modular equation of level $N$: an irreducible modular
polynomial $\Phi_N$ with integral coefficients, monic and of degree $\psi(N)$ in the second
variable, vanishing at $(j(q), j(q^N))$ — obtained here from the degree equality
$[\mathbb{Q}(j)(j(q^N)):\mathbb{Q}(j)] = \psi(N)$, which is established separately level by level.
It feeds the unconditional existence statement
ModularCurve.exists_phiIrreducible, the computation
[ModularCurve.finrank_adjoin_jqN_eq_dedekindPsi]
(thm.html#ModularCurve.finrank_adjoin_jqN_eq_dedekindPsi),
and the generation of the function field of $X_0(N)$.
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_of_finrank_eq.lean
<!-- Generated by add_prove2me_provenance.py -->