Primality of unary naturals by trial division

A natural p is prime exactly when 2 ≤ p and no m with 2 ≤ m < p divides it (Turing.MultiTapeTM.ComputableInPolyTime.decide_prime_eq). Testing every candidate below p takes time polynomial in p, hence in the length of its unary encoding (Turing.MultiTapeTM.ComputableInPolyTime.unary_decide_prime).

Main results

• Turing.MultiTapeTM.ComputableInPolyTime.decide_prime_eq: primality by trial division.
• Turing.MultiTapeTM.ComputableInPolyTime.unary_decide_prime: in polynomial time.

theorem Turing.MultiTapeTM.ComputableInPolyTime.decide_prime_eq (p : ℕ) : decide (Nat.Prime p) = (decide (2 ≤ p) && (List.range p).all fun (m : ℕ) => decide (m < 2) || decide (p % m ≠ 0))

Primality by trial division.

theorem Turing.MultiTapeTM.ComputableInPolyTime.unary_decide_prime : ComputableInPolyTime (fun (p : ℕ) => decide (Nat.Prime p)) encUnary encBool

Primality of a unary natural, by trial division.