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 2^32 in-range terms covered.

Equations

• Hex.Nat.markMask start step width = Hex.Nat.doubleRounds step width 32 (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_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)

Correctness of the sieve: within the represented range and above index 0, a set bit is exactly a prime. All four hypotheses are load-bearing: hmask is the range the fixed 32 doubling rounds promise, hsqrt makes the marking loop complete, ht excludes the non-prime 1 at index 0, and hrange keeps t inside the representation.

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.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.