def Hex.Nat.numOfIndex (t : Nat) : Nat

The number named by sieve index t: the t-th member of 1, 5, 7, 11, 13, 17, …, the residues coprime to 6.

Equations

• Hex.Nat.numOfIndex t = 3 * t + 1 + t % 2

def Hex.Nat.indexOfNum (n : Nat) : Nat

The sieve index of a residue coprime to 6 (numOfIndex_indexOfNum is the round trip).

Equations

• Hex.Nat.indexOfNum n = n / 3

def Hex.Nat.indexWidth (bound : Nat) : Nat

The number of sieve indices representing values below bound.

Equations

• Hex.Nat.indexWidth bound = 2 * (bound / 6) + if bound % 6 ≥ 2 then 1 else 0

theorem Hex.Nat.numOfIndex_lt_iff {t bound : Nat} : numOfIndex t < bound ↔ t < indexWidth bound

theorem Hex.Nat.numOfIndex_indexOfNum {n : Nat} (h : n % 6 = 1 ∨ n % 6 = 5) : numOfIndex (indexOfNum n) = n

theorem Hex.Nat.indexOfNum_numOfIndex (t : Nat) : indexOfNum (numOfIndex t) = t

def Hex.Nat.doubleRounds (step width : Nat) : Nat → Nat → Nat

Union a mask with its own shifts by step · 2^i for i < r, truncating to width bits every round: after r rounds the mask covers 2^r progression terms per seed bit within the width. Truncating (and skipping shifts that alone exceed the width) keeps every intermediate below 2^width; an untruncated round at the 32-round budget would materialise numbers of step · 2^31 bits.

Equations

• Hex.Nat.doubleRounds step width 0 x✝ = x✝
• Hex.Nat.doubleRounds step width r.succ x✝ = Hex.Nat.doubleRounds step width r (if step * 2 ^ r < width then (x✝ ||| x✝ <<< (step * 2 ^ r)) % 2 ^ width else x✝)

def Hex.Nat.markMask (start step width : Nat) : Nat

The marking mask: progression start start, index step step, truncated to width bits, with enough rounds to cover that width.

Equations

• Hex.Nat.markMask start step width = Hex.Nat.doubleRounds step width (max 32 (width.log2 + 1)) (1 <<< start % 2 ^ width)

def Hex.Nat.markCandidate (width state s : Nat) : Nat

Clear the multiples of p = numOfIndex s at or above p²: the union of the two progressions of index step 2p starting at the indices of p · numOfIndex s and p · numOfIndex (s + 1) (the two residue classes of the cofactor). Nat has no complement, so clearing is and-with-xor against the all-ones width mask.

Equations

• One or more equations did not get rendered due to their size.

def Hex.Nat.sieveGoRange (width : Nat) : Nat → Nat → Nat → Nat

Mark the candidates s, s + 1, … for count steps, unconditionally: marking multiples at or above the square of any coprime-to-6 value only ever clears composites, and the unguarded fold removes an entire invariant from the proof (restricting to unmarked candidates is a later, separately provable optimization).

Equations

• Hex.Nat.sieveGoRange width x✝¹ 0 x✝ = x✝
• Hex.Nat.sieveGoRange width x✝¹ count.succ x✝ = Hex.Nat.sieveGoRange width (x✝¹ + 1) count (Hex.Nat.markCandidate width x✝ x✝¹)

def Hex.Nat.sieveInit (width : Nat) : Nat

All candidate bits except index 0, which names the non-prime 1.

Equations

• Hex.Nat.sieveInit width = 2 ^ width - 2

def Hex.Nat.sieve (bound sqrtBound : Nat) : Nat

The sieve over values below bound, marking candidates up to sqrtBound. sqrtBound is data (rather than Nat.sqrt bound) because core Nat.sqrt does not kernel-reduce; correctness only needs bound ≤ sqrtBound².

Equations

• Hex.Nat.sieve bound sqrtBound = Hex.Nat.sieveGoRange (Hex.Nat.indexWidth bound) 1 (Hex.Nat.indexWidth (sqrtBound + 1) - 1) (Hex.Nat.sieveInit (Hex.Nat.indexWidth bound))

theorem Hex.Nat.sieveGoRange_add (width s a b state : Nat) : sieveGoRange width s (a + b) state = sieveGoRange width (s + a) b (sieveGoRange width s a state)

The fold-splitting lemma the batched replay elaborator stands on.

theorem Hex.Nat.sieve_prime_iff {bound sqrtBound t : Nat} (hsqrt : bound ≤ sqrtBound * sqrtBound) (ht : 0 < t) (hrange : numOfIndex t < bound) : (sieve bound sqrtBound).testBit t = true ↔ Prime (numOfIndex t)

Exact sieve correctness within the represented range and above index zero. The square bound makes the marking loop complete.

theorem Hex.Nat.sieve_testBit_iff {bound sqrtBound t : Nat} (_hmask : indexWidth bound ≤ 2 ^ 32) (hsqrt : bound ≤ sqrtBound * sqrtBound) (ht : 0 < t) (hrange : numOfIndex t < bound) : (sieve bound sqrtBound).testBit t = true ↔ Prime (numOfIndex t)

Compatibility form of sieve correctness for the original mask range.

def Hex.Nat.bitsToListGo (state : Nat) : Nat → Nat → List Nat

Collect the represented values with set bits over fuel indices starting at t0, ascending.

Equations

• Hex.Nat.bitsToListGo state x✝ 0 = []
• Hex.Nat.bitsToListGo state x✝ fuel.succ = if state.testBit x✝ = true then Hex.Nat.numOfIndex x✝ :: Hex.Nat.bitsToListGo state (x✝ + 1) fuel else Hex.Nat.bitsToListGo state (x✝ + 1) fuel

def Hex.Nat.Sieve.readBits (word start : Nat) : Nat → Nat → List Nat

Read a bounded word, translating its bit indices to sieve indices.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Nat.Sieve.readBits word start x✝ 0 = []

def Hex.Nat.Sieve.readChunks (state : Nat) : Nat → Nat → Nat → List Nat

Read at most 64 bits per word. Each large-integer shift supplies a whole word, instead of copying the large integer once per candidate bit. Completeness requires count ≤ 64 * fuel; less fuel returns only a prefix. Use bitsToListFast to supply enough fuel automatically.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Nat.Sieve.readChunks state 0 x✝¹ x✝ = []

def Hex.Nat.bitsToListFast (state start count : Nat) : List Nat

Compiled readback in 64-bit chunks, equal to the structural bit scan at every state, starting index, and length.

Equations

• Hex.Nat.bitsToListFast state start count = Hex.Nat.Sieve.readChunks state (count / 64 + 1) start count

@[csimp]

theorem Hex.Nat.bitsToListGo_eq_fast : bitsToListGo = bitsToListFast

Chunking changes only runtime readback, not its exact list or order.

def Hex.Nat.bitsToList (state bound : Nat) : List Nat

The represented values with set bits below bound, ascending, starting from index 1 (index 0 names the non-prime 1).

Equations

• Hex.Nat.bitsToList state bound = Hex.Nat.bitsToListGo state 1 (Hex.Nat.indexWidth bound - 1)

theorem Hex.Nat.mem_bitsToList {state bound n : Nat} (hw : 1 ≤ indexWidth bound) : n ∈ bitsToList state bound ↔ ∃ (t : Nat), 1 ≤ t ∧ t < indexWidth bound ∧ state.testBit t = true ∧ numOfIndex t = n

Membership in the read-back list is a set bit on a represented index above 0.

theorem Hex.Nat.bitsToList_pairwise_lt (state bound : Nat) : List.Pairwise (fun (x1 x2 : Nat) => x1 < x2) (bitsToList state bound)

The read-back list is strictly ascending.

theorem Hex.Nat.prime_mod_six {n : Nat} (hp : Prime n) (h5 : 5 ≤ n) : n % 6 = 1 ∨ n % 6 = 5

A prime of at least 5 is coprime to 6: the residue fact that puts primes onto sieve indices.

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

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

Equations

• Hex.Nat.primesBelow bound = if bound ≤ 2 then [] else if bound ≤ 3 then [2] else 2 :: 3 :: Hex.Nat.bitsToList (Hex.Nat.sieve bound (bound.sqrt + 1)) bound

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

Exact membership in the runtime prime enumeration.

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

The runtime prime enumeration is strictly ascending.

theorem Hex.Nat.primesBelow_nodup (bound : Nat) : (primesBelow bound).Nodup

No prime occurs twice in the runtime enumeration.