1.6. Trial-division primality🔗

HexArith supplies a self-contained primality test. It checks candidate divisors from 2 through ⌊√n⌋, stopping before the first candidate whose square exceeds n. 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 bounded trial-division primality test. Returns true exactly when n is prime. Candidate divisors start at 2, and the loop stops before testing the first k whose square exceeds n; thus it performs at most ⌊√n⌋ - 1 remainder tests. It remains pure Lean so emitted primality certificates can be replayed by the kernel without Mathlib, native_decide, or a fixed prime table.

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 Mathlib-free Hex.Nat.Prime predicate. It turns a successful runtime test into explicit primality evidence without relying on a hardcoded prime table.

theorem

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

Completeness of the executable trial-division test: every project-local prime witness makes the Boolean checker return true.