Pocklington's primality test, cube-root variant

The classic Pocklington test requires factoring a divisor F > √N of N - 1. This variant (due to Brillhart–Lehmer–Selfridge) only needs F > N^(1/3), at the cost of an additional divisibility sieve up to a small bound m and a non-square check on r² - 8s (where R = (N-1)/F and R = 2·F·s + r).

theorem Nat.prime_iff_not_exists_mul_eq' (p : ℕ) : Prime p ↔ 2 ≤ p ∧ ¬∃ (m : ℕ) (n : ℕ), 2 ≤ m ∧ m < p ∧ 2 ≤ n ∧ n < p ∧ m * n = p

theorem Nat.modEq_prod {ι : Type u_1} {s : Finset ι} {f g : ι → ℕ} {b : ℕ} (hb : ∀ i ∈ s, f i ≡ g i [MOD b]) : ∏ i ∈ s, f i ≡ ∏ i ∈ s, g i [MOD b]

theorem Nat.modEq_one_of_dvd_of_prime (n b : ℕ) (prime : ∀ (p : ℕ), Prime p → p ∣ n → p ≡ 1 [MOD b]) (d : ℕ) (hdn : d ∣ n) : d ≡ 1 [MOD b]

theorem Nat.modEq_iff_exists_mul_add {p q b : ℕ} (hqb : q < b) : p ≡ q [MOD b] ↔ ∃ (k : ℕ), k * b + q = p

theorem Nat.modEq_iff_exists_mul_add' {p q b : ℕ} (hqp : q ≤ p) : p ≡ q [MOD b] ↔ ∃ (k : ℕ), k * b + q = p

theorem Nat.add_sq_eq_dist_sq_add_four_mul (c d : ℕ) : (c + d) ^ 2 = (max c d - min c d) ^ 2 + 4 * (c * d)

def PrimeCert.Pocklington3Cert (r s : ℕ) : Prop

The non-square certificate: one of three conditions that rule out r² - 8s being a perfect square, which is needed to exclude composite factorisations.

Equations

• PrimeCert.Pocklington3Cert r s = (s = 0 ∨ ¬IsSquare (r ^ 2 - 8 * s) ∨ r ^ 2 < 8 * s)

theorem PrimeCert.pocklington3_test (N F R m r s : ℕ) (R_def : F * R + 1 = N) (r_def : R % (2 * F) = r) (s_def : R / (2 * F) = s) (h2n : 2 ≤ N) (odd_n : Odd N) (odd_R : Odd R) (primitive : ∀ p ∈ F.primeFactors, ∃ (a : ℕ), a ^ (N - 1) ≡ 1 [MOD N] ∧ (a ^ ((N - 1) / p) - 1).gcd N = 1) (divisors : ∀ (l : ℕ), 1 ≤ l → l < m → ¬l * F + 1 ∣ N) (bound : N + (m * F + 1) * (m * F) < (m * F + 1) * (2 * F ^ 2 + r * F + 1)) (cert : s = 0 ∨ ¬IsSquare (r ^ 2 - 8 * s) ∨ r ^ 2 < 8 * s) : Nat.Prime N

def PrimeCert.forallB (f : ℕ → Bool) (start len : ℕ) (step : ℕ := 1) : Bool

Equations

• PrimeCert.forallB f start len step = (Nat.rec (start, true) (fun (x : ℕ) (ih : ℕ × Bool) => Prod.rec (fun (i : ℕ) (b : Bool) => (eagerReduce (i.add step), f i && b)) ih) len).2

theorem PrimeCert.forallB_iff_range' (f : ℕ → Bool) (start len step : ℕ) : forallB f start len step = true ↔ ∀ n ∈ List.range' start len step, f n = true

theorem PrimeCert.forallB_iff (f : ℕ → Bool) (start len step : ℕ) : forallB f start len step = true ↔ ∀ n < len, f (n * step + start) = true

theorem PrimeCert.forallB_iff' (f : ℕ → Bool) (start r len step : ℕ) : forallB f (start * step + r) len step = true ↔ ∀ (n : ℕ), start ≤ n → n < start + len → f (n * step + r) = true

theorem PrimeCert.forallB_one_iff (f : ℕ → Bool) (start len : ℕ) : forallB f start len = true ↔ ∀ (n : ℕ), start ≤ n → n < start + len → f n = true

theorem PrimeCert.Pocklington3Cert.of_prime (r s p : ℕ) (hp : Nat.Prime p) (h2p : 2 < p) (cond : powMod (r ^ 2 - 8 * s) (p / 2) p = p - 1) : Pocklington3Cert r s

inductive PrimeCert.Pocklington3CertMode : Type

How to discharge the Pocklington3Cert obligation:

• zero: s = 0
• prime p hp: witness that r² - 8s is a quadratic non-residue mod p
• lt: r² < 8s

• zero : Pocklington3CertMode
• prime (p : ℕ) (hp : Nat.Prime p) : Pocklington3CertMode
• lt : Pocklington3CertMode

noncomputable def PrimeCert.Pocklington3CertMode.calculate (m : Pocklington3CertMode) (r s : ℕ) : Bool

Equations

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

theorem PrimeCert.Pocklington3CertMode.to_cert (m : Pocklington3CertMode) (r s : ℕ) (h : m.calculate r s = true) : Pocklington3Cert r s

structure PrimeCert.PrimePow : Type

• prime : ℕ
• pow : ℕ
• pf : Nat.Prime self.prime
• pow_ne_zero : Nat.blt 0 self.pow = true

noncomputable def PrimeCert.PrimePow.toNat (pp : PrimePow) : ℕ

Equations

• pp.toNat = PrimeCert.PrimePow.rec (fun (p v : ℕ) (x : Nat.Prime p) (x_1 : Nat.blt 0 v = true) => p.pow v) pp

@[simp]

theorem PrimeCert.PrimePow.toNat_def (pp : PrimePow) : pp.toNat = pp.prime ^ pp.pow

theorem PrimeCert.PrimePow.prime_dvd_toNat (pp : PrimePow) : pp.prime ∣ pp.toNat

noncomputable def PrimeCert.pocklington3_calculate (N e root m : ℕ) (F' : List PrimePow) (mode : Pocklington3CertMode) : Bool

Equations

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

theorem List.rec_and {α : Type u_1} (f : α → Bool) (b : Bool) (l : List α) : rec b (fun (hd : α) (x : List α) (ih : Bool) => f hd && ih) l = true ↔ b = true ∧ ∀ x ∈ l, f x = true

theorem PrimeCert.mem_primeFactors_prod_toNat (L : List PrimePow) (p : ℕ) : p ∈ (List.map PrimePow.toNat L).prod.primeFactors → ∃ pp ∈ L, pp.prime = p

theorem PrimeCert.of_gcd_pred_mod_eq_one (a b : ℕ) (h : (a % b - 1).gcd b = 1) (hb : 2 ≤ b) : (a - 1).gcd b = 1

theorem PrimeCert.pocklington3_certKR (N root m e : ℕ) (F' : List PrimePow) (mode : Pocklington3CertMode) (cert : pocklington3_calculate N e root m F' mode = true) : Nat.Prime N

Inputs (not all needed):

• N: the number to be certified as prime
• F: an even divisor of N-1, fully factored, to be given as a literal
• F': the odd part of F, given in factorised form
• e: the exponent of 2 in F, so that F = 2^e * F'
• R: the quotient (N-1)/F, odd, given as a literal.
• root: a pseudo-primitive root (for F)
• m: an arbitrary number (> 0), which should be small for better performance.
• s, r := divmod(R, 2*F), given as literals

def PrimeCert.Meta.pock3_mode : Lean.ParserDescr

Syntax for the non-square certificate mode in pock3:

• A numeric literal 0 means s = 0
• A numeric literal p (prime, p > 2) means r² - 8s is a quadratic non-residue mod p
• < means r² < 8s

Equations

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

def PrimeCert.Meta.parsePock3Mode (stx : Lean.TSyntax `PrimeCert.Meta.pock3_mode) (dict : PrimeDict) : Lean.MetaM Q(Pocklington3CertMode)

Equations

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

def PrimeCert.Meta.pock3_spec : Lean.ParserDescr

Syntax for a pock3 certificate step: (N, root, m, mode, F).

• N: the number to certify as prime
• root: a pseudo-primitive root (for the factored part of N - 1)
• m: sieve bound — all l * F + 1 for 1 ≤ l < m must not divide N (smaller m = less sieve work but requires larger F)
• mode: how to discharge the non-square condition (see pock3_mode)
• F: the even, fully-factored divisor of N - 1, written as 2 ^ e * p₁ ^ e₁ * p₂ * ... (the power of 2 must come first)

-- Certify 73471: root 3, sieve bound 1, non-square witness 7, F = 2 * 31
pock3 (73471, 3, 1, 7, 2 * 31)

-- With higher power of 2 and multiple odd factors:
pock3 (32560621, 2, 1, 7, 2 ^ 2 * 3 * 29)

Equations

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

def PrimeCert.Meta.PrimePow.base : PrimePow → ℕ

Equations

• (PrimeCert.Meta.PrimePow.prime p).base = p
• (PrimeCert.Meta.PrimePow.pow p e).base = p

def PrimeCert.Meta.parsePrimePow' (stx : Lean.TSyntax `PrimeCert.Meta.prime_pow) (dict : PrimeDict) : Lean.MetaM Q(PrimeCert.PrimePow)

Equations

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

def PrimeCert.Meta.parseFactored' (stx : Lean.TSyntax `PrimeCert.Meta.factored) (dict : PrimeDict) : Lean.MetaM Q(List PrimeCert.PrimePow)

Equations

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

def PrimeCert.Meta.parsePock3Spec : PrimeCertMethod `PrimeCert.Meta.pock3_spec

Equations

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

def PrimeCert.Meta.pock3 : PrimeCertExt

Equations

• PrimeCert.Meta.pock3 = { syntaxName := `PrimeCert.Meta.pock3_spec, methodName := `PrimeCert.Meta.parsePock3Spec }

def step_groupPock3_ : Lean.ParserDescr

Equations

• step_groupPock3_ = Lean.ParserDescr.node `step_groupPock3_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "pock3") PrimeCert.Meta.pock3_spec)

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

Equations

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