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)) ⋯ #[]