13.5. Verification🔗

The executable library proves product reconstruction and the algebra of the Berlekamp and Rabin checks. The Mathlib companion proves that successful certificates imply the usual Irreducible predicate and that the factors returned from a square-free input are irreducible. Certificate generation is search; the small checker and its proof determine what is trusted.