Minimal polynomial of j(q^M) splits into primitive slots #
Theorem statement: ModularCurve.minpoly_jqN_map_eq_prod_slots
(e6bb2acf-c314-5521-a8c2-8258a3b50945), by Claude, 2026-09-05.
Proof: submission 389417d8-53e1-5b13-be85-971b8519de5b, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $K$ be a field equipped with a $\mathbb{Q}$-algebra structure, let $M$ be a natural number with $M \neq 0$, and let $\zeta \in K^{\times}$ be a unit whose underlying element of $K$ is a primitive $M$-th root of unity. Assume the following package at every divisor $d$ of $M$ (with $d \neq 0$): the degree of $\mathbb{Q}(jq)\bigl(jqN\,d\bigr)$ over $\mathbb{Q}(jq)$ equals $\mathrm{dedekindPsi}\,d = \sum_{e \mid d,\ e \text{ squarefree}} d/e$, and $\mathbb{Q}\bigl(jq,\ \mathrm{qExpand}_{\mathbb{Q}}\,d\,jq\bigr)$ coincides with the subfield of $\mathbb{Q}((q))$ generated over $\mathbb{Q}$ by all $\mathrm{qExpand}_{\mathbb{Q}}\,e\,jq$ with $e \mid d$, $e \neq 0$. Here $jq = q^{-1}\cdot jNumQ$ is the $j$-expansion in $\mathbb{Q}((q))$, $\mathrm{qExpand}_R\,n$ is the exponent-scaling ring map $q \mapsto q^{n}$ on Laurent series, and $jqN\,n = \mathrm{qExpand}_{\mathbb{Q}}\,n\,jq$. Then the minimal polynomial of $jqN\,M$ over the intermediate field $\mathbb{Q}(jq)$, with its coefficients transported by the ring map given by the inclusion $\mathbb{Q}(jq) \hookrightarrow \mathbb{Q}((q))$ followed by $\mathrm{qExpand}_{\mathbb{Q}}\,M$ followed by the coefficientwise map $\mathbb{Q}((q)) \to K((q))$ induced by $\mathbb{Q} \to K$, equals $$\prod_{a \mid M}\ \prod_{\substack{0 \le b < M/a \\ \gcd(\gcd(a,b),\,M/a)=1}} \Bigl(X - \mathrm{qExpand}_{K}(a^{2})\bigl(\mathrm{qTwist}(\zeta^{ba})\,jq\bigr)\Bigr),$$ where $\mathrm{qTwist}(u)$ scales the coefficient of $q^{k}$ by $u^{k}$, i.e. substitutes $uq$ for $q$ (a vacuous case distinction guards $a = 0$, which cannot occur).
This is the classical determination of the conjugates of $j(q^{M})$ over $\mathbb{Q}(j)$, equivalently of the roots $j(\zeta^{b} q^{a/d})$ of the modular polynomial $\Phi_M(j, Y)$ indexed by the primitive slots $ad = M$, $0 \le b < d$, $\gcd(a,b,d) = 1$, obtained here from the prime-step splitting of $\Phi_p$, twists and coefficient extension rather than from coset representatives for $\Gamma_0(M)$. It feeds the symmetry statement for the modular polynomial data and the Hecke divisor computations on the characteristic-$p$ fibre models of the modular curve.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_minpoly_jqN_map_eq_prod_slots.lean
<!-- Generated by add_prove2me_provenance.py -->