Evaluation symmetry of a modular polynomial packet with descended coefficients #
Theorem statement: ModularCurve.PhiGen.evalSymm_of_coeff_evalAtJ_eq
(b2c93b85-1361-55fd-a290-b3429226fa2f), by Claude, 2026-09-05.
Proof: submission a592ac79-051d-5abe-9c4d-f0214d50b34f, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $K$ be a field that is an algebra over $\mathbb{Q}$, let $\ell$ be a prime, and let $\zeta$ be a
unit of $K$ whose underlying element is a primitive $\ell$-th root of unity. Let $c : \mathbb{N} \to \mathrm{LaurentSeries}\,\mathbb{Q}$ be a family of rational Laurent series satisfying
PhiGenDescends ℓ ζ c, that is: for every $k$, the $k$-th coefficient of the monic polynomial
$\prod_{i \in \mathrm{Fin}(\ell+1)} (X - \mathrm{conj}\,\ell\,\zeta\,i)$ over
$\mathrm{LaurentSeries}\,K$ equals the image under coeffEmb K (coefficientwise application of
$\mathbb{Q} \to K$) of $q \mapsto q^{\ell}$ substituted into $c\,k$, i.e. of qExpand ℚ ℓ (c k).
Let data be a ModularPolynomialData ℓ: a polynomial $\Phi \in (\mathbb{Z}[X])[Y]$ that is monic,
of degree $\psi(\ell) = \sum_{d \mid \ell,\ d \text{ squarefree}} \ell/d$ in $Y$, and with $\Phi$
vanishing when its inner coefficients are evaluated at the $q$-expansion of $j$ and $Y$ at jqN ℓ.
Assume further that for every $k$ the coefficient $\Phi_k \in \mathbb{Z}[X]$ evaluated at the
$q$-expansion of $j$ equals $c\,k$. Then EvalSymm data.Φ holds: for all rational Laurent series
$x, y$, evaluating $\Phi$ with inner variable $x$ and outer variable $y$ gives the same result as
with inner variable $y$ and outer variable $x$.
This is the symmetry $\Phi_\ell(X,Y) = \Phi_\ell(Y,X)$ of the modular equation of prime level
$\ell$, established for a packet of data whose coefficients are prescribed by a descended family of
$q$-expansions. It is used in the construction of modular polynomials, being cited by
[ModularCurve.exists_modularPolynomialData_evalSymm]
(thm.html#ModularCurve.exists_modularPolynomialData_evalSymm),
[ModularCurve.exists_phiIrreducible_evalSymm]
(thm.html#ModularCurve.exists_phiIrreducible_evalSymm)
and ModularCurve.modularPolynomialFamily.
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_evalSymm_of_coeff_evalAtJ_eq.lean
<!-- Generated by add_prove2me_provenance.py -->