19.5. Coverage and failure messages
Every input must be a closed term. A polynomial mentioning a local
hypothesis or metavariable is rejected. Executable FpPoly and
ZPoly inputs must also be definitionally transparent, so compiled
evaluation and kernel checking can both see their coefficients.
Mathlib Polynomial inputs are parsed from X, Polynomial.C,
numerals, addition, subtraction, multiplication, negation, and powers
with literal natural exponents. Named definitions are unfolded within
a fixed fuel limit. Other constructors, such as a raw
Polynomial.monomial application, receive an unsupported-syntax
error even when the term is closed.
For FpPoly p, every closed input at a literal prime modulus inside
the ZMod64 bounds is covered, subject to the Rabin-certificate replay
budget
(degree + 1) · p ≤ 2²⁶.
The budget is checked once for each distinct factor. An over-budget input is rejected during elaboration instead of emitting a proof that would be too expensive to check. A composite modulus is rejected with a message saying that the modulus is not prime.
Integer factor search is total, but the plain tactics still need a small certificate for each irreducible factor. They recognize:
-
prime constants and primitive linear polynomials;
-
irreducibility after reduction at a prime below
512; -
Eisenstein's criterion after shifts
0, ±1, ±2, ±3, with witness primes at most128; -
multi-prime degree obstructions using primes from
3through71.
These bounded searches do not cover every irreducible polynomial. Balanced Swinnerton-Dyer examples can be reducible at every candidate prime, fail all of the small Eisenstein shifts, and retain a possible proper factor degree in every modular factorization. The plain tactics then report the factor they could not certify and point to the kernel-evaluated forms. They never weaken the requested statement.
Zero polynomials and units receive targeted messages rather than false
irreducibility proofs. A reducible input to irreducibility reports
the factor count found by factor_poly.