EnumerationClosure.lean

1 import RealizationBoundaries.ListingSearchEquivalence
2 import RealizationBoundaries.OracleEnumerationNormalForm
3 
4 /-! # Equivalent native enumeration contracts and the exact spectrum criterion -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace RealizationBoundaries
8 
9 theorem oracleEnumerable_iff_searchEnumeration (X : ℕ → Bool) (A : Set ℕ) :
10     OracleEnumerable X A ↔ Nonempty (OracleSearchEnumeration X A) := by
11   constructor
12   · intro h
13     obtain ⟨test, hc, hs⟩ := oracleEnumerable_has_total_search X A h
14     exact ⟨⟨test, hc, hs⟩⟩
15   · rintro ⟨E⟩
16     exact E.toOracleEnumerable
17 
18 theorem oracleEnumerable_iff_stageListing (X : ℕ → Bool) (A : Set ℕ) :
19     OracleEnumerable X A ↔ Nonempty (OracleStageListing X A) :=
20   (oracleEnumerable_iff_searchEnumeration X A).trans
21     (oracle_searchEnumeration_iff_stageListing X A)
22 
23 /-- Monograph 3.3, also in the native partial-recursive-domain formulation. -/
24 theorem oracle_spectrum_copy_iff_enumerable (X : ℕ → Bool) (B : Set Prime) :
25     HasOracleGroupCopy X (spectrumSubgroup B) ↔
26       OracleEnumerable X {n | primeAt n ∈ B} :=
27   (oracle_spectrum_copy_iff_searchEnumeration X B).trans
28     (oracleEnumerable_iff_searchEnumeration X {n | primeAt n ∈ B}).symm
29 
30 end RealizationBoundaries

Back to source controls