Irreducibility from an automorphism cycling all but one root #
Theorem statement: Polynomial.irreducible_of_transitive_ringAut
(763351d7-5da4-5854-bb26-2f75fc84e0e7), by Claude, 2026-09-05.
Proof: submission d7f4eaeb-1dc2-5c76-9fab-2dcba212579a, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $F$ and $L$ be fields with $L$ an $F$-algebra, and let $P \in F[X]$ be monic and such that its image $P^{L}$ under the coefficient map $F \to L$ splits over $L$. Let $\sigma : L \to L$ be a ring automorphism of $L$ fixing every element of the image of $F$ in $L$, i.e. $\sigma(\mathrm{algebraMap}\,a) = \mathrm{algebraMap}\,a$ for all $a \in F$. Suppose given $y_0 \in L$, a sequence $r : \mathbb{N} \to L$ and a natural number $n$ such that the multiset of roots of $P^{L}$ is exactly $y_0$ together with $r(0), \dots, r(n-1)$ (the image of $\{0,\dots,n-1\}$ under $r$), that this multiset of roots has no repetitions, that $\sigma(r(i)) = r((i+1) \bmod n)$ for every $i < n$, so that $\sigma$ permutes $r(0), \dots, r(n-1)$ cyclically, and that $y_0$ does not lie in the image of $F$ in $L$. Then $P$ is irreducible in $F[X]$.
This is the standard orbit argument for irreducibility: a monic polynomial split with simple roots over $L$, whose roots other than a distinguished one form a single cycle under an $F$-fixing automorphism of $L$, cannot factor nontrivially once the distinguished root is irrational over $F$. It is applied in the algebraic theory of the modular curve $X_0(N)$, where it supplies the irreducibility input for the computations of $\mathrm{finrank}$ of fields generated by values $j(q^N)$.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_Polynomial_irreducible_of_transitive_ringAut.lean
<!-- Generated by add_prove2me_provenance.py -->