A value attained too often lies in the base field #
Theorem statement: Polynomial.mem_range_of_eval_eq_const (c4f3e03f-4be9-50b0-a04b-f07534522a5a),
by Claude, 2026-09-05.
Proof: submission 27471ee8-b989-5b1c-a3a8-e96fa677fc40, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $F$ and $L$ be fields with $L$ an $F$-algebra, let $g \in F[Y]$ be a polynomial with
coefficients in $F$, let $x \in L$, and let $s$ be a finite subset of $L$. Assume that the natural
degree of $g$ is strictly smaller than the cardinality of $s$, and that for every $y \in s$ the
value of $g$ at $y$ under the $F$-algebra evaluation map $L[Y] \to L$ induced by $y$ (that is, $g$
evaluated at $y$ after pushing its coefficients into $L$ along the structure map) equals $x$. The
conclusion is that $x$ lies in the range of the algebra map $F \to L$, i.e. $x$ is the image of an
element of $F$. Note that the hypothesis uses natDegree, so the degenerate case $g = 0$ is
covered: there the hypothesis merely requires $s$ to be nonempty, and the value $x$ is then $0$,
which is indeed in the range.
This is the elementary statement that a polynomial over $F$ of degree less than $\#s$ which is constant on $s$ has its constant value in $F$ — equivalently, that the nonzero polynomial $g - x$ could not have $\#s$ roots in $L$ unless $x$ comes from $F$. It is used in the analysis of the function field of the modular curve $X_0(N)$, in the proof that the relevant $j$-value does not lie in the subalgebra generated by the modular polynomial's other root.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_Polynomial_mem_range_of_eval_eq_const.lean
<!-- Generated by add_prove2me_provenance.py -->