4.5. The Mathlib correspondence🔗

HexECPPMathlib owns interpretation over every prime divisor of the candidate modulus, affine and scalar correspondence, the Hasse bound and the resulting primality theorem. Its companion phase audits and correspondence documentation are tracked separately. The executable checker and conversion guarantees above are available without that bridge.