def Hex.PrimalityTactic.natPrimeCertThreshold : Nat

The measured opt-in norm_num crossover. Numerals below 2^24 use trial division; 25-bit and larger numerals use bounded certificate search.

Equations

• Hex.PrimalityTactic.natPrimeCertThreshold = 16777216

def Hex.PrimalityTactic.natPrimeRhoRestartBudget : Nat

Restart budget for the opt-in negative Nat.Prime route. One seeded draw preserves useful small-factor coverage without multiplying the bounded exhaustion cost.

Equations

• Hex.PrimalityTactic.natPrimeRhoRestartBudget = 1

def Hex.PrimalityTactic.natPrimeRhoStepBudget : Nat

Per-restart Brent cycle-step budget for the opt-in negative Nat.Prime route. The fixed cap bounds work independently of input width while retaining odd small-factor coverage through the supported 512-bit ceiling.

Equations

• Hex.PrimalityTactic.natPrimeRhoStepBudget = 1 <<< 16