DegreeVariation.lean

1 import RealizationBoundaries.ComputableNormalCodes
2 import RealizationBoundaries.ObservationSystems
3 import RealizationBoundaries.OracleCopyOperations
4 import RealizationBoundaries.ComputableFiniteObservations
5 
6 /-! # Least presentation degrees over one observation system
7 
8 The usual degrees of sets are the native Mathlib Turing degrees represented by
9 total binary membership oracles. Mathlib also permits partial-function oracle
10 degrees; no totalization theorem about that broader carrier is assumed here.
11 -/
12 set_option autoImplicit false
13 noncomputable section
14 namespace RealizationBoundaries
15 
16 def selectorTuringDegree (a : ℕ → Bool) : TuringDegree :=
17   toAntisymmetrization TuringReducible (selectorOracle a)
18 
19 theorem selectorTuringDegree_le_iff (a X : ℕ → Bool) :
20     selectorTuringDegree a ≤ selectorTuringDegree X ↔ SelectorReducible a X := Iff.rfl
21 
22 /-- Degrees of sets, using the official native degree carrier and membership oracles. -/
23 def SetTuringDegree := {d : TuringDegree // ∃ a : ℕ → Bool, selectorTuringDegree a = d}
24 
25 def HasLeastPresentationDegree (H : Type*) [AddGroup H] (d : TuringDegree) : Prop :=
26   (∃ a : ℕ → Bool, selectorTuringDegree a = d ∧ Nonempty (OracleGroupCopy a H)) ∧
27     ∀ X : ℕ → Bool, Nonempty (OracleGroupCopy X H) → d ≤ selectorTuringDegree X
28 
29 /-- The degree is attained by an actual copy and bounds every other copy below. -/
30 theorem paired_least_presentation_degree (a : ℕ → Bool) :
31     HasLeastPresentationDegree (pairedGroup a) (selectorTuringDegree a) := by
32   constructor
33   · exact ⟨a, rfl, (paired_oracle_copy_iff a a).mpr (TuringReducible.refl _)⟩
34   · intro X hX
35     exact (selectorTuringDegree_le_iff a X).mpr ((paired_oracle_copy_iff a X).mp hX)
36 
37 /-- Every ordinary degree of a set occurs among the actual countable paired groups,
38 while their complete source-free finite quotient observations remain identical. -/
39 theorem every_set_degree_with_common_observations (d : SetTuringDegree) :
40     ∃ a : ℕ → Bool,
41       selectorTuringDegree a = d.val ∧
42       HasLeastPresentationDegree (pairedGroup a) d.val ∧
43       Countable (pairedGroup a) ∧ Infinite (pairedGroup a) ∧
44       AddGroup.ResiduallyFinite (pairedGroup a) ∧
45       Nonempty (CanonicalCompletion (selectorLine (pairedSelector a)) ≃ₜ+ Ambient) ∧
46       ∀ b : ℕ → Bool, CommonCofinalObservation
47         (allFiniteObservation (selectorLine (pairedSelector a)))
48         (allFiniteObservation (selectorLine (pairedSelector b))) := by
49   obtain ⟨a, ha⟩ := d.property
50   refine ⟨a, ha, ha ▸ paired_least_presentation_degree a,
51     (paired_countably_infinite a).1, (paired_countably_infinite a).2,
52     preimage_residuallyFinite _, ⟨pairedCompletionEquiv a⟩, ?_⟩
53   intro b
54   exact allFiniteObservation_common _ _
55 
56 /-- Reducedness is retained for every degree: no nontrivial divisible group embeds. -/
57 theorem paired_degree_reduced (a : ℕ → Bool) (E : Type*) [AddGroup E] [Nontrivial E]
58     (hdiv : ∀ m : ℕ, 0 < m → ∀ x : E, ∃ y : E, m • y = x)
59     (f : E →+ pairedGroup a) : ¬ Function.Injective f := by
60   intro hf
61   exact not_injective_hom_of_divisible E hdiv ((pairedGroup a).subtype.comp f)
62     (Subtype.val_injective.comp hf)
63 
64 def IsReducedAddGroup (H : Type*) [AddGroup H] : Prop :=
65   ∀ (E : Type) [AddGroup E] [Nontrivial E],
66     (∀ m : ℕ, 0 < m → ∀ x : E, ∃ y : E, m • y = x) →
67       ∀ f : E →+ H, ¬ Function.Injective f
68 
69 theorem paired_isReduced (a : ℕ → Bool) : IsReducedAddGroup (pairedGroup a) := by
70   intro E _ _ hdiv f
71   exact paired_degree_reduced a E hdiv f
72 
73 /-- Monograph 8.4 with the literal fixed, natively computable finite-group diagram. -/
74 theorem every_set_degree_with_fixed_computable_observation (d : SetTuringDegree) :
75     ∃ a : ℕ → Bool,
76       selectorTuringDegree a = d.val ∧
77       HasLeastPresentationDegree (pairedGroup a) d.val ∧
78       Countable (pairedGroup a) ∧ Infinite (pairedGroup a) ∧
79       IsReducedAddGroup (pairedGroup a) ∧
80       AddGroup.ResiduallyFinite (pairedGroup a) ∧
81       Nonempty (CanonicalCompletion (selectorLine (pairedSelector a)) ≃ₜ+ Ambient) ∧
82       CommonCofinalObservation
83         (allFiniteObservation (selectorLine (pairedSelector a))) fixedComputableObservation := by
84   obtain ⟨a, ha, hd, hc, hi, hr, he, _⟩ := every_set_degree_with_common_observations d
85   exact ⟨a, ha, hd, hc, hi, paired_isReduced a, hr, he, allFiniteObservation_fixed_computable _⟩
86 
87 end RealizationBoundaries

Back to source controls