perf(hex-primality): enforce measured elaborator policy

[kim-em]

Closes #9779.

This PR replaces the unexplained 8192-bit primality elaborator guard with a shared, measured positive-certificate policy:

• enforce a 512-bit input ceiling, 1040 recursive fuel ceiling, 2 Brent restarts, and 32768 cycle steps per restart across core and Mathlib certificate handlers
• reject over-budget inputs before search; report exhaustion with exact attempts, seed, fuel, and search maxima; never fall through to total trial decision
• generalize the composite-verdict theorem to every explicit PrimeCertBudget
• document and enforce a 10-second absolute fresh-module contract, with an explicit absolute-only harness mode that leaves all relative-budget sweeps unchanged
• exercise accepted boundary search with the rho-backed prime 100297^22 * 2^146 + 1 (31 counted attempts), deterministic 512-bit exhaustion, 513-bit rejection, certificate reification, and kernel replay
• keep the separately bounded opt-in negative factor route documented truthfully without claiming it uses the positive certificate allocation
• commit six clean samples per route with full shared-host provenance; worst observed candidate wall times are 2.52 seconds core and 3.03 seconds Mathlib
• register the build-only elaboration probes and extend the existing single CI job

Local verification:

• lake build HexPrimality HexPrimalityMathlib HexPrimalityKernelProbe HexPrimalityElabProbe HexPrimality.Conformance HexPrimalityMathlib.Conformance HexIntFactor hexprimality_bench
• 126 Python unit checks across the fresh-module harness, primality policy, Mathlib-free lint, factor freshness, and DAG validation
• python3 scripts/check_dag.py
• python3 scripts/ci/check_benches_mathlib_free.py
• python3 scripts/bench/check_factor_sweep_freshness.py
• python3 scripts/check_copyright_headers.py
• git diff --check