The Lucas test for primes

This file implements the Lucas test for primes (not to be confused with the Lucas-Lehmer test for Mersenne primes). A number a witnesses that n is prime if a has order n-1 in the multiplicative group of integers mod n. This is checked by verifying that a^(n-1) = 1 (mod n) and a^d ≠ 1 (mod n) for any divisor d | n - 1. This test is the basis of the Pratt primality certificate.

TODO

• Write a tactic that uses this theorem to generate Pratt primality certificates
• Integrate Pratt primality certificates into the norm_num primality verifier

Implementation notes

Note that the proof for lucas_primality relies on analyzing the multiplicative group modulo p. Despite this, the theorem still holds vacuously for p = 0 and p = 1. In these cases, we can take q to be any prime and see that hd does not hold, since a^((p-1)/q) reduces to 1.

theorem lucas_primality (p : ℕ) (a : ZMod p) (ha : a ^ (p - 1) = 1) (hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1) : Nat.Prime p

If a^(p-1) = 1 mod p, but a^((p-1)/q) ≠ 1 mod p for all prime factors q of p-1, then p is prime. This is true because a has order p-1 in the multiplicative group mod p, so this group must itself have order p-1, which only happens when p is prime.

theorem reverse_lucas_primality (p : ℕ) (hP : Nat.Prime p) : ∃ (a : ZMod p), a ^ (p - 1) = 1 ∧ ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1

If p is prime, then there exists an a such that a^(p-1) = 1 mod p and a^((p-1)/q) ≠ 1 mod p for all prime factors q of p-1. The multiplicative group mod p is cyclic, so a can be any generator of the group (which must have order p-1).

theorem lucas_primality_iff (p : ℕ) : Nat.Prime p ↔ ∃ (a : ZMod p), a ^ (p - 1) = 1 ∧ ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1

A number p is prime if and only if there exists an a such that a^(p-1) = 1 mod p and a^((p-1)/q) ≠ 1 mod p for all prime factors q of p-1.