ListingSearchEquivalence.lean

1 import RealizationBoundaries.SearchEnumerableSpectrum
2 
3 /-! # Equivalence of positive witness tests and actual oracle stage listings -/
4 set_option autoImplicit false
5 set_option backward.isDefEq.respectTransparency false
6 noncomputable section
7 namespace RealizationBoundaries
8 attribute [local instance] Classical.propDecidable
9 
10 /-- An actual listing emits a finite list at every natural stage, with native
11 oracle computation of its encoded list and exact eventual membership. Repeated
12 emissions are permitted. -/
13 structure OracleStageListing (X : ℕ → Bool) (A : Set ℕ) where
14   stage : ℕ → List ℕ
15   stage_computable : OracleComputable X (fun s => Encodable.encode (stage s))
16   stage_spec : ∀ n, n ∈ A ↔ ∃ s, n ∈ stage s
17 
18 /-- A positive test result emits its candidate index plus one; zero is a blank. -/
19 def listingSuccessCell (test : ℕ → ℕ) (k : ℕ) : ℕ :=
20   if test k.unpair.2 = 0 then k.unpair.2.unpair.1 + 1 else 0
21 
22 /-- Remove blank emissions and undo the positive coding. -/
23 def cleanListing (L : List ℕ) : List ℕ :=
24   L.filterMap (fun n => if n = 0 then none else some (n-1))
25 
26 def searchStageListing (test : ℕ → ℕ) (s : ℕ) : List ℕ :=
27   cleanListing (residueLoop (listingSuccessCell test) 0 s)
28 
29 theorem searchStageListing_mem (test : ℕ → ℕ) (s n : ℕ) :
30     n ∈ searchStageListing test s ↔
31       ∃ k < s, k.unpair.1 = n ∧ test k = 0 := by
32   constructor
33   · intro hn
34     obtain ⟨v, hv, hout⟩ := List.mem_filterMap.mp hn
35     rw [residueLoop_eq_ofFn] at hv
36     obtain ⟨i, hi⟩ := List.mem_ofFn.mp hv
37     have hc : v = if test i.val = 0 then i.val.unpair.1+1 else 0 := by
38       simpa only [listingSuccessCell, Nat.unpair_pair] using hi.symm
39     by_cases ht : test i.val = 0
40     · rw [hc, ite_eq_left ht] at hout
41       have hn' : i.val.unpair.1 = n := by simpa using hout
42       exact ⟨i.val, i.isLt, hn', ht⟩
43     · rw [hc, ite_eq_right ht] at hout
44       simp at hout
45   · rintro ⟨k, hk, hkn, ht⟩
46     apply List.mem_filterMap.mpr
47     refine ⟨k.unpair.1+1, ?_, ?_⟩
48     · rw [residueLoop_eq_ofFn]
49       apply List.mem_ofFn.mpr
50       refine ⟨⟨k, hk⟩, ?_⟩
51       simp [listingSuccessCell, ht]
52     · simp [hkn]
53 
54 theorem listingSuccessCell_computable {X : ℕ → Bool} {test : ℕ → ℕ}
55     (ht : OracleComputable X test) : OracleComputable X (listingSuccessCell test) := by
56   have hs := (ht.comp OracleComputable.right).isZero
57   have hv : OracleComputable X (fun k : ℕ => k.unpair.2.unpair.1+1) :=
58     OracleComputable.of_computable ((Primrec.succ.comp
59       ((Primrec.fst.comp Primrec.unpair).comp (Primrec.snd.comp Primrec.unpair))).to_comp)
60   exact (hs.mul hv).of_eq (fun k => by
61     simp only [listingSuccessCell]
62     split <;> simp_all)
63 
64 theorem primrec_cleanListing : Primrec cleanListing := by
65   have hcell : Primrec (fun p : List ℕ × ℕ => if p.2 = 0 then none else some (p.2-1)) :=
66     Primrec.ite (Primrec.eq.comp Primrec.snd (Primrec.const 0)) (Primrec.const none)
67       (Primrec.option_some.comp (Primrec.nat_sub.comp Primrec.snd (Primrec.const 1)))
68   exact Primrec.listFilterMap Primrec.id hcell
69 
70 theorem searchStageListing_computable {X : ℕ → Bool} {test : ℕ → ℕ}
71     (ht : OracleComputable X test) :
72     OracleComputable X (fun s => Encodable.encode (searchStageListing test s)) := by
73   have hloop := (residueLoop_oracleComputable (listingSuccessCell_computable ht)).comp
74     ((OracleComputable.const 0).pair OracleComputable.id)
75   have hclean : Computable (fun c : ℕ => Encodable.encode (cleanListing (decodeResidues c))) :=
76     (Primrec.encode.comp (primrec_cleanListing.comp primrec_decodeResidues)).to_comp
77   exact (OracleComputable.of_computable hclean).comp hloop |>.of_eq
78     (fun s => by simp [searchStageListing])
79 
80 /-- A total positive test gives a literal oracle-computable listing of exactly
81 its selected elements. Every witness appears at a finite stage. -/
82 def OracleSearchEnumeration.toStageListing {X : ℕ → Bool} {A : Set ℕ}
83     (E : OracleSearchEnumeration X A) : OracleStageListing X A where
84   stage := searchStageListing E.test
85   stage_computable := searchStageListing_computable E.test_computable
86   stage_spec := by
87     intro n
88     rw [E.test_spec]
89     constructor
90     · rintro ⟨t, ht⟩
91       refine ⟨Nat.pair n t + 1, (searchStageListing_mem E.test _ _).mpr ?_⟩
92       exact ⟨Nat.pair n t, Nat.lt_succ_self _, by simp, ht⟩
93     · rintro ⟨s, hs⟩
94       obtain ⟨k, _, hk, ht⟩ := (searchStageListing_mem E.test s n).mp hs
95       refine ⟨k.unpair.2, ?_⟩
96       rw [← hk, Nat.pair_unpair]
97       exact ht
98 
99 /-- Membership in each finite emitted list is an oracle-computable positive
100 candidate test, so listing semantics gives positive-witness semantics. -/
101 def OracleStageListing.toSearchEnumeration {X : ℕ → Bool} {A : Set ℕ}
102     (L : OracleStageListing X A) : OracleSearchEnumeration X A where
103   test := fun k => if k.unpair.1 ∈ L.stage k.unpair.2 then 0 else 1
104   test_computable := by
105     have hl : Primrec (fun k : ℕ => k.unpair.1) := Primrec.fst.comp Primrec.unpair
106     have hr : Primrec (fun k : ℕ => k.unpair.2) := Primrec.snd.comp Primrec.unpair
107     have hmem : Computable (fun k : ℕ =>
108         if k.unpair.1 ∈ decodeResidues k.unpair.2 then 0 else 1) :=
109       (Primrec.ite ((Primrec.eq.exists_mem_list).comp
110           (primrec_decodeResidues.comp hr) hl) (Primrec.const 0) (Primrec.const 1)).to_comp.of_eq
111         (fun k => by simp)
112     exact (OracleComputable.of_computable hmem).comp
113       (OracleComputable.left.pair (L.stage_computable.comp OracleComputable.right)) |>.of_eq
114         (fun k => by simp)
115   test_spec := by
116     intro n
117     simp only [Nat.unpair_pair, ite_eq_left_iff, one_ne_zero, imp_false, not_not]
118     exact L.stage_spec n
119 
120 /-- Explicit positive search and literal native oracle stage listings are the
121 same enumeration contract. -/
122 theorem oracle_searchEnumeration_iff_stageListing (X : ℕ → Bool) (A : Set ℕ) :
123     Nonempty (OracleSearchEnumeration X A) ↔ Nonempty (OracleStageListing X A) := by
124   constructor
125   · rintro ⟨E⟩
126     exact ⟨E.toStageListing⟩
127   · rintro ⟨L⟩
128     exact ⟨L.toSearchEnumeration⟩
129 
130 /-- Monograph 3.3 with literal enumeration semantics and actual finite or
131 infinite computable copies of the selected prime subgroup. -/
132 theorem oracle_spectrum_copy_iff_stageListing (X : ℕ → Bool) (B : Set Prime) :
133     HasOracleGroupCopy X (spectrumSubgroup B) ↔
134       Nonempty (OracleStageListing X {n | primeAt n ∈ B}) :=
135   (oracle_spectrum_copy_iff_searchEnumeration X B).trans
136     (oracle_searchEnumeration_iff_stageListing X {n | primeAt n ∈ B})
137 
138 end RealizationBoundaries

Back to source controls