3.2. Deciding primality🔗

Hex.Nat.isPrime is the total convenience decision: the committed table below 10^5, exact trial division below 6 · 10^6, and certificate search above.

true#eval Hex.Nat.isPrime 1945555039024054273  -- 27 · 2^56 + 1

true

false#eval Hex.Nat.isPrime 561  -- a Carmichael number

false

def

Hex.Nat.isPrime (n : ℕ) : Bool
Hex.Nat.isPrime (n : ℕ) : Bool

The pure total convenience decision: the bounded path from the reproducible seed, with exact trial division as the fallback if that path exhausts its fuel, which is what makes the iff unconditional. Callers that need a real time bound and resumable state use isPrime?.

theorem

Hex.Nat.isPrime_iff {n : ℕ} : Hex.Nat.isPrime n = true ↔ Hex.Nat.Prime n
Hex.Nat.isPrime_iff {n : ℕ} :
  Hex.Nat.isPrime n = true ↔
    Hex.Nat.Prime n

The total decision is exact.

Callers that need a real time bound use the resumable form, which returns the advanced random state on failure instead of silently retrying:

def

Hex.Nat.isPrime? (n : ℕ) (r : Hex.Rand) (fuel : ℕ) :
  Except Hex.Nat.PrimeDecisionFailure (Bool × Hex.Rand)
Hex.Nat.isPrime? (n : ℕ) (r : Hex.Rand)
  (fuel : ℕ) :
  Except Hex.Nat.PrimeDecisionFailure
    (Bool × Hex.Rand)

The bounded decision: table below primeTableBound, Miller--Rabin composite filtering, exact trial division below isPrimeTrialThreshold, then certificate search. A failed base or a table/trial miss returns a certified false; an accepted certificate returns true; an exhausted search is an error rather than an unbounded computation.

theorem

Hex.Nat.isPrime?_spec {n : ℕ} {r : Hex.Rand} {fuel : ℕ} {b : Bool}
  {r' : Hex.Rand} (h : Hex.Nat.isPrime? n r fuel = Except.ok (b, r')) :
  b = true ↔ Hex.Nat.Prime n
Hex.Nat.isPrime?_spec {n : ℕ}
  {r : Hex.Rand} {fuel : ℕ} {b : Bool}
  {r' : Hex.Rand}
  (h :
    Hex.Nat.isPrime? n r fuel =
      Except.ok (b, r')) :
  b = true ↔ Hex.Nat.Prime n

Every successful bounded decision is exact.

Compositeness is filtered by Miller-Rabin before any certificate work begins. The test is deliberately not exposed to proofs — it appears in no proof term — but it is available as a runtime filter:

def

Hex.Nat.isProbablePrime (n : ℕ)
  (bases : List ℕ := Hex.Nat.defaultBases) : Bool
Hex.Nat.isProbablePrime (n : ℕ)
  (bases : List ℕ :=
    Hex.Nat.defaultBases) :
  Bool

Run millerRabin over a base list. true proves nothing about n; it is consumed only as a filter ahead of certificate construction.