theorem fermat_little_theorem (p : ℕ) [Fact (Nat.Prime p)] (a : ZMod p) : a ^ p = a

Fermat's little theorem in ZMod p: for any element a, we have a ^ p = a when p is prime.

theorem totient_eq_sub_one_iff_prime (N : ℕ) (hN : 2 ≤ N) : N.totient = N - 1 ↔ Nat.Prime N

Euler's criterion for primality: an integer N ≥ 2 is prime iff its Euler totient equals N - 1.

def IsCarmichael (N : ℕ) : Prop

N is a Carmichael number if it is a composite integer greater than 1 for which every unit a in ZMod N satisfies a ^ (N - 1) = 1.

noncomputable def millerRabinS (N : ℕ) : ℕ

The exponent s in the Miller-Rabin decomposition N - 1 = 2^s * d, defined as the 2-adic valuation of N - 1.

noncomputable def millerRabinD (N : ℕ) : ℕ

The odd part d in the Miller-Rabin decomposition N - 1 = 2^s * d.

theorem millerRabin_decomp (N : ℕ) : N - 1 = 2 ^ millerRabinS N * millerRabinD N

The Miller-Rabin decomposition: N - 1 = 2 ^ millerRabinS N * millerRabinD N.

theorem sq_chain_dichotomy {R : Type u_1} [CommRing R] [IsDomain R] (x : R) (n : ℕ) (h : x ^ 2 ^ n = 1) : x = 1 ∨ ∃ i < n, x ^ 2 ^ i = -1

In an integral domain, if x ^ (2 ^ n) = 1, then either x = 1 or there exists i < n such that x ^ (2 ^ i) = -1. This is the algebraic core of the Miller-Rabin "square-root chain" argument.

theorem lemma_11_6 (p : ℕ) (hp : Nat.Prime p) (a : ZMod p) (ha : a ≠ 0) : Xor' (a ^ millerRabinD p = 1) (∃ i < millerRabinS p, a ^ (2 ^ i * millerRabinD p) = -1)

Lemma 11.6 (Sutherland): writing a prime p = 2^s t + 1 with t odd, for any integer a nonzero mod p, exactly one of the following holds: (i) a^t ≡ 1 (mod p); (ii) a^{2^i t} ≡ -1 (mod p) for some 0 ≤ i < s.

def IsMillerRabinWitness (N a : ℕ) : Prop

An integer a is a Miller-Rabin witness for the compositeness of N if a is nonzero mod N, a^d ≢ 1, and a^(2^r · d) ≢ -1 for every 0 ≤ r < s, where N - 1 = 2^s · d with d odd.

noncomputable def millerRabinWitnessSet (N : ℕ) : Finset ℕ

The set of Miller-Rabin witnesses in [1, N-1].

noncomputable def millerRabinLiarSet (N : ℕ) : Finset ℕ

The set of Miller-Rabin liars (non-witnesses) in [1, N-1].

theorem millerRabin_witness_liar_card (N : ℕ) : (millerRabinWitnessSet N).card + (millerRabinLiarSet N).card = (Finset.Icc 1 (N - 1)).card

The Miller-Rabin witness set and liar set together partition [1, N-1].

theorem zmod_ne_zero_of_mem_Icc {N : ℕ} (hN : N > 1) {a : ℕ} (ha : a ∈ Finset.Icc 1 (N - 1)) : ↑a ≠ 0

A residue from [1, N-1] is nonzero in ZMod N whenever N > 1.

theorem millerRabin_liar_coprime {N : ℕ} (hN : N > 1) {a : ℕ} (ha_mem : a ∈ millerRabinLiarSet N) : a.Coprime N

Any Miller-Rabin liar for N (with N > 1) is coprime to N.

theorem millerRabin_liar_bound (N : ℕ) (hN_odd : ¬2 ∣ N) (hN_composite : ¬Nat.Prime N) (hN_gt : N > 1) : 4 * (millerRabinLiarSet N).card ≤ N - 1

Miller-Rabin liar bound: for an odd composite N > 1, at most one quarter of the elements of [1, N-1] are liars.

theorem monier_rabin (N : ℕ) (hN_odd : ¬2 ∣ N) (hN_composite : ¬Nat.Prime N) (hN_gt : N > 1) : 4 * (millerRabinWitnessSet N).card ≥ 3 * (N - 1)

Theorem 11.8 (Monier-Rabin): For an odd composite integer N > 1, at least 3/4 of the integers in [1, N-1] are Miller-Rabin witnesses.

@[irreducible]

def twoAdicVal : ℕ → ℕ

The 2-adic valuation of a natural number, computed recursively by dividing by 2 while the input is even.

@[irreducible]

theorem two_pow_twoAdicVal_dvd (n : ℕ) : 2 ^ twoAdicVal n ∣ n

2 ^ twoAdicVal n divides n.

theorem twoAdicVal_decomp (n : ℕ) : n = 2 ^ twoAdicVal n * (n / 2 ^ twoAdicVal n)

n = 2 ^ twoAdicVal n * (n / 2 ^ twoAdicVal n): extracting the 2-adic factor of n.

def millerRabinStep (N a : ℕ) : Bool

One iteration of the Miller-Rabin primality test for a candidate N with a base a: succeeds iff a^d ≡ 1 or a^(2^r · d) ≡ -1 for some r < s, where N - 1 = 2^s · d.

def millerRabinTest (N : ℕ) (witnesses : List ℕ) : Bool

The full Miller-Rabin test: run millerRabinStep on each witness in the list and report true iff every one returns true.

theorem pow_two_pow_eq_one_or_neg_one {R : Type u_1} [Ring R] [NoZeroDivisors R] {x : R} {n : ℕ} (hx : x ^ 2 ^ n = 1) : x = 1 ∨ ∃ r < n, x ^ 2 ^ r = -1

In a ring with no zero divisors, if x ^ 2^n = 1, then x = 1 or there exists r < n such that x ^ 2^r = -1.

theorem millerRabin_decompose (N : ℕ) : N - 1 = 2 ^ millerRabinS N * millerRabinD N

The Miller-Rabin decomposition (restatement): N - 1 = 2 ^ millerRabinS N * millerRabinD N.

theorem millerRabinStep_true_of_prime (p : ℕ) [hp : Fact (Nat.Prime p)] {a : ℕ} (ha : ↑a ≠ 0) : millerRabinStep p a = true

The Miller-Rabin step always returns true on a true prime p with any base nonzero mod p.

def IsZeroModN (Pz : ℤ) (N : ℕ) : Prop

A projective z-coordinate Pz is zero modulo N if N divides Pz.

def IsNonzeroModN (Pz : ℤ) (N : ℕ) : Prop

A projective z-coordinate Pz is nonzero modulo N if N does not divide Pz.

def IsStronglyNonzeroModN (Pz : ℤ) (N : ℕ) : Prop

A projective z-coordinate Pz is strongly nonzero modulo N if gcd(Pz, N) = 1.

theorem not_dvd_of_stronglyNonzeroModN {Pz : ℤ} {N p : ℕ} (hstr : IsStronglyNonzeroModN Pz N) (hp : Nat.Prime p) (hpN : p ∣ N) : ¬↑p ∣ Pz

If Pz is strongly nonzero mod N and p is a prime divisor of N, then p ∤ Pz.

theorem isNonzeroModN_of_isStronglyNonzeroModN {Pz : ℤ} {N : ℕ} (hstr : IsStronglyNonzeroModN Pz N) (hN : 1 < N) : IsNonzeroModN Pz N

Strongly nonzero mod N implies nonzero mod N, provided N > 1.

theorem isStronglyNonzeroModN_iff_isNonzeroModN_of_prime {Pz : ℤ} {N : ℕ} (hN : Nat.Prime N) : IsStronglyNonzeroModN Pz N ↔ IsNonzeroModN Pz N

When N is prime, "strongly nonzero mod N" coincides with "nonzero mod N".

theorem fourth_root_mono {p N : ℕ} (hp2 : p ^ 2 ≤ N) : (√↑p + 1) ^ 2 ≤ (√√↑N + 1) ^ 2

Monotonicity used in the Goldwasser-Kilian bound: if p ^ 2 ≤ N, then (√p + 1)^2 ≤ (√√N + 1)^2.

structure GoldwasserKilianHyp (W : WeierstrassCurve ℤ) (N M : ℕ) (zMP : ℤ) (zMlP : ℕ → ℤ) : Prop

The hypotheses of the Goldwasser-Kilian primality criterion (Theorem 11.13 of Sutherland): N, M > 1, M > (N^{1/4}+1)^2, N coprime to the discriminant of W, the multiple MP is zero mod N, and (M/ℓ)P is strongly nonzero mod N for every prime ℓ ∣ M.

• hN : N > 1
• hM : M > 1
• hMbound : ↑M > (√√↑N + 1) ^ 2
• hcop : N.Coprime W.Δ.natAbs
• hzero : IsZeroModN zMP N
• hstrong (ℓ : ℕ) : Nat.Prime ℓ → ℓ ∣ M → IsStronglyNonzeroModN (zMlP ℓ) N

theorem disc_ne_zero_of_coprime_dvd (W : WeierstrassCurve ℤ) (N p : ℕ) (hcop : N.Coprime W.Δ.natAbs) (hp : Nat.Prime p) (hpN : p ∣ N) : (Int.castRingHom (ZMod p)) W.Δ ≠ 0

If N is coprime to the discriminant of W and p is a prime divisor of N, then the discriminant maps to a nonzero element of ZMod p.

theorem reduction_point_nsmul_properties (W : WeierstrassCurve ℤ) (N M : ℕ) (zMP : ℤ) (zMlP : ℕ → ℤ) (hM : M > 1) (hcop : N.Coprime W.Δ.natAbs) (hzero : IsZeroModN zMP N) (hstrong : ∀ (ℓ : ℕ), Nat.Prime ℓ → ℓ ∣ M → IsStronglyNonzeroModN (zMlP ℓ) N) (p : ℕ) (hp : Nat.Prime p) (hpN : p ∣ N) [Fact (Nat.Prime p)] : ∃ (Pbar : (W.map (Int.castRingHom (ZMod p))).toAffine.Point), M • Pbar = 0 ∧ ∀ (ℓ : ℕ), Nat.Prime ℓ → ℓ ∣ M → (M / ℓ) • Pbar ≠ 0

Under the Goldwasser-Kilian hypotheses, for any prime p ∣ N, the reduction of the point modulo p is annihilated by M and not by M/ℓ for any prime ℓ ∣ M.

theorem reduction_point_has_order (W : WeierstrassCurve ℤ) (N M : ℕ) (zMP : ℤ) (zMlP : ℕ → ℤ) (hM : M > 1) (hcop : N.Coprime W.Δ.natAbs) (hzero : IsZeroModN zMP N) (hstrong : ∀ (ℓ : ℕ), Nat.Prime ℓ → ℓ ∣ M → IsStronglyNonzeroModN (zMlP ℓ) N) (p : ℕ) (hp : Nat.Prime p) (hpN : p ∣ N) [Fact (Nat.Prime p)] : ∃ (Pbar : (W.map (Int.castRingHom (ZMod p))).toAffine.Point), addOrderOf Pbar = M

Under the Goldwasser-Kilian hypotheses, for any prime p ∣ N, the reduction of the point modulo p has additive order exactly M.

theorem hasse_order_bound_from_GK (W : WeierstrassCurve ℤ) (N M : ℕ) (zMP : ℤ) (zMlP : ℕ → ℤ) (hyp : GoldwasserKilianHyp W N M zMP zMlP) (p : ℕ) (hp : Nat.Prime p) (hpN : p ∣ N) : ↑M ≤ (√↑p + 1) ^ 2

Under the Goldwasser-Kilian hypotheses, for every prime p ∣ N the order parameter M is bounded by the Hasse interval upper bound (√p + 1)^2.

theorem goldwasser_kilian (W : WeierstrassCurve ℤ) (N M : ℕ) (zMP : ℤ) (zMlP : ℕ → ℤ) (hN : N > 1) (hM : M > 1) (hMbound : ↑M > (√√↑N + 1) ^ 2) (hcop : N.Coprime W.Δ.natAbs) (hzero : ↑N ∣ zMP) (hstrong : ∀ (ℓ : ℕ), Nat.Prime ℓ → ℓ ∣ M → (zMlP ℓ).gcd ↑N = 1) : Nat.Prime N

Theorem 11.13 (Goldwasser-Kilian, Sutherland): Let E/ℚ be an elliptic curve and M, N > 1 with M > (N^{1/4}+1)^2 and N coprime to Δ(E). If MP is zero mod N and (M/ℓ)P is strongly nonzero mod N for every prime ℓ ∣ M, then N is prime.