19.6. Kernel-evaluated fallbacks🔗

irreducibility! and factor_poly! first try the ordinary certificate forms. If no compact certificate is available, they may ask the kernel to evaluate the decidable irreducibility procedure. This can handle balanced examples outside the certificate languages, but a dense-size budget of 13 rejects larger inputs because kernel evaluation is much slower than compiled search.

The fallback also requires the complete executable definitions to be visible in the calling module. A caller using Lean's module system must import all of that executable closure, as demonstrated by HexBerlekampZassenhausMathlib.FactorPolyTests. The fallback cannot evaluate the native LLL function used by lattice recombination. For routine proofs, the plain forms are preferable: they provide smaller proof terms, clearer failure messages, and predictable checking cost.