SpectrumComputability.lean

1 import RealizationBoundaries.ComputablePresentations
2 import Mathlib.Computability.Halting
3 
4 /-! # The halting-complement prime spectrum and its actual presentation obstruction -/
5 set_option autoImplicit false
6 set_option backward.isDefEq.respectTransparency false
7 noncomputable section
8 namespace RealizationBoundaries
9 
10 /-- The actual diagonal halting set for Mathlib's partial-recursive program codes. -/
11 def diagonalHalting (n : ℕ) : Prop :=
12   ((Denumerable.ofNat Nat.Partrec.Code n).eval n).Dom
13 
14 /-- Relative computable enumeration is closed under ordinary computable preimages. -/
15 theorem oracleEnumerable_computable_preimage (X : ℕ → Bool) (A : Set ℕ)
16     (hA : OracleEnumerable X A) (g : ℕ → ℕ) (hg : Computable g) :
17     OracleEnumerable X {n | g n ∈ A} := by
18   obtain ⟨f, hf, hdom⟩ := hA
19   have hcomp : Nat.RecursiveIn {selectorOracle X} (fun n => f (g n)) := by
20     apply (Nat.RecursiveIn.comp hf (OracleComputable.of_computable hg)).of_eq
21     intro n
22     simp
23   exact ⟨_, hcomp, fun n => hdom (g n)⟩
24 
25 /-- The empty-information membership oracle contributes only a computable constant. -/
26 theorem recursiveIn_empty_selector_partrec {f : ℕ →. ℕ}
27     (hf : Nat.RecursiveIn {selectorOracle (fun _ => false)} f) : Nat.Partrec f := by
28   apply hf.partrec_of_oracle
29   intro g hg
30   rw [Set.mem_singleton_iff.mp hg]
31   change Nat.Partrec (fun _ : ℕ => Part.some (0 : ℕ))
32   exact Partrec.nat_iff.mp (Computable.const 0).partrec
33 
34 /-- The complement of the actual diagonal halting set is not computably enumerable.
35 The proof uses a code for the putative semidecision procedure on its own code. -/
36 theorem diagonalHalting_complement_not_enumerable :
37     ¬ OracleEnumerable (fun _ => false) {n | ¬ diagonalHalting n} := by
38   rintro ⟨f, hf, hdom⟩
39   obtain ⟨c, rfl⟩ := Nat.Partrec.Code.exists_code.mp (recursiveIn_empty_selector_partrec hf)
40   have h := hdom (Encodable.encode c)
41   have hh : (c.eval (Encodable.encode c)).Dom ↔ ¬ (c.eval (Encodable.encode c)).Dom := by
42     simpa only [Set.mem_ofPred_eq, diagonalHalting, Denumerable.ofNat_encode] using h
43   by_cases hc : (c.eval (Encodable.encode c)).Dom
44   · exact hh.mp hc hc
45   · exact hc (hh.mpr hc)
46 
47 /-- The literal index spectrum printed in Monograph 3.4. -/
48 def haltingIndexSpectrum : Set ℕ :=
49   {i | ∃ n, i = 2*n ∨ (i = 2*n+1 ∧ ¬ diagonalHalting n)}
50 
51 /-- Its actual prime-coordinate selector. -/
52 def haltingPrimeSpectrum : Set Prime := primeAt '' haltingIndexSpectrum
53 
54 @[simp] theorem even_mem_haltingIndexSpectrum (n : ℕ) : 2*n ∈ haltingIndexSpectrum :=
55   ⟨n, Or.inl rfl⟩
56 
57 @[simp] theorem odd_mem_haltingIndexSpectrum_iff (n : ℕ) :
58     2*n+1 ∈ haltingIndexSpectrum ↔ ¬ diagonalHalting n := by
59   constructor
60   · rintro ⟨m, h | ⟨h, hm⟩⟩
61     · omega
62     · have hmn : m = n := by omega
63       simpa [hmn] using hm
64   · intro h
65     exact ⟨n, Or.inr ⟨rfl, h⟩⟩
66 
67 @[simp] theorem primeAt_mem_haltingPrimeSpectrum_iff (n : ℕ) :
68     primeAt n ∈ haltingPrimeSpectrum ↔ n ∈ haltingIndexSpectrum := by
69   constructor
70   · rintro ⟨m, hm, hmn⟩
71     exact primeAt_injective hmn ▸ hm
72   · intro hn
73     exact ⟨n, hn, rfl⟩
74 
75 /-- Enumeration of the printed spectrum would enumerate the halting complement
76 by filtering the odd positions through an ordinary primitive recursive map. -/
77 theorem haltingPrimeSpectrum_not_enumerable :
78     ¬ OracleEnumerable (fun _ => false) {n | primeAt n ∈ haltingPrimeSpectrum} := by
79   intro h
80   have hg : Computable (fun n : ℕ => 2*n+1) :=
81     (Primrec.nat_add.comp (Primrec.nat_mul.comp (Primrec.const 2) Primrec.id)
82       (Primrec.const 1)).to_comp
83   obtain ⟨f, hf, hdom⟩ := oracleEnumerable_computable_preimage (fun _ => false)
84     {n | primeAt n ∈ haltingPrimeSpectrum} h (fun n => 2*n+1) hg
85   apply diagonalHalting_complement_not_enumerable
86   exact ⟨f, hf, fun n => (hdom n).trans (by simp)⟩
87 
88 /-- Monograph 3.4's no-computable-copy conclusion, for the actual infinite prime
89 support subgroup and the native ordinary-computability oracle convention. -/
90 theorem haltingSpectrum_no_computable_copy :
91     IsEmpty (OracleGroupCopy (fun _ => false) (spectrumSubgroup haltingPrimeSpectrum)) := by
92   constructor
93   intro c
94   exact haltingPrimeSpectrum_not_enumerable
95     (oracle_spectrum_copy_implies_enumerable _ _ c)
96 
97 /-- Every production prime coordinate has an actual natural index. -/
98 theorem primeAt_surjective : Function.Surjective primeAt := by
99   intro p
100   refine ⟨Nat.count Nat.Prime p.val, ?_⟩
101   exact Subtype.ext (Nat.nth_count p.property)
102 
103 /-- Infinitely many even coordinates survive in the halting-complement group. -/
104 def haltingSpectrumEvenSeed (n : ℕ) : spectrumSubgroup haltingPrimeSpectrum :=
105   ⟨primeSeed (primeAt (2*n)), (primeSeed_mem_spectrumSubgroup _ _).mpr
106     ((primeAt_mem_haltingPrimeSpectrum_iff _).mpr (even_mem_haltingIndexSpectrum n))⟩
107 
108 theorem haltingSpectrumEvenSeed_injective : Function.Injective haltingSpectrumEvenSeed := by
109   intro n m h
110   have hp := primeAt_injective (primeSeed_injective
111     (congrArg (fun z : spectrumSubgroup haltingPrimeSpectrum => z.val) h))
112   omega
113 
114 instance haltingSpectrum_infinite : Infinite (spectrumSubgroup haltingPrimeSpectrum) :=
115   Infinite.of_injective haltingSpectrumEvenSeed haltingSpectrumEvenSeed_injective
116 
117 /-- Native semidecision of the actual diagonal halting set. -/
118 theorem diagonalHalting_re : REPred diagonalHalting :=
119   (Nat.Partrec.Code.eval_part.comp (Computable.ofNat Nat.Partrec.Code) Computable.id).dom_re
120 
121 /-- The prime coordinates killed by the extra effectively enumerable relators. -/
122 def killedHaltingPrimes : Set Prime :=
123   {p | ∃ n, diagonalHalting n ∧ primeAt (2*n+1) = p}
124 
125 theorem haltingPrimeSpectrum_complement : haltingPrimeSpectrum = killedHaltingPrimesᶜ := by
126   classical
127   ext p
128   obtain ⟨i, rfl⟩ := primeAt_surjective p
129   rw [primeAt_mem_haltingPrimeSpectrum_iff]
130   change (∃ n, i = 2*n ∨ (i = 2*n+1 ∧ ¬ diagonalHalting n)) ↔
131     ¬ ∃ n, diagonalHalting n ∧ primeAt (2*n+1) = primeAt i
132   simp only [primeAt_injective.eq_iff]
133   constructor
134   · rintro ⟨n, hi | ⟨hi, hn⟩⟩ ⟨m, hm, hmi⟩
135     · omega
136     · have : m = n := by omega
137       exact hn (this ▸ hm)
138   · intro h
139     by_cases hi : i % 2 = 0
140     · exact ⟨i/2, Or.inl (by omega)⟩
141     · have he : i = 2*(i/2)+1 := by omega
142       refine ⟨i/2, Or.inr ⟨he, ?_⟩⟩
143       intro hk
144       exact h ⟨i/2, hk, he.symm⟩
145 
146 /-- Keep precisely the selected coordinates of an actual finitely supported vector. -/
147 def spectrumProjection (B : Set Prime) : finiteSupport →+ spectrumSubgroup B where
148   toFun x := by
149     classical
150     let y : Ambient := fun p => if p ∈ B then x.val p else 0
151     have hy : y ∈ finiteSupport := x.property.subset (by
152       intro p hp
153       by_contra hx
154       exact hp (by simp [y, show x.val p = 0 from not_not.mp hx]))
155     refine ⟨⟨y, hy⟩, ?_⟩
156     intro p hp
157     by_contra hn
158     exact hp (by simp [y, hn])
159   map_zero' := by
160     classical
161     apply Subtype.ext
162     apply Subtype.ext
163     funext p
164     simp
165   map_add' x y := by
166     classical
167     apply Subtype.ext
168     apply Subtype.ext
169     funext p
170     by_cases hp : p ∈ B <;> simp [hp]
171 
172 @[simp] theorem spectrumProjection_apply_mem (B : Set Prime) (x : finiteSupport)
173     (p : Prime) (hp : p ∈ B) : (spectrumProjection B x).val.val p = x.val p := by
174   classical
175   simp [spectrumProjection, hp]
176 
177 @[simp] theorem spectrumProjection_apply_not_mem (B : Set Prime) (x : finiteSupport)
178     (p : Prime) (hp : p ∉ B) : (spectrumProjection B x).val.val p = 0 := by
179   classical
180   simp [spectrumProjection, hp]
181 
182 theorem spectrumProjection_surjective (B : Set Prime) :
183     Function.Surjective (spectrumProjection B) := by
184   intro x
185   refine ⟨x.val, ?_⟩
186   apply Subtype.ext
187   apply Subtype.ext
188   funext p
189   by_cases hp : p ∈ B
190   · exact spectrumProjection_apply_mem B x.val p hp
191   · rw [spectrumProjection_apply_not_mem B x.val p hp]
192     symm
193     by_contra hn
194     exact hp (x.property hn)
195 
196 theorem spectrumProjection_ker (B : Set Prime) :
197     (spectrumProjection B).ker = spectrumSubgroup Bᶜ := by
198   classical
199   ext x
200   constructor
201   · intro hx p hp
202     by_contra hn
203     have hb : p ∈ B := not_not.mp hn
204     have he := congrArg (fun z : spectrumSubgroup B => z.val.val p) hx
205     rw [spectrumProjection_apply_mem B x p hb] at he
206     exact hp he
207   · intro hx
208     apply Subtype.ext
209     apply Subtype.ext
210     funext p
211     by_cases hp : p ∈ B
212     · rw [spectrumProjection_apply_mem B x p hp]
213       by_contra hn
214       exact hx hn hp
215     · exact spectrumProjection_apply_not_mem B x p hp
216 
217 /-- The quotient by the omitted actual coordinates is exactly the retained support group. -/
218 def spectrumQuotientEquiv (B : Set Prime) :
219     (finiteSupport ⧸ spectrumSubgroup Bᶜ) ≃+ spectrumSubgroup B :=
220   (QuotientAddGroup.quotientAddEquivOfEq (spectrumProjection_ker B).symm).trans
221     (QuotientAddGroup.quotientKerEquivOfSurjective (spectrumProjection B)
222       (spectrumProjection_surjective B))
223 
224 /-- Actual support subgroups are generated by precisely their retained prime seeds. -/
225 theorem spectrumSubgroup_eq_seedClosure (B : Set Prime) :
226     spectrumSubgroup B = AddSubgroup.closure (primeSeed '' B) := by
227   classical
228   apply le_antisymm
229   · intro x hx
230     rw [finiteSupport_primeSeed_decomposition x]
231     apply AddSubgroup.sum_mem
232     intro p hp
233     apply AddSubgroup.nsmul_mem
234     apply AddSubgroup.subset_closure
235     exact ⟨p, hx (by simpa using hp), rfl⟩
236   · apply (AddSubgroup.closure_le _).mpr
237     rintro _ ⟨p, hp, rfl⟩
238     exact (primeSeed_mem_spectrumSubgroup B p).mpr hp
239 
240 /-- The extra relators are the literal odd prime generators whose programs halt. -/
241 def haltingSeedRelators : Set finiteSupport :=
242   {x | ∃ n, diagonalHalting n ∧ primeSeed (primeAt (2*n+1)) = x}
243 
244 theorem haltingSeedRelators_eq :
245     haltingSeedRelators = primeSeed '' killedHaltingPrimes := by
246   ext x
247   constructor
248   · rintro ⟨n, hn, rfl⟩
249     exact ⟨primeAt (2*n+1), ⟨n, hn, rfl⟩, rfl⟩
250   · rintro ⟨p, ⟨n, hn, rfl⟩, rfl⟩
251     exact ⟨n, hn, rfl⟩
252 
253 /-- Quotienting the actual direct sum by the actual extra relators gives H. -/
254 def haltingRelatorQuotientEquiv :
255     (finiteSupport ⧸ AddSubgroup.closure haltingSeedRelators) ≃+
256       spectrumSubgroup haltingPrimeSpectrum := by
257   have he : AddSubgroup.closure haltingSeedRelators =
258       spectrumSubgroup haltingPrimeSpectrumᶜ := by
259     rw [haltingSeedRelators_eq, ← spectrumSubgroup_eq_seedClosure,
260       haltingPrimeSpectrum_complement, compl_compl]
261   exact (QuotientAddGroup.quotientAddEquivOfEq he).trans
262     (spectrumQuotientEquiv haltingPrimeSpectrum)
263 
264 /-- A genuine finite-stage program for the extra relator indices. Each natural
265 stage decodes a program index and fuel, returning its odd generator exactly
266 when the bounded universal evaluator has observed termination. -/
267 def haltingRelatorIndexStage (k : ℕ) : Option ℕ :=
268   if ((Denumerable.ofNat Nat.Partrec.Code k.unpair.1).evaln k.unpair.2
269       k.unpair.1).isSome then some (2*k.unpair.1+1) else none
270 
271 theorem primrec_haltingRelatorIndexStage : Primrec haltingRelatorIndexStage := by
272   have hl : Primrec (fun k : ℕ => k.unpair.1) := Primrec.fst.comp Primrec.unpair
273   have hr : Primrec (fun k : ℕ => k.unpair.2) := Primrec.snd.comp Primrec.unpair
274   have he : Primrec (fun k : ℕ => (Denumerable.ofNat Nat.Partrec.Code k.unpair.1).evaln
275       k.unpair.2 k.unpair.1) :=
276     Nat.Partrec.Code.primrec_evaln.comp ((hr.pair ((Primrec.ofNat _).comp hl)).pair hl)
277   have hn : Primrec (fun k : ℕ => 2*k.unpair.1+1) :=
278     Primrec.nat_add.comp (Primrec.nat_mul.comp (Primrec.const 2) hl) (Primrec.const 1)
279   exact Primrec.ite (Primrec.eq.comp (Primrec.option_isSome.comp he) (Primrec.const true))
280     (Primrec.option_some.comp hn) (Primrec.const none)
281 
282 theorem haltingRelatorIndexStage_correct (i : ℕ) :
283     (∃ k, haltingRelatorIndexStage k = some i) ↔
284       ∃ n, diagonalHalting n ∧ 2*n+1 = i := by
285   constructor
286   · rintro ⟨k, hk⟩
287     unfold haltingRelatorIndexStage at hk
288     split_ifs at hk with h
289     · have hn : 2*k.unpair.1+1 = i := Option.some.inj hk
290       refine ⟨k.unpair.1, ?_, hn⟩
291       obtain ⟨v, hv⟩ := Option.isSome_iff_exists.mp h
292       exact (Nat.Partrec.Code.evaln_sound hv).1
293   · rintro ⟨n, hn, rfl⟩
294     obtain ⟨v, hv⟩ := Part.dom_iff_mem.mp hn
295     obtain ⟨t, ht⟩ := Nat.Partrec.Code.evaln_complete.mp hv
296     refine ⟨Nat.pair n t, ?_⟩
297     simp [haltingRelatorIndexStage, Option.isSome_iff_exists.mpr ⟨v, ht⟩]
298 
299 /-- The computably emitted labels denote exactly the actual extra relators,
300 so enumeration and the quotient identification refer to the same objects. -/
301 theorem haltingRelatorIndexStage_exact :
302     haltingSeedRelators =
303       (fun i => primeSeed (primeAt i)) '' {i | ∃ k, haltingRelatorIndexStage k = some i} := by
304   ext x
305   constructor
306   · rintro ⟨n, hn, rfl⟩
307     exact ⟨2*n+1, (haltingRelatorIndexStage_correct _).mpr ⟨n, hn, rfl⟩, rfl⟩
308   · rintro ⟨i, hi, rfl⟩
309     obtain ⟨n, hn, rfl⟩ := (haltingRelatorIndexStage_correct i).mp hi
310     exact ⟨n, hn, rfl⟩
311 
312 /-- A genuine computable copy on a finite initial segment. This branch is
313 necessary because finite groups cannot have bijective names on all of Nat. -/
314 structure FiniteGroupCopy (H : Type*) [AddGroup H] where
315   size : ℕ
316   names : Fin size ≃ H
317   zero : Fin size
318   add : Fin size → Fin size → Fin size
319   zero_spec : names zero = 0
320   add_spec : ∀ i j, names (add i j) = names i + names j
321   add_computable : Computable (fun k : Fin size × Fin size => add k.1 k.2)
322 
323 /-- All entries of each fixed finite operation table are ordinary computable.
324 This is existence of a finite copy, not a uniform stopping rule for an enumeration. -/
325 def finiteGroupCopy (H : Type*) [AddGroup H] [Finite H] : FiniteGroupCopy H := by
326   classical
327   letI := Fintype.ofFinite H
328   let e : Fin (Fintype.card H) ≃ H := (Fintype.equivFin H).symm
329   refine ⟨Fintype.card H, e, e.symm 0, fun i j => e.symm (e i + e j), ?_, ?_, ?_⟩
330   · exact e.apply_symm_apply 0
331   · intro i j
332     exact e.apply_symm_apply _
333   · exact (Primrec.dom_finite _).to_comp
334 
335 /-- The finite-or-infinite convention for genuinely computable countable copies. -/
336 def HasOracleGroupCopy (X : ℕ → Bool) (H : Type*) [AddGroup H] : Prop :=
337   Nonempty (FiniteGroupCopy H) ∨ Nonempty (OracleGroupCopy X H)
338 
339 theorem hasOracleGroupCopy_of_finite (X : ℕ → Bool) (H : Type*) [AddGroup H] [Finite H] :
340     HasOracleGroupCopy X H := Or.inl ⟨finiteGroupCopy H⟩
341 
342 /-- A finite-domain copy cannot witness an infinite group. -/
343 theorem finiteGroupCopy_false_of_infinite (H : Type*) [AddGroup H] [Infinite H] :
344     IsEmpty (FiniteGroupCopy H) := by
345   constructor
346   intro c
347   let : Finite H := Finite.of_equiv (Fin c.size) c.names
348   exact not_finite H
349 
350 /-- The halting spectrum obstruction also rules out the broad finite-or-infinite
351 copy convention; the infinitely many retained even factors exclude its finite branch. -/
352 theorem haltingSpectrum_no_any_computable_copy :
353     ¬ HasOracleGroupCopy (fun _ => false) (spectrumSubgroup haltingPrimeSpectrum) := by
354   intro h
355   rcases h with hf | hi
356   · exact hf.elim (finiteGroupCopy_false_of_infinite _).false
357   · exact hi.elim haltingSpectrum_no_computable_copy.false
358 
359 /-- Every fixed finite set has an ordinary primitive-recursive membership test. -/
360 theorem finite_set_primrec_membership (A : Set ℕ) (hA : A.Finite) :
361     PrimrecPred (fun n => n ∈ A) := by
362   classical
363   let L := hA.toFinset.toList
364   have hm : PrimrecPred (fun n : ℕ => ∃ a ∈ L, a = n) :=
365     (Primrec.eq.exists_mem_list).comp (Primrec.const L) Primrec.id
366   exact hm.of_eq (fun n => by simp [L])
367 
368 /-- Finite spectra are enumerable relative to every oracle, without a uniform
369 procedure for finding the final stage of a finite enumeration. -/
370 theorem oracleEnumerable_of_finite (X : ℕ → Bool) (A : Set ℕ) (hA : A.Finite) :
371     OracleEnumerable X A := by
372   classical
373   let test : ℕ → ℕ := fun k => if k.unpair.1 ∈ A then 0 else 1
374   have ht : OracleComputable X test := OracleComputable.of_computable
375     ((Primrec.ite ((finite_set_primrec_membership A hA).comp
376         (Primrec.fst.comp Primrec.unpair)) (Primrec.const 0) (Primrec.const 1)).to_comp)
377   obtain ⟨f, hf, hdom⟩ := oracleEnumerable_of_test X test ht
378   exact ⟨f, hf, fun n => (hdom n).trans (by simp [test])⟩
379 
380 /-- A finite group has only finitely many intrinsic prime-torsion indices. -/
381 theorem finite_group_primeSpectrum_indices (H : Type*) [AddGroup H] [Finite H] :
382     {n | HasPrimeTorsion H (primeAt n)}.Finite := by
383   have hinj : Function.Injective (fun n : ℕ => (primeAt n).val) :=
384     Subtype.val_injective.comp primeAt_injective
385   apply ((Set.finite_Iic (Nat.card H)).preimage hinj.injOn).subset
386   rintro n ⟨x, hx, hpx⟩
387   have ho : addOrderOf x = (primeAt n).val := addOrderOf_eq_prime hpx hx
388   have hd := addOrderOf_dvd_natCard x
389   rw [ho] at hd
390   exact Nat.le_of_dvd Nat.card_pos hd
391 
392 /-- The lower prime-spectrum criterion includes both finite and infinite coded
393 domains, so no finite case is silently excluded by the Nat-domain convention. -/
394 theorem oracle_any_spectrum_copy_implies_enumerable (X : ℕ → Bool) (B : Set Prime)
395     (h : HasOracleGroupCopy X (spectrumSubgroup B)) :
396     OracleEnumerable X {n | primeAt n ∈ B} := by
397   rcases h with hf | hi
398   · obtain ⟨c⟩ := hf
399     let : Finite (spectrumSubgroup B) := Finite.of_equiv (Fin c.size) c.names
400     have hA : {n | primeAt n ∈ B}.Finite := by
401       simpa only [spectrumSubgroup_hasPrimeTorsion_iff] using
402         finite_group_primeSpectrum_indices (spectrumSubgroup B)
403     exact oracleEnumerable_of_finite X _ hA
404   · obtain ⟨c⟩ := hi
405     exact oracle_spectrum_copy_implies_enumerable X B c
406 
407 end RealizationBoundaries

Back to source controls