PrimeComputability.lean

1 import RealizationBoundaries.PairedPrimes
2 import Mathlib.Computability.RE
3 
4 /-!
5 # Native computability of the actual prime enumeration
6 
7 The production `primeAt` uses Mathlib's mathematical nth-prime function. The
8 proof below derives a primitive recursive prime test and prime-counting
9 function, then identifies terminating unbounded search with that exact nth
10 function. No arbitrary function is declared computable merely because it is a
11 Lean definition.
12 -/
13 set_option autoImplicit false
14 noncomputable section
15 namespace RealizationBoundaries
16 
17 /-- Trial division is a primitive recursive relation. -/
18 theorem primrec_nat_dvd : PrimrecRel ((· ∣ ·) : ℕ → ℕ → Prop) := by
19   exact (Primrec.eq.comp (Primrec.nat_mod.comp Primrec.snd Primrec.fst)
20     (Primrec.const 0)).of_eq fun p => Nat.dvd_iff_mod_eq_zero.symm
21 
22 /-- Primality is decided by the bounded divisor test from `Nat.prime_def_lt`. -/
23 theorem primrec_prime_predicate : PrimrecPred Nat.Prime := by
24   have hdiv : PrimrecRel (fun m n : ℕ => m ∣ n → m = 1) :=
25     (primrec_nat_dvd.not.or (Primrec.eq.comp Primrec.fst (Primrec.const 1))).of_eq
26       (fun _ => by simp only [or_iff_not_imp_left, not_not])
27   have hforall : PrimrecPred (fun n : ℕ => ∀ m < n, m ∣ n → m = 1) :=
28     hdiv.forall_lt.comp Primrec.id Primrec.id
29   exact ((Primrec.nat_le.comp (Primrec.const 2) Primrec.id).and hforall).of_eq
30     fun _ => Nat.prime_def_lt.symm
31 
32 /-- The Boolean prime test itself is primitive recursive. -/
33 theorem primrec_prime_decide : Primrec (fun n : ℕ => decide n.Prime) :=
34   primrec_prime_predicate.decide
35 
36 /-- Counting primes below a bound is primitive recursive, by filtering a finite
37 range with the proved primitive recursive primality test. -/
38 theorem primrec_prime_count : Primrec (Nat.count Nat.Prime) := by
39   refine (Primrec.list_length.comp
40     ((Primrec.listFilter primrec_prime_predicate).comp Primrec.list_range)).of_eq ?_
41   intro n
42   simp only [Nat.count, List.countP_eq_length_filter]
43 
44 /-- The search relation means exactly: prime `p` has zero-based prime index `n`. -/
45 def primeIndexRelation (n p : ℕ) : Prop := p.Prime ∧ Nat.count Nat.Prime p = n
46 
47 instance primeIndexRelation_decidable : DecidableRel primeIndexRelation := by
48   unfold primeIndexRelation
49   infer_instance
50 
51 theorem primeIndexRelation_primrec : PrimrecRel primeIndexRelation := by
52   exact ((primrec_prime_predicate.comp Primrec.snd).and
53     (Primrec.eq.comp (primrec_prime_count.comp Primrec.snd) Primrec.fst))
54 
55 theorem primeIndexRelation_total (n : ℕ) : ∃ p, primeIndexRelation n p :=
56   ⟨Nat.nth Nat.Prime n,
57     Nat.nth_mem_of_infinite Nat.infinite_setOfPred_prime n,
58     Nat.count_nth_of_infinite Nat.infinite_setOfPred_prime n⟩
59 
60 /-- The existing mathematical nth-prime enumeration is native computable. The
61 unbounded search terminates by infinitude of primes and is identified using
62 `Nat.nth_count`, so this applies to the actual production enumeration. -/
63 theorem computable_nth_prime : Computable (Nat.nth Nat.Prime) := by
64   refine (Computable.find primeIndexRelation_primrec.computablePred
65     primeIndexRelation_total).of_eq ?_
66   intro n
67   have ht := Nat.find_spec (primeIndexRelation_total n)
68   have he := Nat.nth_count ht.1
69   rw [ht.2] at he
70   exact he.symm
71 
72 /-- Native computability of the literal natural value of `primeAt`. -/
73 theorem computable_primeAt_value : Computable (fun n : ℕ => (primeAt n).val) :=
74   computable_nth_prime
75 
76 end RealizationBoundaries

Back to source controls