ComputableNormalCodes.lean

1 import RealizationBoundaries.ComputablePresentations
2 import RealizationBoundaries.RootAlgorithm
3 import RealizationBoundaries.RationalComputability
4 import RealizationBoundaries.ComputableQuotientCodes
5 
6 /-! # Native oracle computations on finite normal-form codes -/
7 set_option autoImplicit false
8 set_option backward.isDefEq.respectTransparency false
9 noncomputable section
10 namespace RealizationBoundaries
11 
12 /-- The actual paired-prime mask, expressed using the prime-counting index. -/
13 def pairedMask (a : ℕ → Bool) (p : ℕ) : ℕ :=
14   if (if a (Nat.count Nat.Prime p / 2) then 1 else 0) = Nat.count Nat.Prime p % 2
15   then 1 else 0
16 
17 theorem pairedMask_exact (a : ℕ → Bool) (p : Prime) :
18     pairedMask a p.val = 1 ↔ p ∈ pairedSelector a := by
19   have hindex : primeAt (Nat.count Nat.Prime p.val) = p :=
20     Subtype.ext (Nat.nth_count p.property)
21   constructor
22   · intro h
23     have hm : (if a (Nat.count Nat.Prime p.val / 2) then 1 else 0) =
24         Nat.count Nat.Prime p.val % 2 := by
25       by_contra hm
26       simp [pairedMask, hm] at h
27     refine ⟨Nat.count Nat.Prime p.val / 2, ?_⟩
28     have he : chosenIndex a (Nat.count Nat.Prime p.val / 2) = Nat.count Nat.Prime p.val := by
29       unfold chosenIndex
30       cases ha : a (Nat.count Nat.Prime p.val / 2) <;> simp [ha] at hm ⊢ <;> omega
31     change primeAt (chosenIndex a (Nat.count Nat.Prime p.val / 2)) = p
32     rw [he, hindex]
33   · rintro ⟨n, hn⟩
34     have hi : Nat.count Nat.Prime p.val = chosenIndex a n := by
35       rw [← hn]
36       exact Nat.count_nth_of_infinite Nat.infinite_setOfPred_prime _
37     have hdiv : chosenIndex a n / 2 = n := by
38       unfold chosenIndex
39       split <;> omega
40     have hmod : chosenIndex a n % 2 = if a n then 1 else 0 := by
41       unfold chosenIndex
42       split <;> omega
43     simp [pairedMask, hi, hdiv, hmod]
44 
45 namespace OracleComputable
46 variable {X : ℕ → Bool} {f g : ℕ → ℕ}
47 
48 theorem ncAdd (hf : OracleComputable X f) (hg : OracleComputable X g) :
49     OracleComputable X (fun n => f n + g n) :=
50   (of_computable ((Primrec.nat_add.comp (Primrec.fst.comp Primrec.unpair)
51     (Primrec.snd.comp Primrec.unpair)).to_comp)).comp (hf.pair hg) |>.of_eq
52     (fun n => by simp)
53 
54 theorem ncSub (hf : OracleComputable X f) (hg : OracleComputable X g) :
55     OracleComputable X (fun n => f n - g n) :=
56   (of_computable ((Primrec.nat_sub.comp (Primrec.fst.comp Primrec.unpair)
57     (Primrec.snd.comp Primrec.unpair)).to_comp)).comp (hf.pair hg) |>.of_eq
58     (fun n => by simp)
59 
60 theorem ncMod (hf : OracleComputable X f) (hg : OracleComputable X g) :
61     OracleComputable X (fun n => f n % g n) :=
62   (of_computable ((Primrec.nat_mod.comp (Primrec.fst.comp Primrec.unpair)
63     (Primrec.snd.comp Primrec.unpair)).to_comp)).comp (hf.pair hg) |>.of_eq
64     (fun n => by simp)
65 
66 theorem ncEq (hf : OracleComputable X f) (hg : OracleComputable X g) :
67     OracleComputable X (fun n => if f n = g n then 1 else 0) := by
68   have he : Computable (fun k : ℕ => if k.unpair.1 = k.unpair.2 then 1 else 0) :=
69     (Primrec.ite (Primrec.eq.comp (Primrec.fst.comp Primrec.unpair)
70       (Primrec.snd.comp Primrec.unpair)) (Primrec.const 1) (Primrec.const 0)).to_comp
71   exact (of_computable he).comp (hf.pair hg) |>.of_eq (fun n => by simp)
72 
73 /-- Native primitive recursion with a parameter and a total state. -/
74 theorem ncRec {b s : ℕ → ℕ} (hb : OracleComputable X b) (hs : OracleComputable X s) :
75     OracleComputable X (fun z => Nat.rec (b z.unpair.1)
76       (fun k r => s (Nat.pair z.unpair.1 (Nat.pair k r))) z.unpair.2) := by
77   apply (Nat.RecursiveIn.prec hb hs).of_eq
78   intro n
79   dsimp
80   induction n.unpair.2 with
81   | zero => rfl
82   | succ k ih =>
83     dsimp only
84     rw [ih]
85     simp
86 
87 end OracleComputable
88 
89 /-- A true oracle query, followed by primitive prime indexing and parity. -/
90 theorem pairedMask_oracleComputable (a X : ℕ → Bool) (ha : SelectorReducible a X) :
91     OracleComputable X (pairedMask a) := by
92   have hb : OracleComputable X (fun n => if a n then 1 else 0) := RecursiveIn.iff_nat.mp ha
93   have hc : Primrec (fun n => Nat.count Nat.Prime n) := primrec_prime_count
94   have hi : OracleComputable X (fun n => Nat.count Nat.Prime n / 2) :=
95     OracleComputable.of_computable ((Primrec.nat_div.comp hc (Primrec.const 2)).to_comp)
96   have hp : OracleComputable X (fun n => Nat.count Nat.Prime n % 2) :=
97     OracleComputable.of_computable ((Primrec.nat_mod.comp hc (Primrec.const 2)).to_comp)
98   exact (hb.comp hi).ncEq hp
99 
100 /-- A total decoder of finite residue lists from native natural codes. -/
101 def decodeResidues (n : ℕ) : List ℕ := (Encodable.decode (α := List ℕ) n).getD []
102 
103 @[simp] theorem decodeResidues_encode (d : List ℕ) : decodeResidues (Encodable.encode d) = d := by
104   simp [decodeResidues]
105 
106 theorem primrec_decodeResidues : Primrec decodeResidues :=
107   Primrec.option_getD.comp Primrec.decode (Primrec.const [])
108 
109 /-- Native oracle finite-loop construction; output codes are ordinary finite lists. -/
110 def residueLoop (f : ℕ → ℕ) (input : ℕ) (N : ℕ) : List ℕ :=
111   Nat.rec [] (fun i xs => xs ++ [f (Nat.pair input i)]) N
112 
113 theorem residueLoop_eq_ofFn (f : ℕ → ℕ) (input N : ℕ) :
114     residueLoop f input N = List.ofFn (fun i : Fin N => f (Nat.pair input i.val)) := by
115   induction N with
116   | zero => rfl
117   | succ N ih =>
118     change residueLoop f input N ++ [f (Nat.pair input N)] = _
119     rw [ih, List.ofFn_succ_last]
120     rfl
121 
122 /-- Every cell may query the oracle; primitive recursion certifies the complete bounded loop. -/
123 theorem residueLoop_oracleComputable {X : ℕ → Bool} {f : ℕ → ℕ}
124     (hf : OracleComputable X f) :
125     OracleComputable X (fun z => Encodable.encode (residueLoop f z.unpair.1 z.unpair.2)) := by
126   have hcat : Computable (fun n : ℕ => Encodable.encode
127       (decodeResidues n.unpair.1 ++ [n.unpair.2])) :=
128     Primrec.encode.to_comp.comp ((Primrec.list_concat.comp
129       (primrec_decodeResidues.comp (Primrec.fst.comp Primrec.unpair))
130       (Primrec.snd.comp Primrec.unpair)).to_comp)
131   have hstep : OracleComputable X (fun z => Encodable.encode
132       (decodeResidues z.unpair.2.unpair.2 ++
133         [f (Nat.pair z.unpair.1 z.unpair.2.unpair.1)])) := by
134     exact (OracleComputable.of_computable hcat).comp
135       ((OracleComputable.right.comp OracleComputable.right).pair
136         (hf.comp (OracleComputable.left.pair
137           (OracleComputable.left.comp OracleComputable.right)))) |>.of_eq
138       (fun n => by simp)
139   apply ((OracleComputable.const (Encodable.encode ([] : List ℕ))).ncRec hstep).of_eq
140   intro n
141   dsimp
142   induction n.unpair.2 with
143   | zero => rfl
144   | succ k ih =>
145     simp only [Nat.unpair_pair] at ih ⊢
146     rw [ih, decodeResidues_encode]
147     rfl
148 
149 /-- Finite residue-list equality uses only bounded prime-coordinate tests. -/
150 def ResiduesEqual (d e : List ℕ) : Prop :=
151   ∀ p < max d.length e.length, p.Prime → d.getD p 0 % p = e.getD p 0 % p
152 
153 instance residuesEqual_decidable : DecidableRel ResiduesEqual := by
154   unfold ResiduesEqual
155   infer_instance
156 
157 theorem residuesEqual_iff (d e : List ℕ) :
158     ResiduesEqual d e ↔ finiteCodeValue d = finiteCodeValue e := by
159   constructor
160   · intro h
161     funext p
162     by_cases hp : p.val < max d.length e.length
163     · apply (ZMod.natCast_eq_natCast_iff _ _ p.val).mpr
164       exact h p.val hp p.property
165     · have hd : d.length ≤ p.val := (le_max_left _ _).trans (Nat.le_of_not_gt hp)
166       have he : e.length ≤ p.val := (le_max_right _ _).trans (Nat.le_of_not_gt hp)
167       rw [finiteCodeValue_eq_zero d p hd, finiteCodeValue_eq_zero e p he]
168   · intro h p _ hp
169     have hh := congrArg (fun x : Ambient => (x ⟨p, hp⟩).val) h
170     simpa only [finiteCodeValue, ZMod.val_natCast, ← List.getD_eq_getElem?_getD] using hh
171 
172 theorem primrec_residuesEqual : PrimrecRel ResiduesEqual := by
173   let dl : Primrec (fun z : ℕ × (List ℕ × List ℕ) => z.2.1) := Primrec.fst.comp Primrec.snd
174   let el : Primrec (fun z : ℕ × (List ℕ × List ℕ) => z.2.2) := Primrec.snd.comp Primrec.snd
175   have hr : PrimrecRel (fun p : ℕ => fun de : List ℕ × List ℕ =>
176       p.Prime → de.1.getD p 0 % p = de.2.getD p 0 % p) :=
177     ((primrec_prime_predicate.comp Primrec.fst).not.or
178       (Primrec.eq.comp
179         (Primrec.nat_mod.comp ((Primrec.list_getD 0).comp dl Primrec.fst) Primrec.fst)
180         (Primrec.nat_mod.comp ((Primrec.list_getD 0).comp el Primrec.fst) Primrec.fst))).of_eq
181           (fun _ => by simp only [or_iff_not_imp_left, not_not])
182   exact hr.forall_mem_list.comp
183     (Primrec.list_range.comp (Primrec.nat_max.comp (Primrec.list_length.comp Primrec.fst)
184       (Primrec.list_length.comp Primrec.snd))) Primrec.id |>.of_eq
185         (fun _ => by simp only [List.mem_range, id_eq, ResiduesEqual])
186 
187 /-- The actual finite-support correction represented by one native list. -/
188 def finiteResidues (d : List ℕ) : finiteSupport := by
189   refine ⟨finiteCodeValue d, ?_⟩
190   apply (Set.finite_Iio d.length).preimage Subtype.val_injective.injOn |>.subset
191   intro p hp
192   by_contra hn
193   exact hp (finiteCodeValue_eq_zero d p (Nat.le_of_not_gt hn))
194 
195 abbrev NativeNormalCode := RationalCode × List ℕ
196 
197 /-- The names denote the original ambient paired-prime group, with no abstract replacement. -/
198 def nativeNormalValue (a : ℕ → Bool) (c : NativeNormalCode) : pairedGroup a :=
199   ⟨rationalSection (pairedSelector a) (RationalCode.value c.1) + finiteCodeValue c.2,
200     (pairedGroup a).add_mem (rationalSection_mem _ _)
201       (finiteSupport_le_preimage _ (finiteResidues c.2).property)⟩
202 
203 theorem nativeNormalValue_surjective (a : ℕ → Bool) :
204     Function.Surjective (nativeNormalValue a) := by
205   intro x
206   obtain ⟨r, d, hd⟩ := normalForm_exists (pairedSelector a) x
207   obtain ⟨q, hq⟩ := RationalCode.value_surjective r
208   obtain ⟨code, hc⟩ := finiteCodeValue_represents d
209   refine ⟨(q, code), Subtype.ext ?_⟩
210   change rationalSection (pairedSelector a) (RationalCode.value q) + finiteCodeValue code = x.val
211   rw [hq, hc, ← hd]
212 
213 def nativeNormalEqual (c e : NativeNormalCode) : Bool :=
214   RationalCode.equal c.1 e.1 && decide (ResiduesEqual c.2 e.2)
215 
216 theorem nativeNormalEqual_exact (a : ℕ → Bool) (c e : NativeNormalCode) :
217     nativeNormalEqual c e = true ↔ nativeNormalValue a c = nativeNormalValue a e := by
218   rw [nativeNormalEqual, Bool.and_eq_true, RationalCode.equal_iff, decide_eq_true_eq,
219     residuesEqual_iff]
220   constructor
221   · rintro ⟨hr, hd⟩
222     apply Subtype.ext
223     change rationalSection _ _ + _ = rationalSection _ _ + _
224     rw [hr, hd]
225   · intro h
226     have hh := normalForm_unique (pairedSelector_infinite a) _ _
227       (finiteResidues c.2) (finiteResidues e.2) (congrArg Subtype.val h)
228     exact ⟨hh.1, congrArg Subtype.val hh.2⟩
229 
230 theorem primrec_nativeNormalEqual : Primrec₂ nativeNormalEqual :=
231   Primrec.and.comp
232     (RationalCode.primrec_equal.comp (Primrec.fst.comp Primrec.fst) (Primrec.fst.comp Primrec.snd))
233     ((primrec_residuesEqual.comp (Primrec.snd.comp Primrec.fst)
234       (Primrec.snd.comp Primrec.snd)).decide)
235 
236 /-- Total decoding admits redundant raw natural codes, with native decidable equality. -/
237 def decodeNormalCode (n : ℕ) : NativeNormalCode :=
238   (Encodable.decode (α := NativeNormalCode) n).getD default
239 
240 @[simp] theorem decodeNormalCode_encode (c : NativeNormalCode) :
241     decodeNormalCode (Encodable.encode c) = c := by
242   rw [decodeNormalCode, Encodable.encodek]
243   rfl
244 
245 theorem primrec_decodeNormalCode : Primrec decodeNormalCode :=
246   Primrec.option_getD.comp Primrec.decode (Primrec.const default)
247 
248 /-- A primitive bound containing both torsion inputs and all cocycle denominator primes. -/
249 def normalAddBound (c e : NativeNormalCode) : ℕ :=
250   max (max c.2.length e.2.length)
251     (RationalCode.normalDenominator c.1 * RationalCode.normalDenominator e.1 + 1)
252 
253 theorem primrec_normalAddBound : Primrec₂ normalAddBound :=
254   Primrec.nat_max.comp
255     (Primrec.nat_max.comp (Primrec.list_length.comp (Primrec.snd.comp Primrec.fst))
256       (Primrec.list_length.comp (Primrec.snd.comp Primrec.snd)))
257     (Primrec.succ.comp (Primrec.nat_mul.comp
258       (RationalCode.primrec_normalDenominator.comp (Primrec.fst.comp Primrec.fst))
259       (RationalCode.primrec_normalDenominator.comp (Primrec.fst.comp Primrec.snd))))
260 
261 /-- One exact natural-number residue cell for normal-form addition. -/
262 def normalAddCell (a : ℕ → Bool) (z : ℕ) : ℕ :=
263   let c := decodeNormalCode z.unpair.1.unpair.1
264   let e := decodeNormalCode z.unpair.1.unpair.2
265   let p := z.unpair.2
266   (c.2.getD p 0 + e.2.getD p 0 + pairedMask a p *
267     (RationalCode.primeResidue c.1 p + RationalCode.primeResidue e.1 p + p -
268       RationalCode.primeResidue (RationalCode.add c.1 e.1) p)) % p
269 
270 theorem normalAddCell_cast (a : ℕ → Bool) (c e : NativeNormalCode) (p : Prime) :
271     (normalAddCell a (Nat.pair (Nat.pair (Encodable.encode c) (Encodable.encode e)) p.val) :
272       Coordinate p) = finiteCodeValue c.2 p + finiteCodeValue e.2 p +
273         sectionDefect (pairedSelector a) (RationalCode.value c.1) (RationalCode.value e.1) p := by
274   have hb : RationalCode.primeResidue (RationalCode.add c.1 e.1) p.val ≤
275       RationalCode.primeResidue c.1 p.val + RationalCode.primeResidue e.1 p.val + p.val :=
276     (RationalCode.primeResidue_lt _ p.property).le.trans (Nat.le_add_left _ _)
277   simp only [normalAddCell, Nat.unpair_pair, decodeNormalCode_encode, ZMod.natCast_mod,
278     Nat.cast_add, Nat.cast_mul, Nat.cast_sub hb, ZMod.natCast_self, add_zero,
279     RationalCode.primeResidue_cast, RationalCode.value_add]
280   by_cases hp : p ∈ pairedSelector a
281   · have hm := (pairedMask_exact a p).mpr hp
282     simp only [hm, Nat.cast_one, one_mul, sectionDefect, Pi.sub_apply, Pi.add_apply,
283       rationalSection, ite_eq_left hp, finiteCodeValue, ← List.getD_eq_getElem?_getD]
284   · have hm : pairedMask a p.val = 0 := by
285       have hn : pairedMask a p.val ≠ 1 := (pairedMask_exact a p).not.mpr hp
286       have h01 : pairedMask a p.val = 0 ∨ pairedMask a p.val = 1 := by
287         unfold pairedMask
288         split_ifs <;> simp
289       exact h01.resolve_right hn
290     simp [hm, sectionDefect, rationalSection, hp, finiteCodeValue,
291       ← List.getD_eq_getElem?_getD]
292 
293 /-- The finite output correction for two raw natural normal-form codes. -/
294 def normalAddResidues (a : ℕ → Bool) (c e : NativeNormalCode) : List ℕ :=
295   residueLoop (normalAddCell a) (Nat.pair (Encodable.encode c) (Encodable.encode e))
296     (normalAddBound c e)
297 
298 theorem normalAddResidues_exact (a : ℕ → Bool) (c e : NativeNormalCode) :
299     finiteCodeValue (normalAddResidues a c e) =
300       finiteCodeValue c.2 + finiteCodeValue e.2 +
301         sectionDefect (pairedSelector a) (RationalCode.value c.1) (RationalCode.value e.1) := by
302   funext p
303   by_cases hp : p.val < normalAddBound c e
304   · rw [normalAddResidues, residueLoop_eq_ofFn]
305     simp only [finiteCodeValue, List.getElem?_ofFn, hp, dite_true, Option.getD_some]
306     exact normalAddCell_cast a c e p
307   · have hpN := Nat.le_of_not_gt hp
308     have hc : c.2.length ≤ p.val :=
309       (le_max_left _ _).trans ((le_max_left _ _).trans hpN)
310     have he : e.2.length ≤ p.val :=
311       (le_max_right _ _).trans ((le_max_left _ _).trans hpN)
312     have hdef : sectionDefect (pairedSelector a) (RationalCode.value c.1)
313         (RationalCode.value e.1) p = 0 := by
314       by_contra hn
315       have hdvd := sectionDefect_support (pairedSelector a)
316         (RationalCode.value c.1) (RationalCode.value e.1) hn
317       have hle := Nat.le_of_dvd
318         (Nat.mul_pos (RationalCode.value c.1).den_pos (RationalCode.value e.1).den_pos) hdvd
319       have hb := (le_max_right (max c.2.length e.2.length)
320         (RationalCode.normalDenominator c.1 * RationalCode.normalDenominator e.1 + 1)).trans hpN
321       rw [← (RationalCode.normal_fields c.1).2, ← (RationalCode.normal_fields e.1).2] at hb
322       omega
323     have hlen : (normalAddResidues a c e).length = normalAddBound c e := by
324       rw [normalAddResidues, residueLoop_eq_ofFn, List.length_ofFn]
325     rw [finiteCodeValue_eq_zero _ p (hlen.symm ▸ hpN)]
326     simp only [Pi.add_apply, finiteCodeValue_eq_zero c.2 p hc,
327       finiteCodeValue_eq_zero e.2 p he, hdef, add_zero]
328 
329 def nativeNormalAdd (a : ℕ → Bool) (c e : NativeNormalCode) : NativeNormalCode :=
330   (RationalCode.add c.1 e.1, normalAddResidues a c e)
331 
332 theorem nativeNormalAdd_exact (a : ℕ → Bool) (c e : NativeNormalCode) :
333     nativeNormalValue a (nativeNormalAdd a c e) = nativeNormalValue a c + nativeNormalValue a e := by
334   apply Subtype.ext
335   change rationalSection _ (RationalCode.value (RationalCode.add c.1 e.1)) +
336     finiteCodeValue (normalAddResidues a c e) = _
337   rw [RationalCode.value_add, normalAddResidues_exact]
338   change rationalSection _ _ + (finiteCodeValue c.2 + finiteCodeValue e.2 +
339     (rationalSection _ _ + rationalSection _ _ - rationalSection _ _)) =
340     (rationalSection _ _ + finiteCodeValue c.2) + (rationalSection _ _ + finiteCodeValue e.2)
341   abel
342 
343 /-- Native oracle computation of the actual cocycle correction at one prime value. -/
344 theorem normalAddCell_oracleComputable (a X : ℕ → Bool) (ha : SelectorReducible a X) :
345     OracleComputable X (normalAddCell a) := by
346   let l : Primrec (fun z : ℕ => decodeNormalCode z.unpair.1.unpair.1) :=
347     primrec_decodeNormalCode.comp
348       ((Primrec.fst.comp Primrec.unpair).comp (Primrec.fst.comp Primrec.unpair))
349   let r : Primrec (fun z : ℕ => decodeNormalCode z.unpair.1.unpair.2) :=
350     primrec_decodeNormalCode.comp
351       ((Primrec.snd.comp Primrec.unpair).comp (Primrec.fst.comp Primrec.unpair))
352   let p : Primrec (fun z : ℕ => z.unpair.2) := Primrec.snd.comp Primrec.unpair
353   let q := Primrec.fst.comp l
354   let t := Primrec.fst.comp r
355   have hb : Primrec (fun z : ℕ =>
356       (decodeNormalCode z.unpair.1.unpair.1).2.getD z.unpair.2 0 +
357         (decodeNormalCode z.unpair.1.unpair.2).2.getD z.unpair.2 0) :=
358     Primrec.nat_add.comp ((Primrec.list_getD 0).comp (Primrec.snd.comp l) p)
359       ((Primrec.list_getD 0).comp (Primrec.snd.comp r) p)
360   have hd : Primrec (fun z : ℕ =>
361       RationalCode.primeResidue (decodeNormalCode z.unpair.1.unpair.1).1 z.unpair.2 +
362         RationalCode.primeResidue (decodeNormalCode z.unpair.1.unpair.2).1 z.unpair.2 + z.unpair.2 -
363         RationalCode.primeResidue (RationalCode.add (decodeNormalCode z.unpair.1.unpair.1).1
364           (decodeNormalCode z.unpair.1.unpair.2).1) z.unpair.2) :=
365     Primrec.nat_sub.comp
366       (Primrec.nat_add.comp (Primrec.nat_add.comp
367         (RationalCode.primrec_primeResidue.comp q p)
368         (RationalCode.primrec_primeResidue.comp t p)) p)
369       (RationalCode.primrec_primeResidue.comp (RationalCode.primrec_add.comp q t) p)
370   exact ((OracleComputable.of_computable hb.to_comp).ncAdd
371     (((pairedMask_oracleComputable a X ha).comp (OracleComputable.of_computable p.to_comp)).mul
372       (OracleComputable.of_computable hd.to_comp))).ncMod
373         (OracleComputable.of_computable p.to_comp)
374 
375 /-- Actual finite normal-form addition, encoded as a natural output. -/
376 def rawNormalAdd (a : ℕ → Bool) (i j : ℕ) : ℕ :=
377   Encodable.encode (nativeNormalAdd a (decodeNormalCode i) (decodeNormalCode j))
378 
379 def rawNormalEqual (i j : ℕ) : ℕ :=
380   if nativeNormalEqual (decodeNormalCode i) (decodeNormalCode j) then 0 else 1
381 
382 theorem rawNormalAdd_oracleComputable (a X : ℕ → Bool) (ha : SelectorReducible a X) :
383     OracleComputable X (fun k => rawNormalAdd a k.unpair.1 k.unpair.2) := by
384   let l : Primrec (fun z : ℕ => decodeNormalCode z.unpair.1) :=
385     primrec_decodeNormalCode.comp (Primrec.fst.comp Primrec.unpair)
386   let r : Primrec (fun z : ℕ => decodeNormalCode z.unpair.2) :=
387     primrec_decodeNormalCode.comp (Primrec.snd.comp Primrec.unpair)
388   have hq : OracleComputable X (fun z : ℕ => Encodable.encode
389       (RationalCode.add (decodeNormalCode z.unpair.1).1 (decodeNormalCode z.unpair.2).1)) :=
390     OracleComputable.of_computable (Primrec.encode.comp
391       (RationalCode.primrec_add.comp (Primrec.fst.comp l) (Primrec.fst.comp r))).to_comp
392   have hi : OracleComputable X (fun z : ℕ => Nat.pair
393       (Encodable.encode (decodeNormalCode z.unpair.1))
394       (Encodable.encode (decodeNormalCode z.unpair.2))) :=
395     (OracleComputable.of_computable (Primrec.encode.comp l).to_comp).pair
396       (OracleComputable.of_computable (Primrec.encode.comp r).to_comp)
397   have hn : OracleComputable X (fun z : ℕ =>
398       normalAddBound (decodeNormalCode z.unpair.1) (decodeNormalCode z.unpair.2)) :=
399     OracleComputable.of_computable (primrec_normalAddBound.comp l r).to_comp
400   have hd : OracleComputable X (fun z : ℕ => Encodable.encode (normalAddResidues a
401       (decodeNormalCode z.unpair.1) (decodeNormalCode z.unpair.2))) := by
402     apply ((residueLoop_oracleComputable (normalAddCell_oracleComputable a X ha)).comp
403       (hi.pair hn)).of_eq
404     intro z
405     simp only [Nat.unpair_pair]
406     rfl
407   apply (hq.pair hd).of_eq
408   intro z
409   exact (Encodable.encode_prod_val _ _).symm
410 
411 theorem rawNormalEqual_computable :
412     Computable (fun k : ℕ => rawNormalEqual k.unpair.1 k.unpair.2) := by
413   have he : Primrec (fun k : ℕ =>
414       nativeNormalEqual (decodeNormalCode k.unpair.1) (decodeNormalCode k.unpair.2)) :=
415     primrec_nativeNormalEqual.comp
416       (primrec_decodeNormalCode.comp (Primrec.fst.comp Primrec.unpair))
417       (primrec_decodeNormalCode.comp (Primrec.snd.comp Primrec.unpair))
418   exact (Primrec.ite (Primrec.eq.comp he (Primrec.const true))
419     (Primrec.const 0) (Primrec.const 1)).to_comp
420 
421 /-- Genuine raw oracle codes for the original paired-prime group. -/
422 def pairedRawCodes (a X : ℕ → Bool) (ha : SelectorReducible a X) :
423     OracleRawGroupCodes X (pairedGroup a) where
424   names n := nativeNormalValue a (decodeNormalCode n)
425   names_surjective := by
426     intro x
427     obtain ⟨c, hc⟩ := nativeNormalValue_surjective a x
428     refine ⟨Encodable.encode c, ?_⟩
429     change nativeNormalValue a (decodeNormalCode (Encodable.encode c)) = x
430     rw [decodeNormalCode_encode]
431     exact hc
432   zero := Encodable.encode (((((0 : ℕ), (0 : ℕ)), (0 : ℕ)), ([] : List ℕ)) : NativeNormalCode)
433   add := rawNormalAdd a
434   equal := rawNormalEqual
435   zero_spec := by
436     rw [decodeNormalCode_encode]
437     apply Subtype.ext
438     change rationalSection (pairedSelector a) (RationalCode.value ((0,0),0)) +
439       finiteCodeValue [] = 0
440     have hr : RationalCode.value ((0,0),0) = 0 := by simp [RationalCode.value_eq,
441       RationalCode.positive, RationalCode.negative, RationalCode.denominator]
442     rw [hr, rationalSection_zero, zero_add]
443     funext p
444     simp [finiteCodeValue]
445   add_spec i j := by
446     change nativeNormalValue a (decodeNormalCode (Encodable.encode _)) = _
447     rw [decodeNormalCode_encode]
448     exact nativeNormalAdd_exact a _ _
449   equal_spec i j := by
450     have he := nativeNormalEqual_exact a (decodeNormalCode i) (decodeNormalCode j)
451     cases hb : nativeNormalEqual (decodeNormalCode i) (decodeNormalCode j) <;>
452       simp [rawNormalEqual, hb] at he ⊢
453     · exact he
454     · exact he
455   add_computable := rawNormalAdd_oracleComputable a X ha
456   equal_computable := OracleComputable.of_computable rawNormalEqual_computable
457 
458 /-- Uniform construction from the genuine oracle reduction, with bijective natural names. -/
459 def pairedOracleCopy (a X : ℕ → Bool) (ha : SelectorReducible a X) :
460     OracleGroupCopy X (pairedGroup a) :=
461   (pairedRawCodes a X ha).toOracleGroupCopy
462 
463 /-- Monograph 8.3: the exact oracle criterion for unmarked copies. -/
464 theorem paired_oracle_copy_iff (a X : ℕ → Bool) :
465     Nonempty (OracleGroupCopy X (pairedGroup a)) ↔ SelectorReducible a X := by
466   constructor
467   · exact oracle_copy_exists_implies_selector_reducible a X
468   · intro ha
469     exact ⟨pairedOracleCopy a X ha⟩
470 
471 end RealizationBoundaries

Back to source controls