theorem Hex.Nat.primeTable_spec (n : ℕ) : n < primeTableBound → (n ∈ primeTable ↔ _root_.Nat.Prime n)

The committed table lists exactly the primes below its bound.

theorem Hex.Nat.primesIn_spec (lo hi n : ℕ) : n ∈ primesIn lo hi ↔ lo ≤ n ∧ n < hi ∧ _root_.Nat.Prime n

Range enumeration is exact for Nat.Prime.

theorem Hex.Nat.filter_prime_range [DecidablePred _root_.Nat.Prime] {bound : ℕ} (h : bound ≤ primeTableBound) : Finset.filter _root_.Nat.Prime (Finset.range bound) = (List.filter (fun (p : ℕ) => decide (p < bound)) primeTable.toList).toFinset

The Finset of primes below a bound inside the table's range is the filtered table.

theorem Hex.Nat.forall_prime_lt {P : ℕ → Prop} {bound : ℕ} (hb : bound ≤ primeTableBound) (h : ∀ p ∈ primeTable, p < bound → P p) (p : ℕ) : p < bound → _root_.Nat.Prime p → P p

Every-prime-below-a-bound statements reduce to a check over the table entries.