ComputablePresentations.lean

1 import RealizationBoundaries.SelectorClassification
2 import RealizationBoundaries.PrimeComputability
3 import RealizationBoundaries.SubgroupSpectrum
4 import Mathlib.Computability.TuringDegree
5 
6 /-!
7 # Genuine oracle computations and paired positive search
8 
9 Oracle computability below is Mathlib's closure of the partial recursive
10 functions under an actual oracle call, primitive recursion and minimization.
11 A classical definition is never accepted as a computation without a proof in
12 that inductive semantics.
13 -/
14 set_option autoImplicit false
15 set_option backward.isDefEq.respectTransparency false
16 noncomputable section
17 
18 namespace RealizationBoundaries
19 
20 /-- The total, zero/one membership oracle for a binary selector. -/
21 def selectorOracle (a : ℕ → Bool) : ℕ →. ℕ :=
22   fun n => Part.some (if a n then 1 else 0)
23 
24 /-- Relative total computability, using the native oracle-recursion semantics. -/
25 def OracleComputable (X : ℕ → Bool) (f : ℕ → ℕ) : Prop :=
26   Nat.RecursiveIn {selectorOracle X} (fun n => Part.some (f n))
27 
28 /-- Selector reducibility is the actual Mathlib Turing reducibility relation. -/
29 def SelectorReducible (a X : ℕ → Bool) : Prop :=
30   TuringReducible (selectorOracle a) (selectorOracle X)
31 
32 namespace OracleComputable
33 
34 variable {X : ℕ → Bool} {f g : ℕ → ℕ}
35 
36 theorem of_computable (hf : Computable f) : OracleComputable X f := by
37   exact RecursiveIn.iff_nat.mp hf.computableIn
38 
39 /-- Substitution of one genuine oracle reduction into another. -/
40 theorem change_oracle {a : ℕ → Bool} (hf : OracleComputable a f)
41     (ha : SelectorReducible a X) : OracleComputable X f := by
42   apply hf.subst
43   intro g hg
44   have he : g = selectorOracle a := Set.mem_singleton_iff.mp hg
45   rw [he]
46   exact RecursiveIn.iff_nat.mp ha
47 
48 theorem of_eq (hf : OracleComputable X f) (h : ∀ n, f n = g n) :
49     OracleComputable X g :=
50   Nat.RecursiveIn.of_eq hf (fun n => congrArg Part.some (h n))
51 
52 theorem comp (hf : OracleComputable X f) (hg : OracleComputable X g) :
53     OracleComputable X (fun n => f (g n)) := by
54   apply (Nat.RecursiveIn.comp hf hg).of_eq
55   intro n
56   simp
57 
58 theorem pair (hf : OracleComputable X f) (hg : OracleComputable X g) :
59     OracleComputable X (fun n => Nat.pair (f n) (g n)) := by
60   apply (Nat.RecursiveIn.pair hf hg).of_eq
61   intro n
62   apply Part.eq_some_iff.mpr
63   exact ⟨⟨trivial, trivial⟩, rfl⟩
64 
65 theorem id : OracleComputable X id := of_computable Computable.id
66 
67 theorem const (k : ℕ) : OracleComputable X (fun _ => k) :=
68   of_computable (Computable.const k)
69 
70 theorem oracle : OracleComputable X (fun n => if X n then 1 else 0) :=
71   Nat.RecursiveIn.oracle (selectorOracle X) (by simp)
72 
73 /-- Total primitive recursion with a coded parameter. -/
74 theorem prec {initial : ℕ → ℕ} {step : ℕ → ℕ → ℕ → ℕ}
75     (hf : OracleComputable X initial)
76     (hg : OracleComputable X
77       (fun k => step k.unpair.1 k.unpair.2.unpair.1 k.unpair.2.unpair.2)) :
78     OracleComputable X (fun k =>
79       Nat.rec (initial k.unpair.1) (fun n r => step k.unpair.1 n r) k.unpair.2) := by
80   apply (Nat.RecursiveIn.prec hf hg).of_eq
81   intro k
82   dsimp
83   induction k.unpair.2 with
84   | zero => rfl
85   | succ n ih =>
86     simp only [Nat.unpair_pair] at ih ⊢
87     rw [ih]
88     simp
89 
90 /-- Total minimization is justified by an explicit termination witness at every input. -/
91 theorem find (hf : OracleComputable X f)
92     (h : ∀ n, ∃ t, f (Nat.pair n t) = 0) :
93     OracleComputable X (fun n => Nat.find (h n)) := by
94   apply (Nat.RecursiveIn.rfind hf).of_eq_tot
95   intro n
96   apply Nat.mem_rfind.mpr
97   constructor
98   · simp [Nat.find_spec (h n)]
99   · intro m hm
100     have hn : f (Nat.pair n m) ≠ 0 := Nat.find_min (h n) hm
101     simp [hn]
102 
103 /-- Finite searches can recover a total output only after a witness is found.
104 Both the stopping test and output reader must themselves be oracle computable. -/
105 theorem search_output (hf : OracleComputable X f) (hg : OracleComputable X g)
106     (h : ∀ n, ∃ t, f (Nat.pair n t) = 0) :
107     OracleComputable X (fun n => g (Nat.pair n (Nat.find (h n)))) :=
108   hg.comp (id.pair (find hf h))
109 
110 theorem left : OracleComputable X (fun n => n.unpair.1) :=
111   Nat.Primrec.left.recursiveIn
112 
113 theorem right : OracleComputable X (fun n => n.unpair.2) :=
114   Nat.Primrec.right.recursiveIn
115 
116 theorem mul (hf : OracleComputable X f) (hg : OracleComputable X g) :
117     OracleComputable X (fun n => f n * g n) :=
118   (Nat.Primrec.mul.recursiveIn : OracleComputable X (Nat.unpaired (· * ·))).comp
119     (hf.pair hg) |>.of_eq (fun n => by simp [Nat.unpaired])
120 
121 theorem isZero (hf : OracleComputable X f) :
122     OracleComputable X (fun n => if f n = 0 then 1 else 0) := by
123   have hz : OracleComputable X (fun n : ℕ => if n = 0 then 1 else 0) :=
124     (Nat.Primrec.casesOn1 1 Nat.Primrec.zero).recursiveIn |>.of_eq
125       (fun n => by cases n <;> simp)
126   exact hz.comp hf
127 
128 /-- Relative selection uses a primitive recursive comparison of the original input. -/
129 theorem ite_lt (N : ℕ) (hf : OracleComputable X f) (hg : OracleComputable X g) :
130     OracleComputable X (fun n => if n < N then f n else g n) := by
131   have hl : Primrec (fun k : ℕ => k.unpair.1) := Primrec.fst.comp Primrec.unpair
132   have hr : Primrec (fun k : ℕ => k.unpair.2) := Primrec.snd.comp Primrec.unpair
133   have hp : Computable (fun k : ℕ =>
134       if k.unpair.1 < N then k.unpair.2.unpair.1 else k.unpair.2.unpair.2) :=
135     (Primrec.ite (Primrec.nat_lt.comp hl (Primrec.const N))
136       (hl.comp hr) (hr.comp hr)).to_comp
137   exact (of_computable hp).comp (id.pair (hf.pair hg)) |>.of_eq
138     (fun n => by simp)
139 
140 end OracleComputable
141 
142 /-- A finite table is ordinary computable even when its fixed entries were
143 selected nonuniformly from a noncomputable set. -/
144 def finiteSelectorTable (a : ℕ → Bool) (N n : ℕ) : ℕ :=
145   if a (n % (N+1)) then 1 else 0
146 
147 theorem computable_finiteSelectorTable (a : ℕ → Bool) (N : ℕ) :
148     Computable (finiteSelectorTable a N) := by
149   let z : ℕ → Fin (N+1) := fun n => ⟨n % (N+1), Nat.mod_lt _ (Nat.succ_pos _)⟩
150   have hz : Primrec z := Primrec.fin_val_iff.mp
151     (Primrec.nat_mod.comp Primrec.id (Primrec.const (N+1)))
152   exact ((Primrec.dom_finite (fun i : Fin (N+1) => if a i.val then 1 else 0)).comp hz).to_comp
153 
154 /-- Hard-coding a finite prefix is a proved Turing reduction, not a uniform
155 procedure for discovering the prefix or its cutoff. -/
156 theorem selector_reduces_of_tail (a X : ℕ → Bool) (N : ℕ)
157     (h : SelectorReducible (fun n => a (n+N)) X) : SelectorReducible a X := by
158   have hb : OracleComputable X (fun n => if a (n+N) then 1 else 0) :=
159     RecursiveIn.iff_nat.mp h
160   have ht := hb.comp (OracleComputable.of_computable
161     (Primrec.nat_sub.comp Primrec.id (Primrec.const N)).to_comp)
162   have hp := OracleComputable.of_computable (X := X) (computable_finiteSelectorTable a N)
163   apply RecursiveIn.iff_nat.mpr
164   apply (hp.ite_lt N ht).of_eq
165   intro n
166   by_cases hn : n < N
167   · simp [hn, finiteSelectorTable, Nat.mod_eq_of_lt (lt_trans hn (Nat.lt_succ_self N))]
168   · simp [hn, Nat.sub_add_cancel (le_of_not_gt hn)]
169 
170 /-- A pair of complementary positive searches. The test is zero at a successful
171 stage and `answer` then gives the selector bit. This interface records an
172 actual recursive procedure and an explicit proof that it terminates. -/
173 structure ComplementarySearch (a X : ℕ → Bool) where
174   test : ℕ → ℕ
175   answer : ℕ → ℕ
176   test_computable : OracleComputable X test
177   answer_computable : OracleComputable X answer
178   terminates : ∀ n, ∃ t, test (Nat.pair n t) = 0
179   correct : ∀ n t, test (Nat.pair n t) = 0 →
180     answer (Nat.pair n t) = if a n then 1 else 0
181 
182 /-- Two complementary positive searches give a genuine Turing reduction. -/
183 theorem complementarySearch_reduces (a X : ℕ → Bool)
184     (s : ComplementarySearch a X) : SelectorReducible a X := by
185   apply RecursiveIn.iff_nat.mpr
186   have h := OracleComputable.search_output s.test_computable s.answer_computable s.terminates
187   exact h.of_eq (fun n => s.correct n _ (Nat.find_spec (s.terminates n)))
188 
189 /-- An oracle-computable group copy on the coded domain ℕ. Addition and equality
190 are computational; the isomorphism names the mathematical structure and is not
191 required to be computable. -/
192 structure OracleGroupCopy (X : ℕ → Bool) (H : Type*) [AddGroup H] where
193   names : ℕ ≃ H
194   zero : ℕ
195   add : ℕ → ℕ → ℕ
196   zero_spec : names zero = 0
197   add_spec : ∀ i j, names (add i j) = names i + names j
198   add_computable : OracleComputable X (fun k => add k.unpair.1 k.unpair.2)
199 
200 /-- Repeated addition on the actual coded domain. -/
201 def OracleGroupCopy.multiple {X : ℕ → Bool} {H : Type*} [AddGroup H]
202     (c : OracleGroupCopy X H) (m y : ℕ) : ℕ :=
203   Nat.rec c.zero (fun _ z => c.add y z) m
204 
205 @[simp] theorem OracleGroupCopy.multiple_spec {X : ℕ → Bool} {H : Type*} [AddGroup H]
206     (c : OracleGroupCopy X H) (m y : ℕ) : c.names (c.multiple m y) = m • c.names y := by
207   induction m with
208   | zero => simpa [OracleGroupCopy.multiple] using c.zero_spec
209   | succ m ih =>
210     change c.names (c.add y (c.multiple m y)) = (m+1) • c.names y
211     rw [c.add_spec, ih, succ_nsmul']
212 
213 /-- Multiplication by an arbitrary coded natural is obtained by native primitive
214 recursion from the copy's addition algorithm. -/
215 theorem OracleGroupCopy.multiple_computable {X : ℕ → Bool} {H : Type*} [AddGroup H]
216     (c : OracleGroupCopy X H) :
217     OracleComputable X (fun k => c.multiple k.unpair.2 k.unpair.1) := by
218   have step : OracleComputable X
219       (fun k => c.add k.unpair.1 k.unpair.2.unpair.2) := by
220     exact c.add_computable.comp (OracleComputable.left.pair
221       (OracleComputable.right.comp OracleComputable.right)) |>.of_eq
222         (fun n => by simp)
223   apply (Nat.RecursiveIn.prec (OracleComputable.const c.zero) step).of_eq
224   intro n
225   dsimp
226   induction n.unpair.2 with
227   | zero => rfl
228   | succ m ih =>
229     simp only [Nat.unpair_pair] at ih ⊢
230     rw [ih]
231     simp [OracleGroupCopy.multiple]
232 
233 /-- A decidable test for each candidate of each prime-root search in a coded copy.
234 The supplied bijection names every actual group element. Only finite candidate
235 tests are assumed computable; root existence is not assumed decidable. -/
236 structure RootSearchPresentation (X : ℕ → Bool) (H : Type*) [AddGroup H] where
237   names : ℕ ≃ H
238   target : H
239   offset : ℕ
240   test : ℕ → ℕ
241   test_computable : OracleComputable X test
242   test_correct : ∀ n side t, test (Nat.pair n (Nat.pair side t)) = 0 ↔
243     (primeAt (2*(n+offset)+side)).val • names t = target
244 
245 /-- The actual prime index used by a coded pair-search input. -/
246 def pairedSearchIndex (offset k : ℕ) : ℕ :=
247   2*(k.unpair.1+offset)+k.unpair.2.unpair.1
248 
249 theorem computable_pairedSearchIndex (offset : ℕ) : Computable (pairedSearchIndex offset) := by
250   have hl : Primrec (fun k : ℕ => k.unpair.1) := Primrec.fst.comp Primrec.unpair
251   have hr : Primrec (fun k : ℕ => k.unpair.2) := Primrec.snd.comp Primrec.unpair
252   exact (Primrec.nat_add.comp
253     (Primrec.nat_mul.comp (Primrec.const 2) (Primrec.nat_add.comp hl (Primrec.const offset)))
254     (hl.comp hr)).to_comp
255 
256 /-- Actual oracle-computable addition yields each decidable candidate root test.
257 The prime computation is the proved computation of the production `primeAt`,
258 not an extra oracle. -/
259 def OracleGroupCopy.rootSearch {X : ℕ → Bool} {H : Type*} [AddGroup H]
260     (c : OracleGroupCopy X H) (h offset : ℕ) : RootSearchPresentation X H where
261   names := c.names
262   target := c.names h
263   offset := offset
264   test := fun k => if c.multiple (primeAt (pairedSearchIndex offset k)).val
265       k.unpair.2.unpair.2 = h then 0 else 1
266   test_computable := by
267     have hm : OracleComputable X (fun k =>
268         c.multiple (primeAt (pairedSearchIndex offset k)).val k.unpair.2.unpair.2) := by
269       exact c.multiple_computable.comp
270         ((OracleComputable.right.comp OracleComputable.right).pair
271           (OracleComputable.of_computable
272             (computable_primeAt_value.comp (computable_pairedSearchIndex offset)))) |>.of_eq
273               (fun k => by simp)
274     have ht : Computable (fun m : ℕ => if m = h then 0 else 1) :=
275       (Primrec.ite (Primrec.eq.comp Primrec.id (Primrec.const h))
276         (Primrec.const 0) (Primrec.const 1)).to_comp
277     exact (OracleComputable.of_computable ht).comp hm
278   test_correct := by
279     intro n side t
280     simp only [pairedSearchIndex, Nat.unpair_pair]
281     rw [ite_eq_left_iff]
282     constructor
283     · intro hc
284       have he : c.multiple (primeAt (2*(n+offset)+side)).val t = h := by
285         by_contra hn
286         exact Nat.one_ne_zero (hc hn)
287       simpa only [← c.multiple_spec] using congrArg c.names he
288     · intro he
289       have hc := c.names.injective ((c.multiple_spec _ _).trans he)
290       simp [hc]
291 
292 /-- Candidate zero for the first prime of a pair. -/
293 def RootSearchPresentation.evenTest {X : ℕ → Bool} {H : Type*} [AddGroup H]
294     (c : RootSearchPresentation X H) (k : ℕ) : ℕ :=
295   c.test (Nat.pair k.unpair.1 (Nat.pair 0 k.unpair.2))
296 
297 /-- Candidate zero for the second prime of a pair. -/
298 def RootSearchPresentation.oddTest {X : ℕ → Bool} {H : Type*} [AddGroup H]
299     (c : RootSearchPresentation X H) (k : ℕ) : ℕ :=
300   c.test (Nat.pair k.unpair.1 (Nat.pair 1 k.unpair.2))
301 
302 theorem RootSearchPresentation.evenTest_computable {X : ℕ → Bool} {H : Type*} [AddGroup H]
303     (c : RootSearchPresentation X H) : OracleComputable X c.evenTest :=
304   c.test_computable.comp (OracleComputable.left.pair
305     ((OracleComputable.const 0).pair OracleComputable.right))
306 
307 theorem RootSearchPresentation.oddTest_computable {X : ℕ → Bool} {H : Type*} [AddGroup H]
308     (c : RootSearchPresentation X H) : OracleComputable X c.oddTest :=
309   c.test_computable.comp (OracleComputable.left.pair
310     ((OracleComputable.const 1).pair OracleComputable.right))
311 
312 /-- Dovetailing two positive root searches terminates when they carry complementary
313 bits. This produces native Turing reducibility from the actual root tests. -/
314 theorem paired_root_search_reduces (a X : ℕ → Bool) {H : Type*} [AddGroup H]
315     (c : RootSearchPresentation X H)
316     (he : ∀ n, (HasPrimeRoot c.target (primeAt (2*(n+c.offset))) ↔ a n = true))
317     (ho : ∀ n, (HasPrimeRoot c.target (primeAt (2*(n+c.offset)+1)) ↔ a n = false)) :
318     SelectorReducible a X := by
319   apply complementarySearch_reduces a X
320   refine {
321     test := fun k => c.evenTest k * c.oddTest k
322     answer := fun k => if c.evenTest k = 0 then 1 else 0
323     test_computable := c.evenTest_computable.mul c.oddTest_computable
324     answer_computable := c.evenTest_computable.isZero
325     terminates := ?_
326     correct := ?_ }
327   · intro n
328     cases ha : a n
329     · obtain ⟨y, hy⟩ := (ho n).mpr ha
330       refine ⟨c.names.symm y, ?_⟩
331       have ht := (c.test_correct n 1 (c.names.symm y)).mpr (by simpa using hy)
332       simp [RootSearchPresentation.oddTest, ht]
333     · obtain ⟨y, hy⟩ := (he n).mpr ha
334       refine ⟨c.names.symm y, ?_⟩
335       have ht := (c.test_correct n 0 (c.names.symm y)).mpr (by simpa using hy)
336       simp [RootSearchPresentation.evenTest, ht]
337   · intro n t ht
338     have hleft : c.evenTest (Nat.pair n t) = 0 ↔ a n = true := by
339       constructor
340       · intro h
341         exact (he n).mp ⟨c.names t, (c.test_correct n 0 t).mp
342           (by simpa [RootSearchPresentation.evenTest] using h)⟩
343       · intro ha
344         by_contra hn
345         have hr : c.oddTest (Nat.pair n t) = 0 := (mul_eq_zero.mp ht).resolve_left hn
346         have hab := (ho n).mp ⟨c.names t, (c.test_correct n 1 t).mp
347           (by simpa [RootSearchPresentation.oddTest] using hr)⟩
348         simp [ha] at hab
349     cases ha : a n <;> simp_all
350 
351 theorem marked_even_root_iff (a : ℕ → Bool) (n : ℕ) :
352     @HasPrimeRoot (pairedGroup a) _ (markedElement (pairedSelector a))
353       (primeAt (2*n)) ↔ a n = true := by
354   cases ha : a n
355   · simp only [Bool.false_eq_true, iff_false]
356     change ¬ ∃ y : pairedGroup a, (primeAt (2*n)).val • y = markedElement (pairedSelector a)
357     have h := chosen_prime_obstructs a n
358     simpa only [chosenIndex, ha, Bool.false_eq_true, ↓reduceIte, add_zero] using h
359   · simp only [iff_true]
360     change ∃ y : pairedGroup a, (primeAt (2*n)).val • y = markedElement (pairedSelector a)
361     have h := omitted_prime_has_root a n
362     simpa only [omittedIndex, ha, ↓reduceIte, add_zero] using h
363 
364 theorem marked_odd_root_iff (a : ℕ → Bool) (n : ℕ) :
365     @HasPrimeRoot (pairedGroup a) _ (markedElement (pairedSelector a))
366       (primeAt (2*n+1)) ↔ a n = false := by
367   cases ha : a n
368   · simp only [iff_true]
369     change ∃ y : pairedGroup a, (primeAt (2*n+1)).val • y = markedElement (pairedSelector a)
370     have h := omitted_prime_has_root a n
371     simpa only [omittedIndex, ha, Bool.false_eq_true, ↓reduceIte] using h
372   · simp only [Bool.true_eq_false, iff_false]
373     change ¬ ∃ y : pairedGroup a, (primeAt (2*n+1)).val • y = markedElement (pairedSelector a)
374     have h := chosen_prime_obstructs a n
375     simpa only [chosenIndex, ha, ↓reduceIte] using h
376 
377 /-- The named element needs no negative existential test: two positive searches
378 suffice and their native oracle program is proved to terminate. -/
379 theorem marked_root_presentation_reduces (a X : ℕ → Bool) {H : Type*} [AddGroup H]
380     (c : RootSearchPresentation X H) (e : H ≃+ pairedGroup a)
381     (hmark : e c.target = markedElement (pairedSelector a)) (hoffset : c.offset = 0) :
382     SelectorReducible a X := by
383   apply paired_root_search_reduces a X c
384   · intro n
385     rw [← hasPrimeRoot_equiv e c.target, hmark]
386     simpa [hoffset] using marked_even_root_iff a n
387   · intro n
388     rw [← hasPrimeRoot_equiv e c.target, hmark]
389     simpa [hoffset] using marked_odd_root_iff a n
390 
391 /-- Uniform marked decoding from the actual addition algorithm and a supplied
392 natural name for the distinguished element (Monograph 8.2). -/
393 theorem oracle_marked_copy_reduces (a X : ℕ → Bool)
394     (c : OracleGroupCopy X (pairedGroup a)) (h : ℕ)
395     (hmark : c.names h = markedElement (pairedSelector a)) : SelectorReducible a X := by
396   apply marked_root_presentation_reduces a X (c.rootSearch h 0) (AddEquiv.refl _)
397   · exact hmark
398   · rfl
399 
400 /-- The unmarked converse of the exact oracle criterion. The abstract naming
401 isomorphism supplies a finite natural constant naming the marker. This theorem
402 does not compute that constant uniformly from an unmarked atomic diagram. -/
403 theorem oracle_unmarked_copy_reduces (a X : ℕ → Bool)
404     (c : OracleGroupCopy X (pairedGroup a)) : SelectorReducible a X := by
405   apply oracle_marked_copy_reduces a X c (c.names.symm (markedElement (pairedSelector a)))
406   exact c.names.apply_symm_apply _
407 
408 /-- The forward half of Monograph 8.3 with a genuine coded-presentation contract. -/
409 theorem oracle_copy_exists_implies_selector_reducible (a X : ℕ → Bool) :
410     Nonempty (OracleGroupCopy X (pairedGroup a)) → SelectorReducible a X := by
411   rintro ⟨c⟩
412   exact oracle_unmarked_copy_reduces a X c
413 
414 /-- Relative computable enumerability is the domain of a partial function in
415 Mathlib's native oracle-recursion semantics. -/
416 def OracleEnumerable (X : ℕ → Bool) (A : Set ℕ) : Prop :=
417   ∃ f : ℕ →. ℕ, Nat.RecursiveIn {selectorOracle X} f ∧
418     ∀ n, (f n).Dom ↔ n ∈ A
419 
420 /-- A dovetailed positive-witness search semidecides its existential predicate. -/
421 theorem oracleEnumerable_of_test (X : ℕ → Bool) (test : ℕ → ℕ)
422     (ht : OracleComputable X test) :
423     OracleEnumerable X {n | ∃ t, test (Nat.pair n t) = 0} := by
424   refine ⟨_, Nat.RecursiveIn.rfind ht, ?_⟩
425   intro n
426   simp [Nat.rfind_dom]
427 
428 /-- Deciding whether a coded candidate is nonzero prime torsion only uses finite
429 addition and equality tests. -/
430 def OracleGroupCopy.torsionTest {X : ℕ → Bool} {H : Type*} [AddGroup H]
431     (c : OracleGroupCopy X H) (k : ℕ) : ℕ :=
432   if c.multiple (primeAt k.unpair.1).val k.unpair.2 = c.zero ∧
433       k.unpair.2 ≠ c.zero then 0 else 1
434 
435 theorem OracleGroupCopy.torsionTest_computable {X : ℕ → Bool} {H : Type*} [AddGroup H]
436     (c : OracleGroupCopy X H) : OracleComputable X c.torsionTest := by
437   have hm : OracleComputable X (fun k => c.multiple (primeAt k.unpair.1).val k.unpair.2) :=
438     c.multiple_computable.comp (OracleComputable.right.pair
439       ((OracleComputable.of_computable computable_primeAt_value).comp OracleComputable.left))
440       |>.of_eq (fun k => by simp)
441   have hl : Primrec (fun k : ℕ => k.unpair.1) := Primrec.fst.comp Primrec.unpair
442   have hr : Primrec (fun k : ℕ => k.unpair.2) := Primrec.snd.comp Primrec.unpair
443   have hp : Computable (fun k : ℕ =>
444       if k.unpair.1 = c.zero ∧ k.unpair.2 ≠ c.zero then 0 else 1) :=
445     (Primrec.ite ((Primrec.eq.comp hl (Primrec.const c.zero)).and
446       (Primrec.eq.comp hr (Primrec.const c.zero)).not)
447         (Primrec.const 0) (Primrec.const 1)).to_comp
448   exact (OracleComputable.of_computable hp).comp (hm.pair OracleComputable.right)
449     |>.of_eq (fun k => by simp [OracleGroupCopy.torsionTest])
450 
451 theorem OracleGroupCopy.torsionTest_correct {X : ℕ → Bool} {H : Type*} [AddGroup H]
452     (c : OracleGroupCopy X H) (n t : ℕ) : c.torsionTest (Nat.pair n t) = 0 ↔
453     c.names t ≠ 0 ∧ (primeAt n).val • c.names t = 0 := by
454   have hzero : c.names t = 0 ↔ t = c.zero := by
455     rw [← c.zero_spec, c.names.injective.eq_iff]
456   have hmul : (primeAt n).val • c.names t = 0 ↔
457       c.multiple (primeAt n).val t = c.zero := by
458     rw [← c.multiple_spec, ← c.zero_spec, c.names.injective.eq_iff]
459   simp only [OracleGroupCopy.torsionTest, Nat.unpair_pair, ite_eq_left_iff,
460     one_ne_zero, imp_false, not_not]
461   constructor
462   · rintro ⟨hm, hn⟩
463     exact ⟨fun he => hn (hzero.mp he), hmul.mpr hm⟩
464   · rintro ⟨hn, hm⟩
465     exact ⟨hmul.mp hm, fun he => hn (hzero.mpr he)⟩
466 
467 /-- The prime spectrum of every genuinely oracle-computable coded copy is
468 computably enumerable relative to that oracle. -/
469 theorem oracle_copy_primeSpectrum_enumerable (X : ℕ → Bool) {H : Type*} [AddGroup H]
470     (c : OracleGroupCopy X H) :
471     OracleEnumerable X {n | HasPrimeTorsion H (primeAt n)} := by
472   obtain ⟨f, hf, hdom⟩ := oracleEnumerable_of_test X c.torsionTest c.torsionTest_computable
473   refine ⟨f, hf, ?_⟩
474   intro n
475   rw [hdom]
476   constructor
477   · rintro ⟨t, ht⟩
478     exact ⟨c.names t, (c.torsionTest_correct n t).mp ht⟩
479   · rintro ⟨y, hy⟩
480     refine ⟨c.names.symm y, (c.torsionTest_correct n _).mpr ?_⟩
481     simpa only [c.names.apply_symm_apply] using hy
482 
483 /-- The forward prime-spectrum implication (Monograph 3.3) on an infinite coded
484 copy. Finite selector groups need the separate finite-domain convention. -/
485 theorem oracle_spectrum_copy_implies_enumerable (X : ℕ → Bool) (B : Set Prime)
486     (c : OracleGroupCopy X (spectrumSubgroup B)) :
487     OracleEnumerable X {n | primeAt n ∈ B} := by
488   obtain ⟨f, hf, hdom⟩ := oracle_copy_primeSpectrum_enumerable X c
489   refine ⟨f, hf, ?_⟩
490   intro n
491   exact (hdom n).trans (spectrumSubgroup_hasPrimeTorsion_iff B (primeAt n))
492 
493 end RealizationBoundaries

Back to source controls