GrammarEscape.lean

1 import RealizationBoundaries.ClassificationConsequences
2 import Mathlib.Data.Nat.Pairing
3 import Mathlib.SetTheory.Cardinal.Continuum
4 
5 /-!
6 # Escape from an arbitrary fixed countable semantic table
7 
8 The semantic table has no effectiveness assumption. Classical representatives
9 are chosen only for outputs isomorphic to an actual paired-prime group. The
10 repeated diagonal defeats eventual equality, and the independent odd blocks
11 retain the full space of free binary selectors.
12 -/
13 set_option autoImplicit false
14 set_option backward.isDefEq.respectTransparency false
15 noncomputable section
16 namespace RealizationBoundaries
17 attribute [local instance] Classical.propDecidable
18 
19 /-- Even positions defeat a semantic output; odd positions repeat a free bit. -/
20 def repeatedDiagonal (B : ℕ → ℕ → Bool) (C : ℕ → Bool) (n : ℕ) : Bool :=
21   if n % 2 = 0 then !(B (Nat.unpair (n / 2)).1 n)
22   else C (Nat.unpair (n / 2)).1
23 
24 @[simp] theorem repeatedDiagonal_even (B : ℕ → ℕ → Bool) (C : ℕ → Bool)
25     (j k : ℕ) : repeatedDiagonal B C (2 * Nat.pair j k) =
26       !(B j (2 * Nat.pair j k)) := by
27   simp [repeatedDiagonal]
28 
29 @[simp] theorem repeatedDiagonal_odd (B : ℕ → ℕ → Bool) (C : ℕ → Bool)
30     (j k : ℕ) : repeatedDiagonal B C (2 * Nat.pair j k + 1) = C j := by
31   have hdiv : (2 * Nat.pair j k + 1) / 2 = Nat.pair j k := by omega
32   have hmod : (2 * Nat.pair j k + 1) % 2 = 1 := by omega
33   simp [repeatedDiagonal, hdiv, hmod]
34 
35 /-- Each semantic output is opposed at infinitely many distinct even indices. -/
36 theorem repeatedDiagonal_infinite_disagreement (B : ℕ → ℕ → Bool)
37     (C : ℕ → Bool) (j : ℕ) :
38     {n : ℕ | repeatedDiagonal B C n ≠ B j n}.Infinite := by
39   have hi : Function.Injective (fun k => 2 * Nat.pair j k) := by
40     intro k l h
41     change 2 * Nat.pair j k = 2 * Nat.pair j l at h
42     have hp : Nat.pair j k = Nat.pair j l := by omega
43     exact (Nat.pair_eq_pair.mp hp).2
44   apply (Set.infinite_range_of_injective hi).mono
45   rintro n ⟨k, rfl⟩
46   simp only [Set.mem_ofPred_eq, repeatedDiagonal_even]
47   cases B j (2 * Nat.pair j k) <;> decide
48 
49 /-- Different free selectors remain different modulo every finite set. -/
50 theorem repeatedDiagonal_free_infinite_disagreement (B : ℕ → ℕ → Bool)
51     (C D : ℕ → Bool) (hCD : C ≠ D) :
52     {n : ℕ | repeatedDiagonal B C n ≠ repeatedDiagonal B D n}.Infinite := by
53   obtain ⟨j, hj⟩ : ∃ j, C j ≠ D j := by
54     by_contra h
55     apply hCD
56     funext j
57     by_contra hj
58     exact h ⟨j, hj⟩
59   have hi : Function.Injective (fun k => 2 * Nat.pair j k + 1) := by
60     intro k l h
61     change 2 * Nat.pair j k + 1 = 2 * Nat.pair j l + 1 at h
62     have hp : Nat.pair j k = Nat.pair j l := by omega
63     exact (Nat.pair_eq_pair.mp hp).2
64   apply (Set.infinite_range_of_injective hi).mono
65   rintro n ⟨k, rfl⟩
66   simpa only [Set.mem_ofPred_eq, repeatedDiagonal_odd] using hj
67 
68 universe u
69 
70 /-- A family representative is selected only when the semantic output belongs
71 up to isomorphism to the actual paired-prime family. -/
72 def semanticRepresentative {Code : Type*} (R : Code → Type u)
73     [∀ j, AddGroup (R j)] (j : Code) : ℕ → Bool :=
74   if h : ∃ a : ℕ → Bool, Nonempty (R j ≃+ pairedGroup a)
75   then h.choose else fun _ => false
76 
77 theorem semanticRepresentative_spec {Code : Type*} (R : Code → Type u)
78     [∀ j, AddGroup (R j)] (j : Code) (h : ∃ a : ℕ → Bool, Nonempty (R j ≃+ pairedGroup a)) :
79     Nonempty (R j ≃+ pairedGroup (semanticRepresentative R j)) := by
80   unfold semanticRepresentative
81   rw [dite_eq_left h]
82   exact h.choose_spec
83 
84 /-- Selector escaping the fixed table, with an unrestricted free binary input. -/
85 def grammarEscapeSelector (R : ℕ → Type u) [∀ j, AddGroup (R j)]
86     (C : ℕ → Bool) : ℕ → Bool := repeatedDiagonal (semanticRepresentative R) C
87 
88 /-- No semantic output is isomorphic to the escaped group. This includes outputs
89 outside the paired family; no membership test or evaluator is assumed. -/
90 theorem grammarEscape_not_output (R : ℕ → Type u) [∀ j, AddGroup (R j)]
91     (C : ℕ → Bool) (j : ℕ) :
92     ¬ Nonempty (pairedGroup (grammarEscapeSelector R C) ≃+ R j) := by
93   rintro ⟨e⟩
94   have hex : ∃ a : ℕ → Bool, Nonempty (R j ≃+ pairedGroup a) :=
95     ⟨grammarEscapeSelector R C, ⟨e.symm⟩⟩
96   obtain ⟨er⟩ := semanticRepresentative_spec R j hex
97   have hf := finite_disagreement_of_pairedEquiv _ _ (e.trans er)
98   exact repeatedDiagonal_infinite_disagreement (semanticRepresentative R) C j hf
99 
100 /-- The entire continuum of free binary inputs gives distinct group isomorphism types. -/
101 theorem grammarEscape_pairwise_nonisomorphic (R : ℕ → Type u) [∀ j, AddGroup (R j)]
102     (C D : ℕ → Bool) (hCD : C ≠ D) :
103     ¬ Nonempty (pairedGroup (grammarEscapeSelector R C) ≃+
104       pairedGroup (grammarEscapeSelector R D)) := by
105   rw [pairedGroup_isomorphic_iff]
106   exact repeatedDiagonal_free_infinite_disagreement (semanticRepresentative R) C D hCD
107 
108 /-- Stronger separation: there is no embedding in either direction. -/
109 theorem grammarEscape_no_embedding (R : ℕ → Type u) [∀ j, AddGroup (R j)]
110     (C D : ℕ → Bool) (hCD : C ≠ D)
111     (f : pairedGroup (grammarEscapeSelector R C) →+
112       pairedGroup (grammarEscapeSelector R D)) : ¬ Function.Injective f :=
113   no_injective_hom_of_infinite_disagreement _ _
114     (repeatedDiagonal_free_infinite_disagreement (semanticRepresentative R) C D hCD) f
115 
116 /-- Distinct free selectors yield distinct actual ambient subgroups. -/
117 theorem grammarEscape_groups_injective (R : ℕ → Type u) [∀ j, AddGroup (R j)] :
118     Function.Injective (fun C : ℕ → Bool => pairedGroup (grammarEscapeSelector R C)) := by
119   intro C D h
120   by_contra hCD
121   exact grammarEscape_pairwise_nonisomorphic R C D hCD
122     ⟨AddEquiv.addSubgroupCongr h⟩
123 
124 /-- An exact cardinal statement, paired with the stronger isomorphism separation
125 above: the actual escaped family has continuum many members. -/
126 theorem grammarEscape_family_cardinality (R : ℕ → Type u) [∀ j, AddGroup (R j)] :
127     Cardinal.mk (Set.range (fun C : ℕ → Bool => pairedGroup (grammarEscapeSelector R C))) =
128       Cardinal.continuum := by
129   rw [Cardinal.mk_range_eq _ (grammarEscape_groups_injective R), Cardinal.mk_arrow]
130   simp only [Cardinal.mk_bool, Cardinal.mk_nat, Cardinal.lift_ofNat, Cardinal.lift_aleph0]
131   exact Cardinal.two_power_aleph0
132 
133 /-- Every escaped group has the original common profinite completion. -/
134 def grammarEscape_completion (R : ℕ → Type u) [∀ j, AddGroup (R j)]
135     (C : ℕ → Bool) :
136     ProfiniteAddGrp.ProfiniteCompletion.completion
137       (AddGrpCat.of (pairedGroup (grammarEscapeSelector R C))) ≃ₜ+ Ambient :=
138   pairedCompletionEquiv _
139 
140 theorem grammarEscape_countably_infinite (R : ℕ → Type u) [∀ j, AddGroup (R j)]
141     (C : ℕ → Bool) : Countable (pairedGroup (grammarEscapeSelector R C)) ∧
142       Infinite (pairedGroup (grammarEscapeSelector R C)) := paired_countably_infinite _
143 
144 theorem grammarEscape_residuallyFinite (R : ℕ → Type u) [∀ j, AddGroup (R j)]
145     (C : ℕ → Bool) : AddGroup.ResiduallyFinite (pairedGroup (grammarEscapeSelector R C)) :=
146   preimage_residuallyFinite _
147 
148 /-- Reducedness is expressed by exclusion of every nonzero divisible subgroup,
149 not only exclusion of a rational summand. -/
150 theorem grammarEscape_reduced (R : ℕ → Type u) [∀ j, AddGroup (R j)]
151     (C : ℕ → Bool) (E : Type*) [AddGroup E] [Nontrivial E]
152     (hdiv : ∀ m : ℕ, 0 < m → ∀ x : E, ∃ y : E, m • y = x)
153     (f : E →+ pairedGroup (grammarEscapeSelector R C)) : ¬ Function.Injective f := by
154   intro hf
155   exact not_injective_hom_of_divisible E hdiv
156     ((pairedGroup (grammarEscapeSelector R C)).subtype.comp f)
157     (Subtype.val_injective.comp hf)
158 
159 /-- Extend representatives from an arbitrary countable code domain along an
160 injection into the natural-number table. Unused indices receive a dummy selector. -/
161 def reindexedSemanticRepresentative {Code : Type*} (R : Code → Type u)
162     [∀ c, AddGroup (R c)] (index : Code → ℕ) (j : ℕ) : ℕ → Bool :=
163   if h : ∃ c, index c = j then semanticRepresentative R h.choose else fun _ => false
164 
165 theorem reindexedSemanticRepresentative_at {Code : Type*} (R : Code → Type u)
166     [∀ c, AddGroup (R c)] (index : Code → ℕ) (hi : Function.Injective index)
167     (c : Code) : reindexedSemanticRepresentative R index (index c) =
168       semanticRepresentative R c := by
169   have h : ∃ d, index d = index c := ⟨c, rfl⟩
170   unfold reindexedSemanticRepresentative
171   rw [dite_eq_left h, hi h.choose_spec]
172 
173 /-- Countability alone supplies the code injection. There is no computability
174 assumption on syntax validity, the index, evaluation or family membership. -/
175 def countableDescriptionIndex (Code : Type*) [Countable Code] : Code → ℕ :=
176   (Countable.exists_injective_nat Code).choose
177 
178 theorem countableDescriptionIndex_injective (Code : Type*) [Countable Code] :
179     Function.Injective (countableDescriptionIndex Code) :=
180   (Countable.exists_injective_nat Code).choose_spec
181 
182 def countableGrammarEscapeSelector {Code : Type*} [Countable Code]
183     (R : Code → Type u) [∀ c, AddGroup (R c)] (C : ℕ → Bool) : ℕ → Bool :=
184   repeatedDiagonal (reindexedSemanticRepresentative R (countableDescriptionIndex Code)) C
185 
186 theorem countableGrammarEscape_not_output {Code : Type*} [Countable Code]
187     (R : Code → Type u) [∀ c, AddGroup (R c)] (C : ℕ → Bool) (c : Code) :
188     ¬ Nonempty (pairedGroup (countableGrammarEscapeSelector R C) ≃+ R c) := by
189   rintro ⟨e⟩
190   have hex : ∃ a : ℕ → Bool, Nonempty (R c ≃+ pairedGroup a) :=
191     ⟨countableGrammarEscapeSelector R C, ⟨e.symm⟩⟩
192   obtain ⟨er⟩ := semanticRepresentative_spec R c hex
193   have hf := finite_disagreement_of_pairedEquiv _ _ (e.trans er)
194   have hi := repeatedDiagonal_infinite_disagreement
195     (reindexedSemanticRepresentative R (countableDescriptionIndex Code)) C
196     (countableDescriptionIndex Code c)
197   rw [reindexedSemanticRepresentative_at R (countableDescriptionIndex Code)
198     (countableDescriptionIndex_injective Code) c] at hi
199   exact hi hf
200 
201 theorem countableGrammarEscape_free_infinite_disagreement {Code : Type*} [Countable Code]
202     (R : Code → Type u) [∀ c, AddGroup (R c)] (C D : ℕ → Bool) (hCD : C ≠ D) :
203     {n : ℕ | countableGrammarEscapeSelector R C n ≠
204       countableGrammarEscapeSelector R D n}.Infinite :=
205   repeatedDiagonal_free_infinite_disagreement _ C D hCD
206 
207 theorem countableGrammarEscape_pairwise_nonisomorphic {Code : Type*} [Countable Code]
208     (R : Code → Type u) [∀ c, AddGroup (R c)] (C D : ℕ → Bool) (hCD : C ≠ D) :
209     ¬ Nonempty (pairedGroup (countableGrammarEscapeSelector R C) ≃+
210       pairedGroup (countableGrammarEscapeSelector R D)) := by
211   rw [pairedGroup_isomorphic_iff]
212   exact countableGrammarEscape_free_infinite_disagreement R C D hCD
213 
214 theorem countableGrammarEscape_no_embedding {Code : Type*} [Countable Code]
215     (R : Code → Type u) [∀ c, AddGroup (R c)] (C D : ℕ → Bool) (hCD : C ≠ D)
216     (f : pairedGroup (countableGrammarEscapeSelector R C) →+
217       pairedGroup (countableGrammarEscapeSelector R D)) : ¬ Function.Injective f :=
218   no_injective_hom_of_infinite_disagreement _ _
219     (countableGrammarEscape_free_infinite_disagreement R C D hCD) f
220 
221 theorem countableGrammarEscape_family_cardinality {Code : Type*} [Countable Code]
222     (R : Code → Type u) [∀ c, AddGroup (R c)] :
223     Cardinal.mk (Set.range (fun C : ℕ → Bool =>
224       pairedGroup (countableGrammarEscapeSelector R C))) = Cardinal.continuum := by
225   have hi : Function.Injective (fun C : ℕ → Bool =>
226       pairedGroup (countableGrammarEscapeSelector R C)) := by
227     intro C D h
228     by_contra hCD
229     exact countableGrammarEscape_pairwise_nonisomorphic R C D hCD
230       ⟨AddEquiv.addSubgroupCongr h⟩
231   rw [Cardinal.mk_range_eq _ hi, Cardinal.mk_arrow]
232   simp only [Cardinal.mk_bool, Cardinal.mk_nat, Cardinal.lift_ofNat, Cardinal.lift_aleph0]
233   exact Cardinal.two_power_aleph0
234 
235 /-- The exact semantic/length interface for admissible grammar expansion.
236 Validity and group isomorphism semantics can both be included in `denotes`. -/
237 structure DescriptionGrammar (Code : Type*) (Object : Type*) where
238   denotes : Code → Object → Prop
239   length : Code → ℕ
240 
241 namespace DescriptionGrammar
242 variable {Code Object : Type*}
243 
244 def Realizes (G : DescriptionGrammar Code Object) (x : Object) : Prop :=
245   ∃ d, G.denotes d x
246 
247 private theorem exists_length (G : DescriptionGrammar Code Object) (x : Object)
248     (h : G.Realizes x) : ∃ n, ∃ d, G.denotes d x ∧ G.length d = n := by
249   obtain ⟨d, hd⟩ := h
250   exact ⟨G.length d, d, hd, rfl⟩
251 
252 /-- Exact shortest length, used only when a description exists. -/
253 def shortestLength (G : DescriptionGrammar Code Object) (x : Object)
254     (h : G.Realizes x) : ℕ := Nat.find (exists_length G x h)
255 
256 theorem shortestLength_spec (G : DescriptionGrammar Code Object) (x : Object)
257     (h : G.Realizes x) : ∃ d, G.denotes d x ∧ G.length d = G.shortestLength x h :=
258   Nat.find_spec (exists_length G x h)
259 
260 theorem shortestLength_le (G : DescriptionGrammar Code Object) (x : Object)
261     (h : G.Realizes x) (d : Code) (hd : G.denotes d x) :
262     G.shortestLength x h ≤ G.length d :=
263   Nat.find_min' (exists_length G x h) ⟨d, hd, rfl⟩
264 
265 /-- Description complexity is infinite exactly when no valid description exists. -/
266 def complexity (G : DescriptionGrammar Code Object) (x : Object) : WithTop ℕ :=
267   if h : G.Realizes x then (G.shortestLength x h : WithTop ℕ) else ⊤
268 
269 theorem complexity_eq_top_iff (G : DescriptionGrammar Code Object) (x : Object) :
270     G.complexity x = ⊤ ↔ ¬ G.Realizes x := by
271   by_cases h : G.Realizes x <;> simp [complexity, h]
272 
273 variable {OtherCode : Type*}
274 
275 /-- Monograph 10.2: semantic translation preserves realizability. -/
276 theorem admissible_expansion (G : DescriptionGrammar Code Object)
277     (H : DescriptionGrammar OtherCode Object) (translate : Code → OtherCode)
278     (preserves : ∀ d x, G.denotes d x → H.denotes (translate d) x)
279     (x : Object) : G.Realizes x → H.Realizes x := by
280   rintro ⟨d, hd⟩
281   exact ⟨translate d, preserves d x hd⟩
282 
283 /-- Translate a shortest valid description; no monotonicity of the overhead
284 function is required because this is the actual shortest source witness. -/
285 theorem admissible_expansion_length (G : DescriptionGrammar Code Object)
286     (H : DescriptionGrammar OtherCode Object) (translate : Code → OtherCode)
287     (preserves : ∀ d x, G.denotes d x → H.denotes (translate d) x)
288     (f : ℕ → ℕ)
289     (length_bound : ∀ d x, G.denotes d x → H.length (translate d) ≤ f (G.length d))
290     (x : Object) (h : G.Realizes x) :
291     H.shortestLength x (admissible_expansion G H translate preserves x h) ≤
292       f (G.shortestLength x h) := by
293   obtain ⟨d, hd, hlen⟩ := G.shortestLength_spec x h
294   exact (H.shortestLength_le x _ (translate d) (preserves d x hd)).trans
295     ((length_bound d x hd).trans_eq (congrArg f hlen))
296 
297 /-- The finite source-complexity version of the printed complexity inequality. -/
298 theorem admissible_expansion_complexity (G : DescriptionGrammar Code Object)
299     (H : DescriptionGrammar OtherCode Object) (translate : Code → OtherCode)
300     (preserves : ∀ d x, G.denotes d x → H.denotes (translate d) x)
301     (f : ℕ → ℕ)
302     (length_bound : ∀ d x, G.denotes d x → H.length (translate d) ≤ f (G.length d))
303     (x : Object) (h : G.Realizes x) :
304     H.complexity x ≤ (f (G.shortestLength x h) : WithTop ℕ) := by
305   have hH := admissible_expansion G H translate preserves x h
306   rw [complexity, dite_eq_left hH]
307   exact_mod_cast admissible_expansion_length G H translate preserves f length_bound x h
308 
309 end DescriptionGrammar
310 
311 /-- The fixed countable table interpreted as a genuine isomorphism semantics.
312 The length function is arbitrary; invalid descriptions can be assigned a dummy output. -/
313 def semanticDescriptionGrammar (R : ℕ → Type u) [∀ j, AddGroup (R j)]
314     (length : ℕ → ℕ) : DescriptionGrammar ℕ (AddSubgroup Ambient) where
315   denotes j H := Nonempty (H ≃+ R j)
316   length := length
317 
318 /-- Every escaped group has infinite description complexity in the fixed grammar. -/
319 theorem grammarEscape_complexity_infinite (R : ℕ → Type u) [∀ j, AddGroup (R j)]
320     (length : ℕ → ℕ) (C : ℕ → Bool) :
321     (semanticDescriptionGrammar R length).complexity
322       (pairedGroup (grammarEscapeSelector R C)) = ⊤ := by
323   rw [DescriptionGrammar.complexity_eq_top_iff]
324   rintro ⟨j, hj⟩
325   exact grammarEscape_not_output R C j hj
326 
327 end RealizationBoundaries

Back to source controls