5.9. The prime table and initial segments🔗

A committed table of the 9,592 primes below 10^5 anchors the small end: compiled membership uses binary search, while kernel replay reads a bit from the verified final sieve state. Both lookup paths are proved equal at every input. Both directions of correctness are proved against a kernel-replayed sieve run (the batched verification is regenerated, never hand-edited, via the #rebuild_primeTable command).

def

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

Membership in the committed prime table. Kernel reduction reads a bit from the already verified final sieve state; compiled code uses binary search through isTablePrime_eq_tableSearch.

The verified compiled sieve also provides a list of every prime strictly below a requested bound, including the exceptional primes 2 and 3. Its membership and strict ordering theorems are independent of the committed table. Pollard p - 1 and ECM use this runtime source for their stage primes:

def

Hex.Nat.primesBelow (bound : ℕ) : List ℕ
Hex.Nat.primesBelow (bound : ℕ) : List ℕ

All primes strictly below the bound, in ascending order. The compiled sieve generates the initial segment at runtime, independently of the table.

theorem

Hex.Nat.mem_primesBelow {bound n : ℕ} :
  n ∈ Hex.Nat.primesBelow bound ↔ n < bound ∧ Hex.Nat.Prime n
Hex.Nat.mem_primesBelow {bound n : ℕ} :
  n ∈ Hex.Nat.primesBelow bound ↔
    n < bound ∧ Hex.Nat.Prime n

Exact membership in the runtime prime enumeration.

theorem

Hex.Nat.primesBelow_pairwise_lt (bound : ℕ) :
  List.Pairwise (fun x1 x2 => x1 < x2) (Hex.Nat.primesBelow bound)
Hex.Nat.primesBelow_pairwise_lt
  (bound : ℕ) :
  List.Pairwise (fun x1 x2 => x1 < x2)
    (Hex.Nat.primesBelow bound)

The runtime prime enumeration is strictly ascending.

The interval API still uses trial division, with no upper bound tied to the table:

#[2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97]#eval Hex.Nat.primesIn 0 100

#[2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97]

def

Hex.Nat.primesIn (lo hi : ℕ) : Array ℕ
Hex.Nat.primesIn (lo hi : ℕ) : Array ℕ

The primes in [lo, hi), ascending. Runtime decision through the isPrimeTrial-backed Decidable instance; the committed table plays no role, so the range is unrestricted.

theorem

Hex.Nat.mem_primesIn {lo hi n : ℕ} :
  n ∈ Hex.Nat.primesIn lo hi ↔ lo ≤ n ∧ n < hi ∧ Hex.Nat.Prime n
Hex.Nat.mem_primesIn {lo hi n : ℕ} :
  n ∈ Hex.Nat.primesIn lo hi ↔
    lo ≤ n ∧ n < hi ∧ Hex.Nat.Prime n

Membership in primesIn lo hi is exactly primality in the half-open interval [lo, hi).