structure Hex.ZMod64.Modulus : Type

A usable word-sized modulus together with the evidence required by ZMod64.

• m : Nat

  The natural-number modulus.

• bounds : Bounds self.m

  Positivity and word-size bounds for the modulus.

structure Hex.ZMod64.Primeextends Hex.ZMod64.Modulus : Type

A usable word-sized modulus known to be prime. This is the data-carrying counterpart of the PrimeModulus typeclass.

• m : Nat
• bounds : Bounds self.m
• prime : Nat.Prime self.m

  Project-local primality evidence for the bundled modulus.

def Hex.ZMod64.primesBelow (start : Nat) : Nat → Array Prime

Return at most the requested number of successive primes below 2^31, in descending order starting at start. Runtime trial division produces the primality evidence stored in every result; candidates above the ZMod64 bound are skipped by clamping the start of the scan.

Equations

• Hex.ZMod64.primesBelow start x✝ = Hex.ZMod64.primesBelow.go✝ x✝ (min start (2 ^ 31 - 1)) ⋯ #[]

theorem Hex.ZMod64.primesBelow_sorted (start count : Nat) : List.Pairwise (fun (a b : Prime) => b.m < a.m) (primesBelow start count).toList

The supply contains strictly decreasing, and hence distinct, moduli.

theorem Hex.ZMod64.primesBelow_count {start : Nat} (hs : 2 ≤ start) (count : Nat) : (primesBelow start count).size = count ∨ ∃ (q : Prime), q ∈ primesBelow start count ∧ q.m = 2

A supply starting at least at two either fills its budget or includes two.