Lucas primality certificates

Proves Nat.Prime p by the Lucas test from a primitive root and the prime factors of p - 1.

@[irreducible]

def Mathlib.Tactic.Primality.powMod (b e m : ℕ) : ℕ

A more kernel-efficient version of b ^ e % m, computed four bits of e at a time by Nat.pow. Replace with Nat.powMod once lean4#15167 is available.

Equations

• Mathlib.Tactic.Primality.powMod b e m = if e = 0 then 1 % m else (Mathlib.Tactic.Primality.powMod b (e / 16) m).pow 16 * b.pow (e % 16) % m

theorem Mathlib.Tactic.Primality.powMod_def (b e m : ℕ) : powMod b e m = b ^ e % m

@[csimp]

theorem Mathlib.Tactic.Primality.powMod_eq_natPowMod : powMod = Nat.powMod

Compiled code runs core's Nat.powMod in place of powMod since it is faster there.

def Mathlib.Tactic.Primality.lucasCheck (p a : ℕ) (factorization : List (ℕ × ℕ)) : Bool

lucasCheck p a factorization checks that a ^ (p - 1) % p = 1, that a ^ ((p - 1) / q) % p ≠ 1 for each (q, e) ∈ factorization, and that the q ^ e multiply to p - 1.

Equations

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

theorem Mathlib.Tactic.Primality.prime_of_lucasCheck {p a : ℕ} {factorization : List (ℕ × ℕ)} (hprime : ∀ f ∈ factorization, Nat.Prime f.1) (h : lucasCheck p a factorization = true) : Nat.Prime p

structure Mathlib.Tactic.Primality.LucasWitness : Type

A candidate witness of a Lucas certificate for a p, which is not recorded in the type.

• root : ℕ

  A primitive root of p.

• primeFactors : List ℕ

  The prime factors of p - 1.

def Mathlib.Tactic.Primality.LucasWitness.factorization? (w : LucasWitness) (p : ℕ) : Option (List (ℕ × ℕ))

The factorization of p - 1 into the prime factors of w, if each of them divides p - 1 and lucasCheck passes with the root of w.

Equations

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

def Mathlib.Tactic.Primality.certifyLucas (p root : ℕ) (factorization : List ((q : ℕ) × ℕ × Q(Nat.Prime «$q»))) : Q(Nat.Prime «$p»)

Proves Nat.Prime p from the primitive root root and the factorization of p - 1 in factorization, each prime factor with its exponent and proof of primality.

Equations

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