Miller–Rabin primality test

DefinitionSplitting off the power of two#✓fully proved

For a natural number \(m > 0\), the two-adic split of \(m\) is the pair \((t, u)\) of natural numbers with \(m = 2^t u\) and \(u\) odd. For \(m = 0\) it is \((0, 0)\).

def twoAdicSplit (m : ℕ) : ℕ × ℕ :=
  if m ≠ 0 ∧ m % 2 = 0 then
    let r := twoAdicSplit (m / 2)
    (r.1 + 1, r.2)
  else (0, m)
termination_by m
decreasing_by omega
Used by 8
Used byAt most half the bases are non-witnesses for a Carmichael number · At most a quarter of the bases are non-witnesses for a Carmichael number · At most a quarter of the bases are non-witnesses when some unit fails Fermat's test and the modulus is not a prime power · Miller–Rabin witness test · What a non-witness satisfies · A prime has no Miller–Rabin witnesses in range · Fermat witnesses are Miller–Rabin witnesses · Cost of the Miller–Rabin witness test

DefinitionThe Miller–Rabin squaring loop#✓fully proved

Fix a modulus \(n\). With no squarings remaining, the loop at the current value \(x\) reports a witness exactly when \(x \ne 1\), at no cost. With \(k + 1\) squarings remaining, it costs one modular multiplication and computes \(y = x^2 \bmod n\); it reports a witness if \(y = 1\), \(x \ne 1\) and \(x \ne n - 1\), and otherwise continues at \(y\) with \(k\) squarings remaining.

Here \(x^2 \bmod 0 = x^2\), and \(n - 1\) is \(0\) when \(n = 0\).

def witnessLoop (n : ℕ) : ℕ → ℕ → TimeM ℕ Bool
  | 0, x => pure (x != 1)
  | k + 1, x => do
      ✓
      let y := x * x % n
      if y = 1 ∧ x ≠ 1 ∧ x ≠ n - 1 then pure true else witnessLoop n k y
Used by 9
Used byMiller–Rabin witness test · What a non-witness satisfies · A prime has no Miller–Rabin witnesses in range · The squaring loop modulo a prime finds no witness when it ends at 1 · When the squaring loop finds no witness · The squaring loop reports a witness when it does not end at 1 · Cost bound for the Miller–Rabin squaring loop · Fermat witnesses are Miller–Rabin witnesses · Cost of the Miller–Rabin witness test

DefinitionMiller–Rabin witness test#✓fully proved

For natural numbers \(a\) and \(n\), write \(n - 1 = 2^t u\) with \(u\) odd (here \(n - 1\) is truncated at \(0\), and \(t = u = 0\) when \(n \le 1\)). The test sets \(x_0\) to the result of modular exponentiation of \(a\) to the power \(u\) modulo \(n\), which is \(a^u \bmod n\) when \(u > 0\) and \(1\) when \(u = 0\). For \(i = 1, \dots, t\) it computes \(x_i = x_{i-1}^2 \bmod n\) and returns true as soon as \(x_i = 1\), \(x_{i-1} \ne 1\) and \(x_{i-1} \ne n - 1\). If no such step occurs, it returns true exactly when \(x_t \ne 1\). Its cost is the cost of the modular exponentiation plus one for each squaring performed.

For a base with \(0 < a < n\), the answer true proves that \(n\) is composite; outside that range the answer carries no such guarantee (for example, the test returns true for \(a = n = 2\)), as in CLRS, whose bases are drawn from \(1, \dots, n - 1\).

def witness (a n : ℕ) : TimeM ℕ Bool := do
  let tu := twoAdicSplit (n - 1)
  let x ← modularExponentiation a tu.2 n
  witnessLoop n tu.1 x
Uses 3 · Used by 17
Statement usesSplitting off the power of two · The Miller–Rabin squaring loop · Modular exponentiation
Used byHalf error bound for Miller–Rabin with several bases · Quarter error bound for Miller–Rabin with several bases · At most half the bases are non-witnesses for a Carmichael number · At most half the bases are non-witnesses when some unit fails Fermat's test · At most a quarter of the bases are non-witnesses for a Carmichael number · At most a quarter of the bases are non-witnesses when some unit fails Fermat's test and the modulus is not a prime power · At most a quarter of the bases are non-witnesses for an odd prime power · Non-witnesses pass Fermat's test and are units · The Miller–Rabin test · Miller–Rabin answers prime exactly when no base is a witness · The Miller–Rabin test never rejects a prime when its bases lie in range · Non-witnesses of a number · A Miller–Rabin witness in range proves compositeness · What a non-witness satisfies · A prime has no Miller–Rabin witnesses in range · Fermat witnesses are Miller–Rabin witnesses · Cost of the Miller–Rabin witness test

DefinitionThe Miller–Rabin test#✓fully proved

Given a natural number \(n\) and a list of bases \(a_1, \dots, a_s\), the test runs the witness test for \(n\) on each base in turn. It answers composite as soon as some base \(a_i\) is a witness to the compositeness of \(n\), and prime if none is (in particular on the empty list). Its cost is the sum of the costs of the witness tests it runs.

This is CLRS MILLER-RABIN(n, s) with the bases given explicitly instead of drawn by RANDOM(1, n - 1). A composite answer is guaranteed correct only when every base lies in \(1, \dots, n - 1\).

def millerRabin (n : ℕ) : List ℕ → TimeM ℕ Bool
  | [] => pure true
  | a :: as => do
      let w ← witness a n
      if w then pure false else millerRabin n as
Uses 1 · Used by 5
Statement usesMiller–Rabin witness test
Used byHalf error bound for Miller–Rabin with several bases · Quarter error bound for Miller–Rabin with several bases · Miller–Rabin answers prime exactly when no base is a witness · The Miller–Rabin test never rejects a prime when its bases lie in range · With bases in range, a composite answer of the Miller–Rabin test is correct

TheoremCost bound for the Miller–Rabin squaring loop#✓fully proved

For all natural numbers \(n\), \(k\) and \(x\), the cost of the squaring loop modulo \(n\) started at \(x\) with \(k\) squarings remaining is at most \(k\).

@[simp]
theorem witnessLoop_time_le (n k x : ℕ) : (witnessLoop n k x).time ≤ k
Uses 1 · Used by 1
Statement usesThe Miller–Rabin squaring loop
Used byCost of the Miller–Rabin witness test

TheoremCost of the Miller–Rabin witness test#✓fully proved

For natural numbers \(a\) and \(n\), write \(n - 1 = 2^t u\) with \(u\) odd (here \(n - 1\) is truncated at \(0\), and \(t = u = 0\) when \(n \le 1\)). The cost of the witness test on base \(a\) and modulus \(n\) is at most the cost of the modular exponentiation of \(a\) to the power \(u\) modulo \(n\) plus \(t\): at most one multiplication for each of the \(t\) squarings.

theorem witness_time_le (a n : ℕ) :
    (witness a n).time ≤ (modularExponentiation a (twoAdicSplit (n - 1)).2 n).time +
      (twoAdicSplit (n - 1)).1
Uses 5
Statement usesSplitting off the power of two · Miller–Rabin witness test · Modular exponentiation
Proof usesThe Miller–Rabin squaring loop · Cost bound for the Miller–Rabin squaring loop

TheoremThe squaring loop modulo a prime finds no witness when it ends at 1#✓fully proved

Let \(p\) be a prime and let \(k\) and \(x\) be natural numbers with \(x < p\) and \(x^{2^k} \bmod p = 1\). Then the squaring loop modulo \(p\) started at \(x\) with \(k\) squarings remaining reports no witness.

theorem witnessLoop_eq_false {p : ℕ} (hp : p.Prime) :
    ∀ k x, x < p → x ^ (2 ^ k) % p = 1 → (witnessLoop p k x).ret = false
Uses 1 · Used by 1
Statement usesThe Miller–Rabin squaring loop
Used byA prime has no Miller–Rabin witnesses in range

TheoremA prime has no Miller–Rabin witnesses in range#✓fully proved

Let \(n\) be a prime and \(a\) a natural number with \(0 < a < n\). Then the witness test does not report \(a\) as a witness to the compositeness of \(n\).

theorem witness_eq_false_of_prime {n a : ℕ} (hn : n.Prime) (ha : 0 < a) (han : a < n) :
    (witness a n).ret = false
Sources
  • CLRS Section 31.8.
Uses 6 · Used by 2
Statement usesMiller–Rabin witness test
Proof usesSplitting off the power of two · The Miller–Rabin squaring loop · The squaring loop modulo a prime finds no witness when it ends at 1 · Modular exponentiation · Correctness of modular exponentiation
Used byThe Miller–Rabin test never rejects a prime when its bases lie in range · A Miller–Rabin witness in range proves compositeness

TheoremA Miller–Rabin witness in range proves compositeness#✓fully proved

Let \(n\) and \(a\) be natural numbers with \(0 < a < n\). If the witness test reports \(a\) as a witness to the compositeness of \(n\), then \(n\) is not prime.

theorem not_prime_of_witness {n a : ℕ} (ha : 0 < a) (han : a < n)
    (h : (witness a n).ret = true) : ¬ n.Prime
Uses 2
Statement usesMiller–Rabin witness test
Proof usesA prime has no Miller–Rabin witnesses in range

TheoremThe Miller–Rabin test never rejects a prime when its bases lie in range#✓fully proved

Let \(n\) be a prime. For every list of bases \(a_1, \dots, a_s\) (possibly empty) with \(0 < a_i < n\) for each \(i\), the Miller–Rabin test run on \(n\) with these bases answers prime.

theorem millerRabin_of_prime {n : ℕ} (hn : n.Prime) :
    ∀ bases : List ℕ, (∀ a ∈ bases, 0 < a ∧ a < n) → (millerRabin n bases).ret = true
Uses 3 · Used by 1
Statement usesThe Miller–Rabin test
Proof usesMiller–Rabin witness test · A prime has no Miller–Rabin witnesses in range
Used byWith bases in range, a composite answer of the Miller–Rabin test is correct

TheoremWith bases in range, a composite answer of the Miller–Rabin test is correct#✓fully proved

Let \(n\) be a natural number and \(a_1, \dots, a_s\) a list of bases with \(0 < a_i < n\) for each \(i\). If the Miller–Rabin test run on \(n\) with these bases answers composite, then \(n\) is not prime.

theorem not_prime_of_millerRabin_eq_false {n : ℕ} {bases : List ℕ}
    (hb : ∀ a ∈ bases, 0 < a ∧ a < n) (h : (millerRabin n bases).ret = false) : ¬ n.Prime
Uses 2
Statement usesThe Miller–Rabin test
Proof usesThe Miller–Rabin test never rejects a prime when its bases lie in range

TheoremThe squaring loop reports a witness when it does not end at 1#✓fully proved

Let \(n\), \(k\) and \(x\) be natural numbers with \(n > 0\), \(x < n\) and \(x^{2^k} \bmod n \ne 1\). Then the squaring loop modulo \(n\) started at \(x\) with \(k\) squarings remaining reports a witness.

theorem witnessLoop_eq_true {n : ℕ} (hn : 0 < n) :
    ∀ k x, x < n → x ^ (2 ^ k) % n ≠ 1 → (witnessLoop n k x).ret = true
Uses 1 · Used by 1
Statement usesThe Miller–Rabin squaring loop
Used byFermat witnesses are Miller–Rabin witnesses

TheoremFermat witnesses are Miller–Rabin witnesses#✓fully proved

Let \(a\) and \(n\) be natural numbers with \(n > 1\). If \(a^{n-1} \bmod n \ne 1\), that is, \(a^{n-1} \not\equiv 1 \pmod{n}\), then the Miller–Rabin witness test on base \(a\) and modulus \(n\) returns true.

theorem witness_of_pow_ne_one {n a : ℕ} (hn : 1 < n) (h : a ^ (n - 1) % n ≠ 1) :
    (witness a n).ret = true
Uses 6 · Used by 1
Statement usesMiller–Rabin witness test
Proof usesSplitting off the power of two · The Miller–Rabin squaring loop · The squaring loop reports a witness when it does not end at 1 · Modular exponentiation · Correctness of modular exponentiation
Used byNon-witnesses pass Fermat's test and are units

TheoremWhen the squaring loop finds no witness#✓fully proved

Let \(n\), \(k\) and \(x\) be natural numbers with \(x < n\). If the Miller–Rabin squaring loop modulo \(n\), started at \(x\) with \(k\) squarings to perform, reports no witness, then \(x = 1\) or \(x^{2^i} \equiv -1 \pmod n\) for some \(i < k\).

theorem witnessLoop_eq_false_imp {n : ℕ} :
    ∀ k x, x < n → (witnessLoop n k x).ret = false →
      x = 1 ∨ ∃ i < k, x ^ (2 ^ i) % n = n - 1
Uses 1 · Used by 1
Statement usesThe Miller–Rabin squaring loop
Used byWhat a non-witness satisfies

TheoremWhat a non-witness satisfies#✓fully proved

Let \(n > 1\) and write \(n - 1 = 2^t u\) with \(u\) odd. If \(a\) is a natural number for which the Miller–Rabin witness test \(\mathrm{WITNESS}(a, n)\) returns false, then \(a^u \equiv 1 \pmod n\), or \(a^{2^i u} \equiv -1 \pmod n\) for some \(i < t\).

theorem witness_eq_false_imp {n a : ℕ} (hn : 1 < n) (h : (witness a n).ret = false) :
    a ^ (twoAdicSplit (n - 1)).2 % n = 1 ∨
      ∃ i < (twoAdicSplit (n - 1)).1, a ^ (2 ^ i * (twoAdicSplit (n - 1)).2) % n = n - 1
Uses 6 · Used by 3
Statement usesSplitting off the power of two · Miller–Rabin witness test
Proof usesThe Miller–Rabin squaring loop · When the squaring loop finds no witness · Modular exponentiation · Correctness of modular exponentiation
Used byAt most half the bases are non-witnesses for a Carmichael number · At most a quarter of the bases are non-witnesses for a Carmichael number · At most a quarter of the bases are non-witnesses when some unit fails Fermat's test and the modulus is not a prime power

TheoremNon-witnesses pass Fermat's test and are units#✓fully proved

Let \(n > 1\) and let \(a\) be a natural number such that the witness test \(\mathrm{WITNESS}(a, n)\) returns false. Then \(a^{n-1} \equiv 1 \pmod n\) and \(a\) is coprime to \(n\).

theorem coprime_of_witness_eq_false {n a : ℕ} (hn : 1 < n) (h : (witness a n).ret = false) :
    a ^ (n - 1) % n = 1 ∧ a.Coprime n
Uses 2 · Used by 5
Statement usesMiller–Rabin witness test
Proof usesFermat witnesses are Miller–Rabin witnesses
Used byAt most half the bases are non-witnesses for a Carmichael number · At most half the bases are non-witnesses when some unit fails Fermat's test · At most a quarter of the bases are non-witnesses for a Carmichael number · At most a quarter of the bases are non-witnesses when some unit fails Fermat's test and the modulus is not a prime power · At most a quarter of the bases are non-witnesses for an odd prime power

DefinitionNon-witnesses of a number#✓fully proved

For a natural number \(n\), the non-witnesses of \(n\) form the finite set of bases \(a\) with \(0 < a < n\) for which the Miller–Rabin witness test \(\mathrm{WITNESS}(a, n)\) returns false, that is, the bases that do not witness the compositeness of \(n\).

def nonwitnesses (n : ℕ) : Finset ℕ := (Finset.Ioo 0 n).filter fun a => (witness a n).ret = false
Uses 1 · Used by 9
Statement usesMiller–Rabin witness test
Used byHalf error bound for Miller–Rabin with several bases · Quarter error bound for Miller–Rabin with several bases · At most half the bases are non-witnesses · At most half the bases are non-witnesses for a Carmichael number · At most half the bases are non-witnesses when some unit fails Fermat's test · At most a quarter of the bases are non-witnesses · At most a quarter of the bases are non-witnesses for a Carmichael number · At most a quarter of the bases are non-witnesses when some unit fails Fermat's test and the modulus is not a prime power · At most a quarter of the bases are non-witnesses for an odd prime power

TheoremAt most half the bases are non-witnesses when some unit fails Fermat's test#✓fully proved

Let \(n > 1\), and suppose some \(x\) coprime to \(n\) has \(x^{n-1} \not\equiv 1 \pmod n\). Then at most \((n - 1)/2\) of the bases \(1, \dots, n - 1\) are non-witnesses for \(n\).

The proof shows that the non-witnesses lie in the proper subgroup \(\{y : y^{n-1} = 1\}\) of \((\mathbb{Z}/n\mathbb{Z})^\times\).

theorem card_nonwitnesses_le_of_pow_ne_one {n x : ℕ} (hn : 1 < n) (hx : x.Coprime n)
    (hfx : x ^ (n - 1) % n ≠ 1) : (nonwitnesses n).card ≤ (n - 1) / 2
Uses 3 · Used by 1
Statement usesNon-witnesses of a number
Proof usesNon-witnesses pass Fermat's test and are units · Miller–Rabin witness test
Used byAt most half the bases are non-witnesses

TheoremAt most half the bases are non-witnesses for a Carmichael number#✓fully proved

Let \(n\) be a Carmichael number: \(n > 2\), \(n\) is not prime, and \(b^{n-1} \equiv 1 \pmod n\) for every \(b\) coprime to \(n\). Then at most \((n - 1)/2\) of the bases \(1, \dots, n - 1\) are non-witnesses for \(n\).

The proof shows that the non-witnesses lie in a proper subgroup of \((\mathbb{Z}/n\mathbb{Z})^\times\).

theorem card_nonwitnesses_le_of_carmichael {n : ℕ} (hC : n.IsCarmichael) :
    (nonwitnesses n).card ≤ (n - 1) / 2
Sources
  • CLRS, third edition, Theorem 31.38, case 2.
Uses 5 · Used by 1
Statement usesNon-witnesses of a number
Proof usesNon-witnesses pass Fermat's test and are units · Splitting off the power of two · Miller–Rabin witness test · What a non-witness satisfies
Used byAt most half the bases are non-witnesses

TheoremAt most half the bases are non-witnesses#✓fully proved

Let \(n > 1\) be odd and not prime. Then at most \((n - 1)/2\) of the bases \(1, \dots, n - 1\) are non-witnesses for \(n\); equivalently, at least \((n - 1)/2\) of them are witnesses to the compositeness of \(n\).

theorem card_nonwitnesses_le {n : ℕ} (hn : 1 < n) (hodd : n % 2 = 1) (hcomp : ¬ n.Prime) :
    (nonwitnesses n).card ≤ (n - 1) / 2
Sources
  • CLRS, third edition, Theorem 31.38.
Uses 3 · Used by 1
Statement usesNon-witnesses of a number
Proof usesAt most half the bases are non-witnesses for a Carmichael number · At most half the bases are non-witnesses when some unit fails Fermat's test
Used byHalf error bound for Miller–Rabin with several bases

TheoremMiller–Rabin answers prime exactly when no base is a witness#✓fully proved

For every natural number \(n\) and every list of bases, the Miller–Rabin test on \(n\) with these bases answers prime if and only if, for every base \(a\) in the list, the witness test \(\mathrm{WITNESS}(a, n)\) returns false, that is, \(a\) is not a witness to the compositeness of \(n\).

theorem millerRabin_eq_true_iff (n : ℕ) :
    ∀ bases : List ℕ, (millerRabin n bases).ret = true ↔ ∀ a ∈ bases, (witness a n).ret = false
Uses 2 · Used by 2
Statement usesThe Miller–Rabin test · Miller–Rabin witness test
Used byHalf error bound for Miller–Rabin with several bases · Quarter error bound for Miller–Rabin with several bases

TheoremHalf error bound for Miller–Rabin with several bases#✓fully proved

Let \(n > 1\) be odd and not prime, and let \(s\) be a natural number. Among the \((n - 1)^s\) lists \((b_1, \dots, b_s)\) of bases with \(0 < b_i < n\), at most \(((n - 1)/2)^s\) make the Miller–Rabin test of \(n\) with bases \(b_1, \dots, b_s\) answer prime.

With uniformly random bases the error probability is therefore at most \(2^{-s}\).

theorem card_millerRabin_errors_le {n : ℕ} (hn : 1 < n) (hodd : n % 2 = 1) (hcomp : ¬ n.Prime)
    (s : ℕ) :
    ((Fintype.piFinset fun _ : Fin s => Finset.Ioo 0 n).filter
        fun b => (millerRabin n (List.ofFn b)).ret = true).card ≤ ((n - 1) / 2) ^ s
Sources
  • CLRS, third edition, Theorem 31.39, in counting form.
Uses 5
Statement usesThe Miller–Rabin test
Proof usesAt most half the bases are non-witnesses · Miller–Rabin answers prime exactly when no base is a witness · Non-witnesses of a number · Miller–Rabin witness test

TheoremAt most a quarter of the bases are non-witnesses when some unit fails Fermat's test and the modulus is not a prime power#✓fully proved

At most a quarter of the bases are non-witnesses when some unit fails Fermat's test and the modulus is not a prime power. Let \(n > 1\) be odd and not prime, and not of the form \(p^e\) with \(p\) prime and \(e \ge 2\). Suppose some \(z\) coprime to \(n\) has \(z^{n-1} \not\equiv 1 \pmod n\). Then at most \((n - 1)/4\) of the bases \(1, \dots, n - 1\) are non-witnesses for \(n\).

theorem card_nonwitnesses_le_quarter_of_pow_ne_one {n z : ℕ} (hn : 1 < n) (hodd : n % 2 = 1)
    (hcomp : ¬ n.Prime) (hpow : ∀ p e, p.Prime → 2 ≤ e → n ≠ p ^ e) (hz : z.Coprime n)
    (hfz : z ^ (n - 1) % n ≠ 1) : (nonwitnesses n).card ≤ (n - 1) / 4
Uses 5 · Used by 1
Statement usesNon-witnesses of a number
Proof usesNon-witnesses pass Fermat's test and are units · Splitting off the power of two · Miller–Rabin witness test · What a non-witness satisfies
Used byAt most a quarter of the bases are non-witnesses

TheoremAt most a quarter of the bases are non-witnesses for a Carmichael number#✓fully proved

Let \(n\) be a Carmichael number: \(n > 2\), \(n\) is not prime, and \(b^{n-1} \equiv 1 \pmod n\) for every \(b\) coprime to \(n\). Then at most \((n - 1)/4\) of the bases \(1, \dots, n - 1\) are non-witnesses for \(n\).

The proof splits \(n\) into three pairwise coprime factors greater than \(1\) and finds four distinct cosets of a subgroup of \((\mathbb{Z}/n\mathbb{Z})^\times\) that holds the non-witnesses.

theorem card_nonwitnesses_le_quarter_of_carmichael {n : ℕ} (hC : n.IsCarmichael) :
    (nonwitnesses n).card ≤ (n - 1) / 4
Uses 5 · Used by 1
Statement usesNon-witnesses of a number
Proof usesNon-witnesses pass Fermat's test and are units · Splitting off the power of two · Miller–Rabin witness test · What a non-witness satisfies
Used byAt most a quarter of the bases are non-witnesses

TheoremAt most a quarter of the bases are non-witnesses for an odd prime power#✓fully proved

Let \(p\) be a prime and \(k \ge 2\) with \(p^k\) odd. Then at most \((p^k - 1)/4\) of the bases \(1, \dots, p^k - 1\) are non-witnesses for \(p^k\).

The proof shows that there are at most \(p - 1\) non-witnesses: they satisfy \(a^{p^k - 1} \equiv 1 \pmod{p^k}\), and two of them that agree modulo \(p\) agree modulo \(p^k\).

theorem card_nonwitnesses_le_quarter_of_prime_pow {p k : ℕ} (hp : p.Prime) (hk : 2 ≤ k)
    (hodd : p ^ k % 2 = 1) : (nonwitnesses (p ^ k)).card ≤ (p ^ k - 1) / 4
Uses 3 · Used by 1
Statement usesNon-witnesses of a number
Proof usesNon-witnesses pass Fermat's test and are units · Miller–Rabin witness test
Used byAt most a quarter of the bases are non-witnesses

TheoremAt most a quarter of the bases are non-witnesses#✓fully proved

Let \(n > 1\) be odd and not prime. Then at most \((n - 1)/4\) of the bases \(1, \dots, n - 1\) are non-witnesses for \(n\), so one uniformly random base fails to expose \(n\) as composite with probability at most \(1/4\).

theorem card_nonwitnesses_le_quarter {n : ℕ} (hn : 1 < n) (hodd : n % 2 = 1) (hcomp : ¬ n.Prime) :
    (nonwitnesses n).card ≤ (n - 1) / 4
Uses 4 · Used by 1
Statement usesNon-witnesses of a number
Proof usesAt most a quarter of the bases are non-witnesses for a Carmichael number · At most a quarter of the bases are non-witnesses when some unit fails Fermat's test and the modulus is not a prime power · At most a quarter of the bases are non-witnesses for an odd prime power
Used byQuarter error bound for Miller–Rabin with several bases

TheoremQuarter error bound for Miller–Rabin with several bases#✓fully proved

Let \(n > 1\) be odd and not prime, and let \(s\) be a natural number. Among the \((n - 1)^s\) lists \((b_1, \dots, b_s)\) of bases with \(0 < b_i < n\), at most \(\lfloor (n - 1)/4 \rfloor^s\) make the Miller–Rabin test of \(n\) with bases \(b_1, \dots, b_s\) answer prime.

With uniformly random bases the error probability is therefore at most \(4^{-s}\).

theorem card_millerRabin_errors_le_quarter {n : ℕ} (hn : 1 < n) (hodd : n % 2 = 1)
    (hcomp : ¬ n.Prime) (s : ℕ) :
    ((Fintype.piFinset fun _ : Fin s => Finset.Ioo 0 n).filter
        fun b => (millerRabin n (List.ofFn b)).ret = true).card ≤ ((n - 1) / 4) ^ s
Uses 5
Statement usesThe Miller–Rabin test
Proof usesAt most a quarter of the bases are non-witnesses · Miller–Rabin answers prime exactly when no base is a witness · Non-witnesses of a number · Miller–Rabin witness test
27 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.