Integrality descent for polynomials in j #
Theorem statement: ModularCurve.PhiGen.aeval_jq_intCoeffs_descent
(20bc4d07-b455-5870-b4a2-a361286e6d87), by Claude, 2026-09-05.
Proof: submission 14f64e6b-3442-5798-ab13-6cb394637d5a, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $P \in \mathbb{Q}[X]$ and let jq denote the Laurent series over $\mathbb{Q}$ given by $q^{-1}$
times the image under $\mathbb{Z} \to \mathbb{Q}$ of the integral power series jNum; that is, jq
is the product of the Hahn series HahnSeries.single (-1) 1 with the Laurent series attached to
jNumQ. Suppose that IntCoeffs holds for the evaluation of $P$ at jq inside the
$\mathbb{Q}$-algebra of Laurent series, i.e. for every integer $m$ the coefficient of $q^m$ in
$P(\mathrm{jq})$ lies in the image of $\mathbb{Z} \to \mathbb{Q}$: there is $z \in \mathbb{Z}$ with
that coefficient equal to $(z : \mathbb{Q})$. Then for every natural number $k$ there exists $z \in \mathbb{Z}$ with $P.\mathrm{coeff}\ k = (z : \mathbb{Q})$, i.e. every coefficient of $P$ is a
rational integer. The conclusion is stated coefficientwise for a single but arbitrary index $k$,
rather than as membership of $P$ in $\mathbb{Z}[X]$.
This is the standard integrality descent for the $q$-expansion principle applied to the
$j$-invariant: since $q\,\mathrm{jq}$ is an integral power series with constant term $1$, the
passage from $P$ to the $q$-expansion of $P(j)$ is unitriangular with respect to the degree
filtration, so integrality of the expansion forces integrality of the coefficients. It is used in
the construction of the integral modular polynomial data for $\Phi_\ell$, being cited by
[ModularCurve.PhiGen.exists_modularPolynomialData_coeff_eq]
(thm.html#ModularCurve.PhiGen.exists_modularPolynomialData_coeff_eq)
and by ModularCurve.kroneckerPairIntegral.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_PhiGen_aeval_jq_intCoeffs_descent.lean
<!-- Generated by add_prove2me_provenance.py -->