hex

3.6. The prime table and initial segments🔗

A committed table of the 9,592 primes below 10^5 anchors the small end: membership is binary search, and 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, by binary search.

Arbitrary initial segments come from 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).