Prime-level splitting of Φₚ at the slot uq^e #
Theorem statement: ModularCurve.PhiGen.splits_prime_at_slot_of_isPrimitiveRoot
(d9095e24-91b1-5043-93c5-196e9d87e5b0), by Claude, 2026-09-05.
Proof: submission c2b3fefc-b92f-55d4-bef5-c549467bd7d4, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $K$ be a field, $p$ a prime, and $\zeta \in K^\times$ a unit whose image in $K$ is a primitive
$p$-th root of unity (so $K$ has characteristic $\neq p$). Let data be a level-$p$ modular
polynomial datum: a polynomial $\Phi \in \mathbb{Z}[X][Y]$, monic, of degree $\sum_{d \mid p,\ d \text{ squarefree}} p/d = p+1$ in $Y$, satisfying $\Phi(j(q), j(q^p)) = 0$ in $\mathbb{Q}((q))$,
where $j$ denotes the formal $q$-expansion jq and the inner variable is evaluated at $j(q)$. Let
$e$ be a nonzero natural number and $u \in K^\times$. Write $j_K = q^{-1}\cdot(\text{image of } E_4^3/\text{(eta factor)})$ for the $j$-expansion jqModC K over $K$, and for a unit $v$ and
nonzero $N$ let $v, N$ act on $K((q))$ by the ring homomorphisms qTwist ($q \mapsto vq$, i.e. the
$k$-th coefficient is multiplied by $v^k$) and qExpand ($q \mapsto q^N$). Then, in $K((q))[Y]$,
specialising the integer coefficients of $\Phi$ into $K((q))$ and its inner variable at $j_K(u^p q^{pe})$ yields $$\Phi\bigl(j_K(u^pq^{pe}), Y\bigr) = \bigl(Y - j_K(u^{p^2}q^{p^2e})\bigr)\prod_{b=0}^{p-1}\bigl(Y - j_K(u\zeta^b q^{e})\bigr).$$
This is the classical factorisation of the level-$p$ modular polynomial, $\Phi_p(j(p\tau), Y) = (Y - j(p^2\tau))\prod_{b<p}(Y - j((\tau+b)/p))$, in the formal $q$-expansion model over an arbitrary field containing a primitive $p$-th root of unity, and stated at an arbitrary slot $s = uq^e$ rather than only at $s = q$. It supplies the list of the $p+1$ expansions lying above a given conjugate one step up a tower of $q$-expansion fields, and is used in the construction of monic factorisations of $\Phi$ over such fields, in the proof that $j(q^{dp})$ lies in the relevant modular function field, and in the chart computations on $X_1(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_PhiGen_splits_prime_at_slot_of_isPrimitiveRoot.lean
<!-- Generated by add_prove2me_provenance.py -->