4.1. Introduction🔗

HexECPP checks arithmetic certificates, converts supplied PARI vectors, and offers an explicitly bounded native CM producer. It uses HexArith.bitLength from HexArith and terminal Hex.Nat.PrimeCert certificates from HexPrimality. The implementation imports no Mathlib module. Production is opt-in: ordinary primality does not automatically fall back to ECPP.

An accepted certificate establishes the arithmetic premises used by ECPP. The unconditional primality implication additionally needs the curve semantics and Hasse bound owned by HexECPPMathlib.