Theorem Details
-- Miller Rabin Fixed Repetition Correctness
import Mathlib
-- see https://manifold.markets/BoltonBailey/is-there-a-number-of-repetitions-fo
-- see https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Miller.E2.80.93Rabin.20Primality.20Test
-- def from https://reservoir.lean-lang.org/@hanwenzhu/primality-tests
def val₂ (n : ℕ) : ℕ :=
padicValNat 2 n
-- def from https://reservoir.lean-lang.org/@hanwenzhu/primality-tests
def oddPart (n : ℕ) : ℕ :=
n / 2 ^ val₂ n
-- def from https://reservoir.lean-lang.org/@hanwenzhu/primality-tests
def SPP (n : ℕ) (a : ZMod n) : Prop :=
a ^ oddPart (n - 1) = 1 ∨
∃ s : ℕ, s < val₂ (n - 1) ∧ a ^ (2 ^ s * oddPart (n - 1)) = -1
-- If n is a prime power, then the test will succeed,
-- since either n is a prime and will be found to be so
-- or n is a composite power of a prime,
-- in which case the test will determine that n is a nontrivial power of another number and therefore is composite.
-- if n has distinct prime factors, the error propability is the fraction of bases to which n is a strong probable prime.
noncomputable def miller_rabin_single_repetition_error_probability (n : Nat) : ℚ :=
if (n ≤ 4 ∨ IsPrimePow n) then (0 : ℚ) else (Nat.card {(a : ZMod (n : Nat)) | SPP n a}) / (n : ℚ)
theorem miller_rabin_not_correct (repetitions : Nat) :
∑' (n : ℕ),
(miller_rabin_single_repetition_error_probability n) ^ (repetitions + 1)
= 0 := sorry
Bounty: 0.0017 ETH
Status: Open