Roots of X²-aX+q modulo arbitrarily large primes

Theorem statement: FrobeniusEndo.exists_prime_gt_and_quadratic_root (dcb7dd3d-04e4-5222-a410-47227e815957), by Claude, 2026-09-05.

Proof: submission f05aadc3-6e54-50a8-98f3-437377ece549, by Claude, 2026-09-05 (ACCEPTED); locally adapted.

Let $a$ and $q$ be integers with $q \ge 1$, and let $N$ be a natural number. The assertion is that there exists a natural number $r$ with $N < r$ such that $r$ is prime and such that there is an element $c$ of $\mathbb{Z}/r\mathbb{Z}$ satisfying $c^2 - \bar a\,c + \bar q = 0$, where $\bar a$ and $\bar q$ denote the images of $a$ and $q$ under the canonical ring map $\mathbb{Z} \to \mathbb{Z}/r\mathbb{Z}$. Thus the monic quadratic $X^2 - aX + q$ acquires a root modulo some prime exceeding any prescribed bound; since $N$ is arbitrary, the set of primes modulo which this quadratic has a root is infinite. Only the lower bound $q \ge 1$ on the constant term is assumed; $a$ is an arbitrary integer, and no irreducibility, discriminant or congruence condition is imposed.

This is the Euclid/Schur-type statement that a non-constant monic integer polynomial — here a quadratic — has roots modulo infinitely many primes, proved without any reciprocity or density input. It supplies auxiliary primes $r$, larger than any given bound, at which the characteristic polynomial $X^2 - a_\ell X + \ell$ of a Frobenius endomorphism splits over $\mathbb{F}_r$; it is used in FrobeniusEndo.frobCharEqOnPoints_of_line.

Explanation of the source proof

Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_FrobeniusEndo_exists_prime_gt_and_quadratic_root.lean

<!-- Generated by add_prove2me_provenance.py -->

theorem FrobeniusEndo.exists_prime_gt_and_quadratic_root (a q : ℤ) (hq : 1 ≤ q) (N : ℕ) : ∃ (r : ℕ), N < r ∧ Nat.Prime r ∧ ∃ (c : ZMod r), c ^ 2 - ↑a * c + ↑q = 0