perf(hex-primality-mathlib): bound negative rho search

[kim-em]

Fixes #9803

Summary

• replace the unnamed 16-restart rho fuel with explicit budgets: one deterministic restart and at most 2^16 Brent cycle steps
• apply that finite work cap throughout the supported 512-bit range, preserving odd small-factor coverage without an input-width cliff
• resume the random state returned by certificate search; conformance pins that the current root-composite preflight consumes zero attempts/draws, so replay starts exactly at seed n
• preserve parity preflight, proper-factor revalidation, independently kernel-checked deriveNotPrime terms, and bounded exhaustion with no trial-division fallthrough
• add fresh 25/32/64/65/512-bit probes, bridge conformance, an absolute-budget sweep, CI manifest tests, and release-quality designated-host evidence

Accepted contract for #9800

The opt-in Nat.Prime norm_num negative route runs only after bounded certificate search returns .composite. Certificate search starts from Hex.Rand.ofSeed n; factor search resumes the returned state with Hex.Nat.Internal.rhoFactorCountedWith? n f.rand natPrimeRhoRestartBudget natPrimeRhoStepBudget, where the named budgets are one restart and 2^16 Brent cycle steps per restart throughout the supported range of at most 512 input bits. The current root-composite preflight consumes zero attempts and leaves the seed state unchanged. The primitive parity preflight can return factor 2 without consuming a restart. Every returned candidate is revalidated as 1 < d, d < n, and n % d = 0 before deriveNotPrime emits an independently kernel-checked proper-factor proof. Exhaustion makes the Hex extension decline; the guarded trial alias also declines at and above 2^24, so exhaustion never starts total/unbounded trial division.

Measurements

Final source-matched release-quality sweep after rebasing onto #9842; CPU 22, six balanced samples per row, 10-second absolute fresh-module gate:

• 25-bit factor found: 3.137 s maximum candidate
• 32-bit factor found: 2.235 s
• 64-bit balanced factor found: 2.286 s
• 65-bit odd factor found: 2.423 s
• 512-bit parity factor found: 2.131 s
• 512-bit odd small factor found: 2.435 s
• 512-bit balanced exhaustion: 3.318 s

release_quality=true; no exceptions, violations, or exhausted sample pairs. Null robust spread/build ratios were 12.51% and 2.69%. The contract is explicitly absolute-only: import-subtracted deltas remain diagnostic and may be unresolved. Report: reports/bench-results/hex-primality-negative-policy-issue-9803-chungus2.json.

The old production-scaled policy was rejected during pilot work: one adversarial 82-bit restart took about 26 s, while the former 16-restart 512-bit search exceeded two minutes. The fixed 2^16 cap removes that scaling while retaining small-factor capability.

Independent review

The requested Opus review confirmed the soundness and no-fallback boundaries, then identified the original 64-bit input-width cliff, unresolved-relative-measurement presentation, missing SPEC/CI wiring, and seed-resume convention. This revision replaces the cliff with bounded work across all widths, makes the absolute contract explicit, updates SPEC and CI, adds 65/512-bit odd-factor probes, and resumes f.rand with exact state replay conformance.

Verification

• lake build HexPrimalityMathlib HexConformance HexPrimalityElabProbe (10,373 jobs)
• python3 -m unittest scripts.bench.test_primality_negative_sweep
• python3 scripts/bench/check_factor_sweep_freshness.py
• git diff --check origin/main...HEAD
• committed report source hashes revalidated after rebasing
• exact certificate-state replay, factor/attempt replay, parity attempts, 512-bit valid-factor replay, and exact exhaustion attempts are asserted in bridge conformance