3.5. Reusable certificates with primality?🔗

The explicitly requested construction tactic primality? uses a larger, finite search profile. It proves the Curve25519 field prime and offers a clickable Try this: replacement containing the complete checked certificate. This example checks the entire suggestion text, so changes to the generated certificate or its formatting are detected:

Apply the suggestion to keep certificate search out of subsequent builds. The replacement uses Hex.Nat.prime_of_checkPrimeAt and decide +kernel; the kernel still replays the certificate. A standalone file containing the replacement needs only import HexPrimality.Cert. The goal retains the expression 2 ^ 255 - 19. With HexPrimalityMathlib imported, primality? also handles Nat.Prime and suggests the corresponding bridge theorem.

Construction supports inputs through 521 bits, recursive depth 32, and a shared limit of 1024 attempts. primality? (maxAttempts := 29) sets a smaller limit; Curve25519 succeeds at 29 and exhausts at 28. It uses stage-one Pollard p - 1 up to 524288, bounded rho work, and deterministic small witnesses before random candidates. Every limit is finite; exhaustion reports the seed, attempts, and resource profile. Success depends on finding enough factors of predecessors for Pocklington, rather than on bit length alone. Construction first tries the factors found by table division before running the more expensive factor search. It can use a power of two alone and can trade up to 63 small-divisor checks for a smaller factored part of the predecessor. These checks are included in the reusable certificate and replayed by the kernel. The ordinary primality policy keeps its existing smaller budget.

With the standard import HexIntFactor, plain primality? also discovers secp256k1, P-384 and Curve448. It preserves the first route's successful certificate; only exhaustion with attempts left triggers a complete retry with bounded ECM. Both routes share the same 1024 attempts and advancing random state. These three fields need an explicit finite Lean heartbeat allowance; set_option maxHeartbeats 4000000 is tested, without a recursion-depth option. See the field-prime tutorial for complete examples. An explicit factor := provider or using certificate bypasses automatic selection. Use primality? (factor := Hex.Nat.Construction.factorSearch) for core-only construction. Automatic fallback also costs time on unsupported inputs: the 507-bit fixture still exhausts, taking about 20.7 seconds instead of 0.9 seconds on the measured host. Native search runs synchronously, so a heartbeat overrun can be reported after it returns; heartbeats are not a wall-clock timeout.

The Curve25519 result has three non-leaf certificate nodes and eight factor entries. Kernel replay reads the already verified sieve bitset for table leaves, and compiled prime enumeration reads 64 candidate bits at a time. Both changes are proved equal to their original implementations.

The fixed-corpus comparison measured Curve25519 native decision at 0.57 seconds and a fresh complete primality? build from its numeral at 1.63 seconds, including Lake overhead and kernel replay. Paired runs using the original 2 ^ 255 - 19 expression took 2.17–2.29 seconds, compared with 7.01–10.41 seconds before these optimizations. FLINT and PARI native decisions took 25.9 and 55.4 milliseconds respectively. The native timings use a standalone executable; the full tactic currently runs search through Lean’s interpreter before kernel checking. All completed samples are retained. These are host-specific observations, not latency guarantees. The measurement report records every sample, certificate sizes, and the comparison with the larger reference certificate.

The fixed comparison corpus also includes standard cryptographic field primes. The current construction profile finds P-256 and the structured 511/512-bit benchmark primes and P-521. The default profile exhausts on secp256k1, P-384 and Curve448. The explicit ECM provider constructs all three: see the field-prime tutorial for complete examples and reusable proofs. P-521 uses 25 factor candidates and 170 attempts; the constructor admits at most 32 factors and still examines at most 4096 subsets. For the expression 2 ^ 521 - 1, set local maxRecDepth to 1024 and exponentiation.threshold to 521; its numeral needs neither option. The standard-field report records the default profile's factoring barriers and separate construction, rendering, and replay measurements. This is not a general-purpose prover for arbitrary cryptographic-size primes.

The first cactus plot compares native exact primality decisions with the complete primality? build. Native timings exclude Lean proof emission and kernel replay, imports, and input conversion. Hex uses certificate construction and a compiled self-check internally to decide primality; FLINT and PARI return exact decisions through their native algorithms. The dashed curve includes the full fresh Lake build: certificate construction, proof emission, imports, and kernel checking.

Direct kernel measurements exclude imports, search, and proof elaboration. They check complete proof bodies, including expanded local auxiliary proofs. With PrimeCert’s fixed-window powering and the same selected Pocklington factors, supplied Curve25519 replay takes about 4.54 milliseconds for Hex and 3.54 milliseconds for PrimeCert on the recorded host. Curve448 takes 9.30 and 6.44 milliseconds. PrimeCert uses common witness bases; a separate matched-base experiment distinguishes that certificate choice from checker cost.

Complete automatic construction is a separate comparison. On the matched Curve25519 Nat.Prime goal, the repeated fresh-module experiment measures about 2.39 seconds for Hex primality? and 3.55 seconds for PrimeCert prime_cert?, including imports, construction, elaboration, and checking. These noisy shared-host observations are not portable performance promises. The replay attribution records exact revisions, every sample, component costs, negative controls, and construction regression checks. Hex uses Lean 4.34.0 and PrimeCert uses Lean 4.33.0; identical-code calibration is reported separately. The kernel replay comparison uses a supplied Curve448 certificate in both systems. The explicit ECM route in the field-prime tutorial constructs its own certificate. The corpus is small and structured.