Pocklington's primality certificate

To use this certificate for primality of N, factorise N - 1 completely.

1. If the largest factor p is > √N, then set F₁ = p.
2. Otherwise, set F₁ to be the product of enough prime factors to be > √N.
3. Then, find a primitive root a of N.
4. Then a will satisfy the conditions required, which are:

• a ^ (N - 1) ≡ 1 (mod N)
• For each prime factor p of F₁, gcd(a ^ ((N - 1) / p) - 1, N) = 1.

theorem List.pairwise_iff_toFinset {α : Type u_1} {β : Type u_2} (l : List α) (hl : l.Nodup) (P : β → β → Prop) (hp : Symmetric P) (e : α → β) [DecidableEq α] : Pairwise (Function.onFun P e) l ↔ _root_.Pairwise (Function.onFun P fun (i : ↥l.toFinset) => e ↑i)

theorem Nat.modEq_finset_prod_iff {a b : ℕ} {ι : Type u_1} (s : Finset ι) (e : ι → ℕ) (co : Pairwise (Function.onFun Coprime fun (i : ↥s) => e ↑i)) : a ≡ b [MOD s.prod e] ↔ ∀ i ∈ s, a ≡ b [MOD e i]

theorem multiplicity_zero_right {α : Type u_1} [MonoidWithZero α] (x : α) : multiplicity x 0 = 1

theorem Nat.modEq_iff_forall_prime_dvd {a b n : ℕ} : a ≡ b [MOD n] ↔ ∀ (p : ℕ), p ∣ n → Prime p → a ≡ b [MOD p ^ multiplicity p n]

theorem Nat.pow_multiplicity_dvd_of_dvd_of_not_dvd_div {q n x : ℕ} (hq : Prime q) (hxn : x ∣ n) (hxnq : ¬x ∣ n / q) : q ^ multiplicity q n ∣ x

theorem pocklington_test (N F₁ : ℕ) (hn₀ : 0 < N) (hf₁ : F₁ ∣ N - 1) (primitive : ∀ p ∈ F₁.primeFactors, ∃ (a : ℕ), a ^ (N - 1) ≡ 1 [MOD N] ∧ (a ^ ((N - 1) / p) - 1).gcd N = 1) (p : ℕ) (hp : Nat.Prime p) (hpn : p ∣ N) : p ≡ 1 [MOD F₁]

Let N be a natural number whose primality we want to certify. Assume we have a partial factorisation N - 1 = F₁ * R₁, where F₁ is fully factorised with prime factors pᵢ. Now for each pᵢ find a pseudo-primitive root aᵢ such that aᵢ ^ (N - 1) ≡ 1 (mod N) and gcd(aᵢ ^ ((N - 1) / pᵢ) - 1, N) = 1. Then any prime factor n of N satisfies n ≡ 1 (mod F₁).

def PocklingtonPred (N root F₁ : ℕ) : Prop

The Pocklington primitive-root predicate: for each prime factor p of F₁, gcd(root ^ ((N-1)/p) - 1, N) = 1. Built incrementally by PocklingtonPred.step.

Equations

• PocklingtonPred N root F₁ = ∀ p ∈ F₁.primeFactors, (root ^ ((N - 1) / p) - 1).gcd N = 1

theorem pocklington_certify (N F₁ : ℕ) (h2n : 2 ≤ N) (hf₁ : F₁ ∣ N - 1) (hf₁' : N.sqrt < F₁) (root : ℕ) (psp : root ^ (N - 1) ≡ 1 [MOD N]) (primitive : PocklingtonPred N root F₁) : Nat.Prime N

theorem pocklington_certifyKR (N root F₁ : ℕ) (primitive : PocklingtonPred N root F₁) (psp : (powModTR root N.pred N).beq 1 = true := by exact eagerReduce (Eq.refl true)) (h2n : Nat.ble 2 N = true := by exact eagerReduce (Eq.refl true)) (hf₁ : (N.pred.mod F₁).beq 0 = true := by exact eagerReduce (Eq.refl true)) (hf₁' : N.blt (F₁.mul F₁) = true := by exact eagerReduce (Eq.refl true)) : Nat.Prime N

@[simp]

theorem PocklingtonPred.zero {N root : ℕ} : PocklingtonPred N root 0

@[simp]

theorem PocklingtonPred.one {N root : ℕ} : PocklingtonPred N root 1

theorem PocklingtonPred.step_pow {N root F₂ p e : ℕ} (hp : Nat.Prime p) (ih : PocklingtonPred N root F₂) (step : ((predModKR (powModTR root (N.pred.div p) N) N).gcd N).beq 1 = true := by exact eagerReduce (Eq.refl true)) (hroot : Nat.blt 0 root = true := by exact eagerReduce (Eq.refl true)) : PocklingtonPred N root (F₂.mul (p.pow e))

theorem PocklingtonPred.step {N root F₂ p : ℕ} (hp : Nat.Prime p) (ih : PocklingtonPred N root F₂) (step : ((predModKR (powModTR root (N.pred.div p) N) N).gcd N).beq 1 = true := by exact eagerReduce (Eq.refl true)) (hroot : Nat.blt 0 root = true := by exact eagerReduce (Eq.refl true)) : PocklingtonPred N root (F₂.mul p)

theorem PocklingtonPred.base_pow {N root p e : ℕ} (hp : Nat.Prime p) (step : ((predModKR (powModTR root (N.pred.div p) N) N).gcd N).beq 1 = true := by exact eagerReduce (Eq.refl true)) (hroot : Nat.blt 0 root = true := by exact eagerReduce (Eq.refl true)) : PocklingtonPred N root (p.pow e)

theorem PocklingtonPred.base {N root p : ℕ} (hp : Nat.Prime p) (step : ((predModKR (powModTR root (N.pred.div p) N) N).gcd N).beq 1 = true := by exact eagerReduce (Eq.refl true)) (hroot : Nat.blt 0 root = true := by exact eagerReduce (Eq.refl true)) : PocklingtonPred N root p

def PrimeCert.Meta.prime_pow : Lean.ParserDescr

A prime power is represented by either p ^ e or p.

Equations

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

inductive PrimeCert.Meta.PrimePow : Type

• prime (p : ℕ) : PrimePow
• pow (p e : ℕ) : PrimePow

instance PrimeCert.Meta.instToMessageDataPrimePow : Lean.ToMessageData PrimePow

Equations

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

def PrimeCert.Meta.parsePrimePow (stx : Lean.TSyntax `PrimeCert.Meta.prime_pow) : Q(ℕ) × PrimePow

Equations

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

def PrimeCert.Meta.factored : Lean.ParserDescr

A full factorisation of a number, written like 3 ^ 4 * 29 * 41.

Equations

• PrimeCert.Meta.factored = Lean.ParserDescr.nodeWithAntiquot "factored" `PrimeCert.Meta.factored (PrimeCert.Meta.prime_pow.sepBy1 " * " (Lean.ParserDescr.symbol " * "))

def PrimeCert.Meta.parseFactored (stx : Lean.TSyntax `PrimeCert.Meta.factored) : Q(ℕ) × Array PrimePow

Equations

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

def PrimeCert.Meta.mkPockPred (N a F₁ : Q(ℕ)) (steps : Array PrimePow) (dict : PrimeDict) : Lean.MetaM Q(PocklingtonPred «$N» «$a» «$F₁»)

Equations

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

def PrimeCert.Meta.pock_spec : Lean.ParserDescr

Syntax for a pock certificate step: (N, root, F₁).

• N: the number to certify as prime
• root: a value satisfying root ^ (N-1) ≡ 1 (mod N) and the GCD conditions
• F₁: a fully-factored divisor of N - 1 with F₁ > √N, written as p₁ ^ e₁ * p₂ * ...

All prime factors appearing in F₁ must already be in the PrimeDict (certified by earlier small or pock steps).

-- In a pock% or prime_cert% call:
pock (339392917, 2, 3 ^ 4 * 29 * 41)
pock (16290860017, 5, 339392917)

Equations

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

def PrimeCert.Meta.parsePockSpec : PrimeCertMethod `PrimeCert.Meta.pock_spec

Equations

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

def PrimeCert.Meta.PrimeCertExt.pock : PrimeCertExt

Equations

• PrimeCert.Meta.PrimeCertExt.pock = { syntaxName := `PrimeCert.Meta.pock_spec, methodName := `PrimeCert.Meta.parsePockSpec }

def «step_groupPock{_;}» : Lean.ParserDescr

Equations

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

def step_groupPock_ : Lean.ParserDescr

Equations

• step_groupPock_ = Lean.ParserDescr.node `step_groupPock_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "pock") PrimeCert.Meta.pock_spec)

def PrimeCert.«termPock%[_,,;_,,]» : Lean.ParserDescr

Convenience elaborator combining small and pock steps into a single term.

Syntax: pock% [small_primes; pock_steps]

• Before the ;: comma-separated small prime literals whose primality is already known (looked up as PrimeCert.prime_<n> declarations, e.g. PrimeCert.prime_31).
• After the ;: comma-separated Pocklington steps (N, root, F₁) where:
  • N is the number to certify
  • root is a pseudo-primitive root of N
  • F₁ is a factored divisor of N - 1 with F₁ > √N, written as p₁ ^ e₁ * p₂ * ...

Steps are processed in order; each step can reference primes certified by earlier steps. The last step's N becomes the certified prime.

-- Certify 31: declare small primes 2, 3; then one Pocklington step
theorem prime_31 : Nat.Prime 31 := pock% [2, 3; (31, 3, 2 * 3)]

-- Multi-step ladder: small primes, then intermediate, then target
theorem prime_16290860017 : Nat.Prime 16290860017 :=
  pock% [3, 29, 41; (339392917, 2, 3 ^ 4 * 29 * 41), (16290860017, 5, 339392917)]

Equations

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