SearchEnumerableSpectrum.lean

1 import RealizationBoundaries.ComputableNormalCodes
2 import RealizationBoundaries.SpectrumComputability
3 
4 /-!
5 # Actual spectrum copies from positive enumerable witnesses
6 
7 The enumeration contract is a total oracle-computable candidate test with an
8 existential natural witness. It neither decides negative membership nor assumes
9 that a classical selector definition is computable.
10 -/
11 set_option autoImplicit false
12 set_option backward.isDefEq.respectTransparency false
13 set_option maxHeartbeats 1000000
14 noncomputable section
15 open scoped BigOperators
16 namespace RealizationBoundaries
17 attribute [local instance] Classical.propDecidable
18 
19 /-- Standard positive-search enumeration semantics. -/
20 structure OracleSearchEnumeration (X : ℕ → Bool) (A : Set ℕ) where
21   test : ℕ → ℕ
22   test_computable : OracleComputable X test
23   test_spec : ∀ n, n ∈ A ↔ ∃ t, test (Nat.pair n t) = 0
24 
25 /-- Product of the first `s` candidate-test results; zero means discovered. -/
26 def discoveryProduct (test : ℕ → ℕ) (n s : ℕ) : ℕ :=
27   Nat.rec 1 (fun t r => r * test (Nat.pair n t)) s
28 
29 theorem discoveryProduct_zero_iff (test : ℕ → ℕ) (n s : ℕ) :
30     discoveryProduct test n s = 0 ↔ ∃ t < s, test (Nat.pair n t) = 0 := by
31   induction s with
32   | zero => simp [discoveryProduct]
33   | succ s ih =>
34     change discoveryProduct test n s * test (Nat.pair n s) = 0 ↔ _
35     rw [mul_eq_zero, ih]
36     constructor
37     · rintro (⟨t, ht, he⟩ | he)
38       · exact ⟨t, Nat.lt_succ_of_lt ht, he⟩
39       · exact ⟨s, Nat.lt_succ_self s, he⟩
40     · rintro ⟨t, ht, he⟩
41       rcases Nat.lt_succ_iff_lt_or_eq.mp ht with ht | rfl
42       · exact Or.inl ⟨t, ht, he⟩
43       · exact Or.inr he
44 
45 theorem discoveryProduct_zero_mono (test : ℕ → ℕ) (n : ℕ) {s t : ℕ}
46     (hst : s ≤ t) (hs : discoveryProduct test n s = 0) :
47     discoveryProduct test n t = 0 := by
48   obtain ⟨k, hk, he⟩ := (discoveryProduct_zero_iff test n s).mp hs
49   exact (discoveryProduct_zero_iff test n t).mpr ⟨k, hk.trans_le hst, he⟩
50 
51 theorem discoveryProduct_computable {X : ℕ → Bool} {test : ℕ → ℕ}
52     (ht : OracleComputable X test) :
53     OracleComputable X (fun k => discoveryProduct test k.unpair.1 k.unpair.2) := by
54   have he := ht.comp (OracleComputable.left.pair
55     (OracleComputable.left.comp OracleComputable.right))
56   exact OracleComputable.prec (step := fun n t r => r * test (Nat.pair n t))
57     (OracleComputable.const 1) ((OracleComputable.right.comp OracleComputable.right).mul he)
58 
59 /-- Raw code is a stage together with a finite residue list. A cell is admitted
60 only after that prime's positive membership witness has actually appeared. -/
61 def spectrumDiscoveryCell (test : ℕ → ℕ) (k : ℕ) : ℕ :=
62   if discoveryProduct test (Nat.count Nat.Prime k.unpair.2) k.unpair.1.unpair.1 = 0
63   then (decodeResidues k.unpair.1.unpair.2).getD k.unpair.2 0 else 0
64 
65 def spectrumDiscoveryResidues (test : ℕ → ℕ) (c : ℕ) : List ℕ :=
66   residueLoop (spectrumDiscoveryCell test) c (decodeResidues c.unpair.2).length
67 
68 theorem spectrumDiscoveryResidues_formula (test : ℕ → ℕ) (c : ℕ) (p : Prime) :
69     finiteCodeValue (spectrumDiscoveryResidues test c) p =
70       if discoveryProduct test (Nat.count Nat.Prime p.val) c.unpair.1 = 0
71       then finiteCodeValue (decodeResidues c.unpair.2) p else 0 := by
72   by_cases hp : p.val < (decodeResidues c.unpair.2).length
73   · rw [spectrumDiscoveryResidues, residueLoop_eq_ofFn]
74     simp only [finiteCodeValue, List.getElem?_ofFn, hp, dite_true, Option.getD_some]
75     simp only [spectrumDiscoveryCell, Nat.unpair_pair]
76     split <;> simp [← List.getD_eq_getElem?_getD]
77   · have hl : (spectrumDiscoveryResidues test c).length = (decodeResidues c.unpair.2).length := by
78       rw [spectrumDiscoveryResidues, residueLoop_eq_ofFn, List.length_ofFn]
79     rw [finiteCodeValue_eq_zero _ p (hl.symm ▸ Nat.le_of_not_gt hp),
80       finiteCodeValue_eq_zero _ p (Nat.le_of_not_gt hp)]
81     split <;> rfl
82 
83 /-- Every raw name denotes an element of the actual selected subgroup. -/
84 def spectrumDiscoveryValue {X : ℕ → Bool} {B : Set Prime}
85     (E : OracleSearchEnumeration X {n | primeAt n ∈ B}) (c : ℕ) : spectrumSubgroup B := by
86   refine ⟨finiteResidues (spectrumDiscoveryResidues E.test c), ?_⟩
87   intro p hp
88   have hseen : discoveryProduct E.test (Nat.count Nat.Prime p.val) c.unpair.1 = 0 := by
89     by_contra hn
90     exact hp (by simp [finiteResidues, spectrumDiscoveryResidues_formula, hn])
91   obtain ⟨t, _, ht⟩ := (discoveryProduct_zero_iff _ _ _).mp hseen
92   have hb := (E.test_spec (Nat.count Nat.Prime p.val)).mpr ⟨t, ht⟩
93   have hindex : primeAt (Nat.count Nat.Prime p.val) = p := Subtype.ext (Nat.nth_count p.property)
94   simpa only [Set.mem_ofPred_eq, hindex] using hb
95 
96 theorem spectrumDiscoveryCell_computable {X : ℕ → Bool} {test : ℕ → ℕ}
97     (ht : OracleComputable X test) : OracleComputable X (spectrumDiscoveryCell test) := by
98   have hl : Primrec (fun k : ℕ => k.unpair.1) := Primrec.fst.comp Primrec.unpair
99   have hr : Primrec (fun k : ℕ => k.unpair.2) := Primrec.snd.comp Primrec.unpair
100   have hi := OracleComputable.of_computable (X := X)
101     (primrec_prime_count.comp hr).to_comp
102   have hs := OracleComputable.of_computable (X := X) (hl.comp hl).to_comp
103   have hz := ((discoveryProduct_computable ht).comp (hi.pair hs)).isZero
104   have hd : OracleComputable X (fun k : ℕ => (decodeResidues k.unpair.1.unpair.2).getD k.unpair.2 0) :=
105     OracleComputable.of_computable (((Primrec.list_getD 0).comp
106       (primrec_decodeResidues.comp (hr.comp hl)) hr).to_comp)
107   exact (hz.mul hd).of_eq (fun k => by
108     simp only [spectrumDiscoveryCell]
109     split <;> simp_all)
110 
111 theorem spectrumDiscoveryResidues_computable {X : ℕ → Bool} {test : ℕ → ℕ}
112     (ht : OracleComputable X test) :
113     OracleComputable X (fun c => Encodable.encode (spectrumDiscoveryResidues test c)) := by
114   have hlen : Computable (fun c : ℕ => (decodeResidues c.unpair.2).length) :=
115     (Primrec.list_length.comp (primrec_decodeResidues.comp (Primrec.snd.comp Primrec.unpair))).to_comp
116   exact (residueLoop_oracleComputable (spectrumDiscoveryCell_computable ht)).comp
117     (OracleComputable.id.pair (OracleComputable.of_computable hlen)) |>.of_eq
118       (fun c => by simp [spectrumDiscoveryResidues])
119 
120 /-- Positive enumeration witnesses eventually admit every finitely supported
121 selected vector. No membership decision for an undiscovered prime is needed. -/
122 theorem spectrumDiscoveryValue_surjective {X : ℕ → Bool} {B : Set Prime}
123     (E : OracleSearchEnumeration X {n | primeAt n ∈ B}) :
124     Function.Surjective (spectrumDiscoveryValue E) := by
125   classical
126   intro x
127   obtain ⟨d, hd⟩ := finiteCodeValue_represents x.val
128   let F := x.val.property.toFinset
129   have hw : ∀ p : {p : Prime // p ∈ F},
130       ∃ t, E.test (Nat.pair (Nat.count Nat.Prime p.val.val) t) = 0 := by
131     intro p
132     have hp : p.val ∈ support x.val.val := x.val.property.mem_toFinset.mp p.property
133     have hB : p.val ∈ B := x.property hp
134     apply (E.test_spec (Nat.count Nat.Prime p.val.val)).mp
135     have he : primeAt (Nat.count Nat.Prime p.val.val) = p.val :=
136       Subtype.ext (Nat.nth_count p.val.property)
137     change primeAt (Nat.count Nat.Prime p.val.val) ∈ B
138     rw [he]
139     exact hB
140   choose w hw using hw
141   let s := Finset.univ.sup (fun p : {p : Prime // p ∈ F} => w p + 1)
142   refine ⟨Nat.pair s (Encodable.encode d), ?_⟩
143   apply Subtype.ext
144   apply Subtype.ext
145   funext p
146   change finiteCodeValue (spectrumDiscoveryResidues E.test (Nat.pair s (Encodable.encode d))) p = x.val.val p
147   rw [spectrumDiscoveryResidues_formula]
148   simp only [Nat.unpair_pair, decodeResidues_encode]
149   by_cases hp : x.val.val p = 0
150   · rw [hd]
151     split <;> simp [hp]
152   · have hpF : p ∈ F := x.val.property.mem_toFinset.mpr hp
153     have hbound : w ⟨p, hpF⟩ < s := by
154       have hb : w ⟨p, hpF⟩ + 1 ≤ s := Finset.le_sup (f := fun q : {p : Prime // p ∈ F} => w q + 1)
155         (Finset.mem_univ (⟨p, hpF⟩ : {p : Prime // p ∈ F}))
156       omega
157     have hs : discoveryProduct E.test (Nat.count Nat.Prime p.val) s = 0 :=
158       (discoveryProduct_zero_iff _ _ _).mpr ⟨w ⟨p, hpF⟩, hbound, hw ⟨p, hpF⟩⟩
159     rw [ite_eq_left hs, hd]
160 
161 /-- One cell of addition uses only the two already discovered finite vectors. -/
162 def spectrumDiscoveryAddCell (test : ℕ → ℕ) (k : ℕ) : ℕ :=
163   spectrumDiscoveryCell test (Nat.pair k.unpair.1.unpair.1 k.unpair.2) +
164     spectrumDiscoveryCell test (Nat.pair k.unpair.1.unpair.2 k.unpair.2)
165 
166 def spectrumDiscoveryAddResidues (test : ℕ → ℕ) (c d : ℕ) : List ℕ :=
167   residueLoop (spectrumDiscoveryAddCell test) (Nat.pair c d)
168     (max (decodeResidues c.unpair.2).length (decodeResidues d.unpair.2).length)
169 
170 def spectrumDiscoveryAdd (test : ℕ → ℕ) (c d : ℕ) : ℕ :=
171   Nat.pair (max c.unpair.1 d.unpair.1)
172     (Encodable.encode (spectrumDiscoveryAddResidues test c d))
173 
174 theorem spectrumDiscoveryAddResidues_exact (test : ℕ → ℕ) (c d : ℕ) :
175     finiteCodeValue (spectrumDiscoveryAddResidues test c d) =
176       finiteCodeValue (spectrumDiscoveryResidues test c) +
177         finiteCodeValue (spectrumDiscoveryResidues test d) := by
178   funext p
179   by_cases hp : p.val < max (decodeResidues c.unpair.2).length (decodeResidues d.unpair.2).length
180   · rw [spectrumDiscoveryAddResidues, residueLoop_eq_ofFn]
181     simp only [finiteCodeValue, List.getElem?_ofFn, hp, dite_true, Option.getD_some]
182     simp only [spectrumDiscoveryAddCell, Nat.unpair_pair]
183     rw [Nat.cast_add]
184     change (spectrumDiscoveryCell test (Nat.pair c p.val) : Coordinate p) +
185       (spectrumDiscoveryCell test (Nat.pair d p.val) : Coordinate p) = _
186     rw [Pi.add_apply, spectrumDiscoveryResidues_formula, spectrumDiscoveryResidues_formula]
187     simp only [spectrumDiscoveryCell, Nat.unpair_pair]
188     split <;> split <;> simp [finiteCodeValue, ← List.getD_eq_getElem?_getD]
189   · have hc : (decodeResidues c.unpair.2).length ≤ p.val := (le_max_left _ _).trans (Nat.le_of_not_gt hp)
190     have hd : (decodeResidues d.unpair.2).length ≤ p.val := (le_max_right _ _).trans (Nat.le_of_not_gt hp)
191     have hlen : (spectrumDiscoveryAddResidues test c d).length =
192         max (decodeResidues c.unpair.2).length (decodeResidues d.unpair.2).length := by
193       rw [spectrumDiscoveryAddResidues, residueLoop_eq_ofFn, List.length_ofFn]
194     rw [finiteCodeValue_eq_zero _ p (hlen.symm ▸ Nat.le_of_not_gt hp)]
195     rw [Pi.add_apply, spectrumDiscoveryResidues_formula, spectrumDiscoveryResidues_formula,
196       finiteCodeValue_eq_zero _ p hc, finiteCodeValue_eq_zero _ p hd]
197     split <;> split <;> simp
198 
199 theorem spectrumDiscoveryValue_add {X : ℕ → Bool} {B : Set Prime}
200     (E : OracleSearchEnumeration X {n | primeAt n ∈ B}) (c d : ℕ) :
201     spectrumDiscoveryValue E (spectrumDiscoveryAdd E.test c d) =
202       spectrumDiscoveryValue E c + spectrumDiscoveryValue E d := by
203   apply Subtype.ext
204   apply Subtype.ext
205   funext p
206   change finiteCodeValue (spectrumDiscoveryResidues E.test (spectrumDiscoveryAdd E.test c d)) p = _
207   rw [spectrumDiscoveryResidues_formula]
208   simp only [spectrumDiscoveryAdd, Nat.unpair_pair, decodeResidues_encode]
209   rw [spectrumDiscoveryAddResidues_exact]
210   by_cases hs : discoveryProduct E.test (Nat.count Nat.Prime p.val) (max c.unpair.1 d.unpair.1) = 0
211   · rw [ite_eq_left hs]
212     rfl
213   · rw [ite_eq_right hs]
214     have hc : discoveryProduct E.test (Nat.count Nat.Prime p.val) c.unpair.1 ≠ 0 :=
215       fun h => hs (discoveryProduct_zero_mono _ _ (le_max_left _ _) h)
216     have hd : discoveryProduct E.test (Nat.count Nat.Prime p.val) d.unpair.1 ≠ 0 :=
217       fun h => hs (discoveryProduct_zero_mono _ _ (le_max_right _ _) h)
218     change 0 = finiteCodeValue (spectrumDiscoveryResidues E.test c) p +
219       finiteCodeValue (spectrumDiscoveryResidues E.test d) p
220     rw [spectrumDiscoveryResidues_formula, spectrumDiscoveryResidues_formula, ite_eq_right hc, ite_eq_right hd, add_zero]
221 
222 theorem spectrumDiscoveryAddCell_computable {X : ℕ → Bool} {test : ℕ → ℕ}
223     (ht : OracleComputable X test) : OracleComputable X (spectrumDiscoveryAddCell test) := by
224   have hcell := spectrumDiscoveryCell_computable ht
225   exact ((hcell.comp ((OracleComputable.left.comp OracleComputable.left).pair OracleComputable.right)).add
226     (hcell.comp ((OracleComputable.right.comp OracleComputable.left).pair OracleComputable.right)))
227 
228 theorem spectrumDiscoveryAdd_computable {X : ℕ → Bool} {test : ℕ → ℕ}
229     (ht : OracleComputable X test) :
230     OracleComputable X (fun k => spectrumDiscoveryAdd test k.unpair.1 k.unpair.2) := by
231   have hl : Primrec (fun k : ℕ => k.unpair.1) := Primrec.fst.comp Primrec.unpair
232   have hr : Primrec (fun k : ℕ => k.unpair.2) := Primrec.snd.comp Primrec.unpair
233   have hlen : Computable (fun k : ℕ =>
234       max (decodeResidues k.unpair.1.unpair.2).length (decodeResidues k.unpair.2.unpair.2).length) :=
235     (Primrec.nat_max.comp
236       (Primrec.list_length.comp (primrec_decodeResidues.comp (hr.comp hl)))
237       (Primrec.list_length.comp (primrec_decodeResidues.comp (hr.comp hr)))).to_comp
238   have hmax : Computable (fun k : ℕ => max k.unpair.1.unpair.1 k.unpair.2.unpair.1) :=
239     (Primrec.nat_max.comp (hl.comp hl) (hl.comp hr)).to_comp
240   have hloop := (residueLoop_oracleComputable (spectrumDiscoveryAddCell_computable ht)).comp
241     (OracleComputable.id.pair (OracleComputable.of_computable hlen))
242   exact ((OracleComputable.of_computable hmax).pair hloop).of_eq
243     (fun k => by simp [spectrumDiscoveryAdd, spectrumDiscoveryAddResidues])
244 
245 def spectrumDiscoveryEqual (test : ℕ → ℕ) (c d : ℕ) : ℕ :=
246   if ResiduesEqual (spectrumDiscoveryResidues test c) (spectrumDiscoveryResidues test d) then 0 else 1
247 
248 theorem spectrumDiscoveryEqual_exact {X : ℕ → Bool} {B : Set Prime}
249     (E : OracleSearchEnumeration X {n | primeAt n ∈ B}) (c d : ℕ) :
250     spectrumDiscoveryEqual E.test c d = 0 ↔ spectrumDiscoveryValue E c = spectrumDiscoveryValue E d := by
251   simp only [spectrumDiscoveryEqual, ite_eq_left_iff, one_ne_zero, imp_false, not_not,
252     residuesEqual_iff, Subtype.ext_iff]
253   rfl
254 
255 theorem spectrumDiscoveryEqual_computable {X : ℕ → Bool} {test : ℕ → ℕ}
256     (ht : OracleComputable X test) :
257     OracleComputable X (fun k => spectrumDiscoveryEqual test k.unpair.1 k.unpair.2) := by
258   have hl : Primrec (fun k : ℕ => k.unpair.1) := Primrec.fst.comp Primrec.unpair
259   have hr : Primrec (fun k : ℕ => k.unpair.2) := Primrec.snd.comp Primrec.unpair
260   have he : Computable (fun k : ℕ =>
261       if ResiduesEqual (decodeResidues k.unpair.1) (decodeResidues k.unpair.2) then 0 else 1) :=
262     (Primrec.ite (primrec_residuesEqual.comp (primrec_decodeResidues.comp hl)
263       (primrec_decodeResidues.comp hr)) (Primrec.const 0) (Primrec.const 1)).to_comp
264   have hm := spectrumDiscoveryResidues_computable ht
265   exact (OracleComputable.of_computable he).comp
266     ((hm.comp OracleComputable.left).pair (hm.comp OracleComputable.right)) |>.of_eq
267       (fun k => by simp [spectrumDiscoveryEqual])
268 
269 /-- The complete raw-code presentation has proved surjectivity, exact equality,
270 and native oracle algorithms for both equality and addition. -/
271 def spectrumDiscoveryRawCodes {X : ℕ → Bool} {B : Set Prime}
272     (E : OracleSearchEnumeration X {n | primeAt n ∈ B}) : OracleRawGroupCodes X (spectrumSubgroup B) where
273   names := spectrumDiscoveryValue E
274   names_surjective := spectrumDiscoveryValue_surjective E
275   zero := Nat.pair 0 (Encodable.encode ([] : List ℕ))
276   add := spectrumDiscoveryAdd E.test
277   equal := spectrumDiscoveryEqual E.test
278   zero_spec := by
279     apply Subtype.ext
280     apply Subtype.ext
281     funext p
282     change finiteCodeValue (spectrumDiscoveryResidues E.test (Nat.pair 0 (Encodable.encode ([] : List ℕ)))) p = 0
283     rw [spectrumDiscoveryResidues_formula]
284     simp [discoveryProduct]
285   add_spec := spectrumDiscoveryValue_add E
286   equal_spec := spectrumDiscoveryEqual_exact E
287   add_computable := spectrumDiscoveryAdd_computable E.test_computable
288   equal_computable := spectrumDiscoveryEqual_computable E.test_computable
289 
290 /-- An infinite selected direct sum obtains an actual bijective Nat-domain copy
291 from positive enumeration witnesses, with no membership oracle for the selector. -/
292 theorem oracle_spectrum_copy_of_searchEnumeration {X : ℕ → Bool} {B : Set Prime}
293     [Infinite (spectrumSubgroup B)]
294     (E : OracleSearchEnumeration X {n | primeAt n ∈ B}) :
295     Nonempty (OracleGroupCopy X (spectrumSubgroup B)) :=
296   (spectrumDiscoveryRawCodes E).oracleGroupCopy_of_rawCodes
297 
298 /-- The explicit witness-test semantics implies the native partial-domain
299 semantics by actual oracle minimization. No converse normal form is assumed. -/
300 theorem OracleSearchEnumeration.toOracleEnumerable {X : ℕ → Bool} {A : Set ℕ}
301     (E : OracleSearchEnumeration X A) : OracleEnumerable X A := by
302   obtain ⟨f, hf, hdom⟩ := oracleEnumerable_of_test X E.test E.test_computable
303   exact ⟨f, hf, fun n => (hdom n).trans (E.test_spec n).symm⟩
304 
305 /-- A fixed finite set has a total ordinary candidate test. This does not infer
306 when a finite enumeration has stopped. -/
307 def finiteSearchEnumeration (X : ℕ → Bool) (A : Set ℕ) (hA : A.Finite) :
308     OracleSearchEnumeration X A where
309   test := fun k => if k.unpair.1 ∈ A then 0 else 1
310   test_computable := OracleComputable.of_computable
311     ((Primrec.ite ((finite_set_primrec_membership A hA).comp
312       (Primrec.fst.comp Primrec.unpair)) (Primrec.const 0) (Primrec.const 1)).to_comp)
313   test_spec := by
314     intro n
315     simp
316 
317 /-- Candidate positive torsion tests give the witness-test enumeration semantics
318 from an actual infinite copy, rather than only an abstract partial domain. -/
319 def spectrumSearchEnumeration_of_copy (X : ℕ → Bool) (B : Set Prime)
320     (c : OracleGroupCopy X (spectrumSubgroup B)) :
321     OracleSearchEnumeration X {n | primeAt n ∈ B} where
322   test := c.torsionTest
323   test_computable := c.torsionTest_computable
324   test_spec := by
325     intro n
326     constructor
327     · intro hn
328       obtain ⟨x, hx⟩ := (spectrumSubgroup_hasPrimeTorsion_iff B (primeAt n)).mpr hn
329       refine ⟨c.names.symm x, (c.torsionTest_correct n _).mpr ?_⟩
330       simpa only [c.names.apply_symm_apply] using hx
331     · rintro ⟨t, ht⟩
332       exact (spectrumSubgroup_hasPrimeTorsion_iff B (primeAt n)).mp
333         ⟨c.names t, (c.torsionTest_correct n t).mp ht⟩
334 
335 /-- Finite and infinite copied domains both provide positive enumeration tests. -/
336 theorem spectrumSearchEnumeration_of_any_copy (X : ℕ → Bool) (B : Set Prime)
337     (h : HasOracleGroupCopy X (spectrumSubgroup B)) :
338     Nonempty (OracleSearchEnumeration X {n | primeAt n ∈ B}) := by
339   rcases h with hf | hi
340   · obtain ⟨c⟩ := hf
341     let : Finite (spectrumSubgroup B) := Finite.of_equiv (Fin c.size) c.names
342     have hA : {n | primeAt n ∈ B}.Finite := by
343       simpa only [spectrumSubgroup_hasPrimeTorsion_iff] using
344         finite_group_primeSpectrum_indices (spectrumSubgroup B)
345     exact ⟨finiteSearchEnumeration X _ hA⟩
346   · obtain ⟨c⟩ := hi
347     exact ⟨spectrumSearchEnumeration_of_copy X B c⟩
348 
349 /-- Positive enumeration gives an actual copy in the finite-or-infinite naming
350 convention. The finite branch uses its fixed finite table nonuniformly. -/
351 theorem oracle_any_spectrum_copy_of_searchEnumeration (X : ℕ → Bool) (B : Set Prime)
352     (E : OracleSearchEnumeration X {n | primeAt n ∈ B}) :
353     HasOracleGroupCopy X (spectrumSubgroup B) := by
354   rcases finite_or_infinite (spectrumSubgroup B) with hfinite | hinfinite
355   · let := hfinite
356     exact hasOracleGroupCopy_of_finite X _
357   · let := hinfinite
358     exact Or.inr (oracle_spectrum_copy_of_searchEnumeration E)
359 
360 /-- Exact prime-spectrum criterion with explicit standard positive-search
361 semantics: finite and infinite copied domains are both covered. -/
362 theorem oracle_spectrum_copy_iff_searchEnumeration (X : ℕ → Bool) (B : Set Prime) :
363     HasOracleGroupCopy X (spectrumSubgroup B) ↔
364       Nonempty (OracleSearchEnumeration X {n | primeAt n ∈ B}) := by
365   constructor
366   · exact spectrumSearchEnumeration_of_any_copy X B
367   · rintro ⟨E⟩
368     exact oracle_any_spectrum_copy_of_searchEnumeration X B E
369 
370 end RealizationBoundaries

Back to source controls