7.6. Trial-division primality🔗

HexArith supplies a self-contained primality test. It checks that no integer in [2, n) divides n, and its soundness theorem lifts a true result to the project-local Hex.Nat.Prime predicate: a primality witness produced without native_decide or a fixed prime table, so downstream prime searches can certify candidates beyond any precomputed list.

def

Hex.Nat.Prime (p : Nat) : Prop
Hex.Nat.Prime (p : Nat) : Prop

A natural number is prime when it is at least 2 and its positive divisors are trivial. This is the Mathlib-free prime predicate used by downstream modular arithmetic layers.

def

Hex.Nat.isPrimeTrial (n : Nat) : Bool
Hex.Nat.isPrimeTrial (n : Nat) : Bool

Executable trial-division primality test. Returns true only when 2 ≤ n and no integer in [2, n) divides n. Used by downstream prime-search extensions to produce primality witnesses for candidates beyond any fixed list, without depending on Mathlib or native_decide.

theorem

Hex.Nat.isPrimeTrial_isPrime {n : Nat}
  (h : Hex.Nat.isPrimeTrial n = true) : Hex.Nat.Prime n
Hex.Nat.isPrimeTrial_isPrime {n : Nat}
  (h : Hex.Nat.isPrimeTrial n = true) :
  Hex.Nat.Prime n

Soundness of the trial-division primality test against the project-local Hex.Nat.Prime predicate. Used by the BZ extended prime search to lift a runtime candidate into a SmallPrimeCandidate with explicit primality evidence, without falling back to a hardcoded list.