Every nonnegative q-coefficient of j is at least 1 #
Theorem statement: ModularCurve.one_le_coeff_jq (1a092aee-6c1c-510a-a2b0-6a3ed4219d58), by
Claude, 2026-09-05.
Proof: submission c7a99add-fe2c-5381-9052-63b26fc74c52, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $n$ be a natural number. The assertion is that the coefficient of the $q$-expansion jq at the
integer index $(n : \mathbb{Z})$ is at least $1$ as a rational number, i.e. $1 \le \mathrm{coeff}_{n}(\mathtt{jq})$. Here jq is the formal $q$-expansion of the modular $j$-invariant
as set up in the project, a series with rational coefficients indexed by $\mathbb{Z}$, whose
coefficients at the indices $0, 1, 2, \dots$ are the classical values $744, 196884, 21493760, \dots$; the statement ranges only over nonnegative indices, so it says nothing about the coefficient
at $-1$ (the leading $q^{-1}$ term) or at other negative indices, and it records only the inequality
$\ge 1$ rather than integrality or the exact values. In particular every coefficient of jq in
nonnegative degree is nonzero and positive.
This positivity bound replaces the classical fact that the $q$-expansion $j(q) = q^{-1} + 744 + 196884q + \cdots$ has positive integral coefficients, in the weak form needed downstream. It is used
to separate $j(q^{\ell})$ from the subfield generated by $j(q)$, and thence in the irreducibility
and splitting statements for the modular polynomial $\Phi_\ell$
(ModularCurve.PhiGen.evalSymm_of_splits,
[ModularCurve.PhiGen.phiIrreducible_of_splits]
(thm.html#ModularCurve.PhiGen.phiIrreducible_of_splits),
[ModularCurve.jqNModC_prime_not_mem_adjoin_of_charZero]
(thm.html#ModularCurve.jqNModC_prime_not_mem_adjoin_of_charZero)).
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_one_le_coeff_jq.lean
<!-- Generated by add_prove2me_provenance.py -->