ComputableFiniteObservations.lean

1 import RealizationBoundaries.ObservationSystems
2 import RealizationBoundaries.PrimeComputability
3 import Mathlib.Data.ZMod.QuotientRing
4 import Mathlib.Data.Nat.Squarefree
5 import Mathlib.CategoryTheory.Whiskering
6 
7 /-!
8 # A fixed computable cofinal finite-observation system
9 
10 All algorithms below depend only on natural stage and residue codes. No
11 selector, dense source, named source element, or oracle is an algorithm input.
12 -/
13 set_option autoImplicit false
14 set_option backward.isDefEq.respectTransparency false
15 noncomputable section
16 open CategoryTheory
17 open scoped BigOperators
18 namespace RealizationBoundaries
19 
20 /-- The first `n` actual prime coordinates. -/
21 def observationPrimes (n : ℕ) : Finset Prime := (Finset.range n).image primeAt
22 
23 theorem observationPrimes_mono {m n : ℕ} (h : m ≤ n) :
24     observationPrimes m ⊆ observationPrimes n :=
25   Finset.image_subset_image (Finset.range_mono h)
26 
27 theorem primeAt_not_mem_observationPrimes (n : ℕ) : primeAt n ∉ observationPrimes n := by
28   rintro h
29   obtain ⟨i, hi, he⟩ := Finset.mem_image.mp h
30   have hin := primeAt_injective he
31   exact (Nat.ne_of_lt (Finset.mem_range.mp hi)) hin
32 
33 @[simp] theorem observationPrimes_zero : observationPrimes 0 = ∅ := by
34   simp [observationPrimes]
35 
36 @[simp] theorem observationPrimes_succ (n : ℕ) :
37     observationPrimes (n+1) = insert (primeAt n) (observationPrimes n) := by
38   simp only [observationPrimes, Finset.range_add_one, Finset.image_insert]
39 
40 /-- The fixed finite cyclic group at stage `n` has this squarefree order. -/
41 def observationModulus (n : ℕ) : ℕ := ∏ p ∈ observationPrimes n, p.val
42 
43 @[simp] theorem observationModulus_zero : observationModulus 0 = 1 := by
44   simp [observationModulus]
45 
46 @[simp] theorem observationModulus_succ (n : ℕ) :
47     observationModulus (n+1) = observationModulus n * (primeAt n).val := by
48   classical
49   rw [observationModulus, observationPrimes_succ,
50     Finset.prod_insert (primeAt_not_mem_observationPrimes n)]
51   exact Nat.mul_comm _ _
52 
53 theorem observationModulus_pos (n : ℕ) : 0 < observationModulus n :=
54   Finset.prod_pos (fun p _ => p.property.pos)
55 
56 instance observationModulus_neZero (n : ℕ) : NeZero (observationModulus n) :=
57   ⟨(observationModulus_pos n).ne'⟩
58 
59 theorem observationModulus_dvd {m n : ℕ} (h : m ≤ n) :
60     observationModulus m ∣ observationModulus n :=
61   Finset.prod_dvd_prod_of_subset _ _ _ (observationPrimes_mono h)
62 
63 theorem observationModulus_squarefree (n : ℕ) : Squarefree (observationModulus n) := by
64   apply Finset.squarefree_prod_of_pairwise_isCoprime
65   · intro p _ q _ hpq
66     change IsRelPrime p.val q.val
67     rw [← Nat.coprime_iff_isRelPrime]
68     exact (Nat.coprime_primes p.property q.property).mpr
69       (fun h => hpq (Subtype.ext h))
70   · intro p _
71     exact p.property.squarefree
72 
73 /-- Prime values are proved computable independently. Primitive recursion then
74 computes the full stage size, rather than assuming a prime-product oracle. -/
75 theorem computable_observationModulus : Computable observationModulus := by
76   have hstep : Computable₂ (fun (_ : ℕ) (p : ℕ × ℕ) => p.2 * (primeAt p.1).val) :=
77     Primrec.nat_mul.to_comp.comp (Computable.snd.comp Computable.snd)
78       (computable_primeAt_value.comp (Computable.fst.comp Computable.snd))
79   refine (Computable.nat_rec Computable.id (Computable.const 1) hstep).of_eq ?_
80   intro n
81   induction n with
82   | zero => exact observationModulus_zero.symm
83   | succ n ih =>
84     change (Nat.rec 1 (fun i r => r * (primeAt i).val) n) * (primeAt n).val = _
85     change Nat.rec 1 (fun i r => r * (primeAt i).val) n = observationModulus n at ih
86     rw [ih, observationModulus_succ]
87 
88 /-- An executable terminating prime search, identified with the actual
89 mathematical enumeration. Its existence proof is erased at runtime. -/
90 def observationPrimeProgram (n : ℕ) : ℕ := Nat.find (primeIndexRelation_total n)
91 
92 theorem observationPrimeProgram_eq (n : ℕ) : observationPrimeProgram n = (primeAt n).val := by
93   have ht := Nat.find_spec (primeIndexRelation_total n)
94   have he := Nat.nth_count ht.1
95   rw [ht.2] at he
96   exact he.symm
97 
98 /-- Executable stage-size computation, with no classical finite-set operation
99 in its runtime path. -/
100 def observationModulusProgram (n : ℕ) : ℕ :=
101   Nat.rec 1 (fun i r => r * observationPrimeProgram i) n
102 
103 theorem observationModulusProgram_eq (n : ℕ) :
104     observationModulusProgram n = observationModulus n := by
105   induction n with
106   | zero => exact observationModulus_zero.symm
107   | succ n ih =>
108     change observationModulusProgram n * observationPrimeProgram n = _
109     rw [ih, observationPrimeProgram_eq, observationModulus_succ]
110 
111 /-- Every actual finite prime set is contained in a prefix. -/
112 theorem observationPrimes_cofinal (s : Finset Prime) :
113     ∃ n, s ⊆ observationPrimes n := by
114   classical
115   induction s using Finset.induction_on with
116   | empty => exact ⟨0, Finset.empty_subset _⟩
117   | @insert p s hp ih =>
118     obtain ⟨n, hn⟩ := ih
119     let i := Nat.count Nat.Prime p.val
120     have hi : primeAt i = p := Subtype.ext (Nat.nth_count p.property)
121     refine ⟨max n (i+1), ?_⟩
122     intro q hq
123     rcases Finset.mem_insert.mp hq with rfl | hqs
124     · apply observationPrimes_mono (Nat.le_max_right n (i+1))
125       exact Finset.mem_image.mpr ⟨i, Finset.mem_range.mpr (Nat.lt_succ_self i), hi⟩
126     · exact observationPrimes_mono (Nat.le_max_left n (i+1)) (hn hqs)
127 
128 /-- The natural residue codes of a stage form a finite decidable domain. -/
129 def observationValid (n x : ℕ) : Prop := x < observationModulus n
130 
131 instance observationValid_decidable : DecidableRel observationValid := by
132   unfold observationValid
133   infer_instance
134 
135 def observationAddCode (n x y : ℕ) : ℕ := (x+y) % observationModulus n
136 
137 def observationNegCode (n x : ℕ) : ℕ :=
138   (observationModulus n - x % observationModulus n) % observationModulus n
139 
140 def observationRestrictionCode (m x : ℕ) : ℕ := x % observationModulus m
141 
142 /-- Executable companions of every finite table. -/
143 def observationValidProgram (n x : ℕ) : Bool := decide (x < observationModulusProgram n)
144 def observationAddProgram (n x y : ℕ) : ℕ := (x+y) % observationModulusProgram n
145 def observationNegProgram (n x : ℕ) : ℕ :=
146   (observationModulusProgram n - x % observationModulusProgram n) % observationModulusProgram n
147 def observationRestrictionProgram (m x : ℕ) : ℕ := x % observationModulusProgram m
148 
149 theorem observationValidProgram_eq (n x : ℕ) :
150     observationValidProgram n x = decide (observationValid n x) := by
151   simp only [observationValidProgram, observationValid, observationModulusProgram_eq]
152 
153 theorem observationAddProgram_eq (n x y : ℕ) :
154     observationAddProgram n x y = observationAddCode n x y := by
155   simp only [observationAddProgram, observationAddCode, observationModulusProgram_eq]
156 
157 theorem observationNegProgram_eq (n x : ℕ) :
158     observationNegProgram n x = observationNegCode n x := by
159   simp only [observationNegProgram, observationNegCode, observationModulusProgram_eq]
160 
161 theorem observationRestrictionProgram_eq (m x : ℕ) :
162     observationRestrictionProgram m x = observationRestrictionCode m x := by
163   simp only [observationRestrictionProgram, observationRestrictionCode, observationModulusProgram_eq]
164 
165 /-- All validity, group-table and transition-table algorithms are ordinary
166 computable and have no selector or oracle parameter. -/
167 theorem computable_observationIndexRelation : Computable (fun k : ℕ =>
168     decide (k.unpair.2 ≤ k.unpair.1)) :=
169   Primrec.nat_le.decide.to_comp.comp
170     (Computable.snd.comp Computable.unpair) (Computable.fst.comp Computable.unpair)
171 
172 theorem computable_observationEquality : Computable (fun k : ℕ =>
173     decide (k.unpair.1 = k.unpair.2)) :=
174   Primrec.eq.decide.to_comp.comp
175     (Computable.fst.comp Computable.unpair) (Computable.snd.comp Computable.unpair)
176 
177 theorem computable_observationValid : Computable (fun k : ℕ =>
178     decide (observationValid k.unpair.1 k.unpair.2)) := by
179   have hlt : Computable₂ (fun a b : ℕ => decide (a < b)) := Primrec.nat_lt.decide.to_comp
180   exact hlt.comp (Computable.snd.comp Computable.unpair)
181     (computable_observationModulus.comp (Computable.fst.comp Computable.unpair))
182 
183 theorem computable_observationAddCode : Computable (fun k : ℕ =>
184     observationAddCode k.unpair.1 k.unpair.2.unpair.1 k.unpair.2.unpair.2) := by
185   have hl : Computable (fun k : ℕ => k.unpair.1) := Computable.fst.comp Computable.unpair
186   have hr : Computable (fun k : ℕ => k.unpair.2) := Computable.snd.comp Computable.unpair
187   exact Primrec.nat_mod.to_comp.comp
188     (Primrec.nat_add.to_comp.comp (hl.comp hr) (hr.comp hr))
189     (computable_observationModulus.comp hl)
190 
191 theorem computable_observationNegCode : Computable (fun k : ℕ =>
192     observationNegCode k.unpair.1 k.unpair.2) := by
193   have hl : Computable (fun k : ℕ => k.unpair.1) := Computable.fst.comp Computable.unpair
194   have hr : Computable (fun k : ℕ => k.unpair.2) := Computable.snd.comp Computable.unpair
195   have hM := computable_observationModulus.comp hl
196   exact Primrec.nat_mod.to_comp.comp
197     (Primrec.nat_sub.to_comp.comp hM (Primrec.nat_mod.to_comp.comp hr hM)) hM
198 
199 theorem computable_observationRestrictionCode : Computable (fun k : ℕ =>
200     observationRestrictionCode k.unpair.1 k.unpair.2) := by
201   exact Primrec.nat_mod.to_comp.comp (Computable.snd.comp Computable.unpair)
202     (computable_observationModulus.comp (Computable.fst.comp Computable.unpair))
203 
204 theorem observationAddCode_valid (n x y : ℕ) :
205     observationValid n (observationAddCode n x y) := Nat.mod_lt _ (observationModulus_pos n)
206 
207 theorem observationNegCode_valid (n x : ℕ) :
208     observationValid n (observationNegCode n x) := Nat.mod_lt _ (observationModulus_pos n)
209 
210 theorem observationRestrictionCode_valid (m x : ℕ) :
211     observationValid m (observationRestrictionCode m x) := Nat.mod_lt _ (observationModulus_pos m)
212 
213 /-- Finite natural names are bijective with the actual finite cyclic group. -/
214 def observationNames (n : ℕ) : Fin (observationModulus n) ≃ ZMod (observationModulus n) :=
215   Equiv.ofBijective (fun x => (x.val : ZMod (observationModulus n))) (by
216     constructor
217     · intro x y h
218       apply Fin.ext
219       have he := congrArg ZMod.val h
220       simpa only [ZMod.val_natCast, Nat.mod_eq_of_lt x.isLt, Nat.mod_eq_of_lt y.isLt] using he
221     · intro x
222       exact ⟨⟨x.val, x.val_lt⟩, ZMod.natCast_zmod_val x⟩)
223 
224 @[simp] theorem observationNames_apply (n : ℕ) (x : Fin (observationModulus n)) :
225     observationNames n x = (x.val : ZMod (observationModulus n)) := rfl
226 
227 theorem observationZeroCode_valid (n : ℕ) : observationValid n 0 := observationModulus_pos n
228 
229 theorem observationAddCode_spec (n x y : ℕ) :
230     (observationAddCode n x y : ZMod (observationModulus n)) =
231       (x : ZMod (observationModulus n)) + (y : ZMod (observationModulus n)) := by
232   simp only [observationAddCode, ZMod.natCast_mod, Nat.cast_add]
233 
234 theorem observationNegCode_spec (n x : ℕ) :
235     (observationNegCode n x : ZMod (observationModulus n)) =
236       -(x : ZMod (observationModulus n)) := by
237   have hx : x % observationModulus n ≤ observationModulus n :=
238     (Nat.mod_lt _ (observationModulus_pos n)).le
239   rw [observationNegCode, ZMod.natCast_mod, Nat.cast_sub hx,
240     ZMod.natCast_self, ZMod.natCast_mod, zero_sub]
241 
242 def observationRestriction {m n : ℕ} (h : m ≤ n) :
243     ZMod (observationModulus n) →+ ZMod (observationModulus m) :=
244   (ZMod.castHom (observationModulus_dvd h) (ZMod (observationModulus m))).toAddMonoidHom
245 
246 theorem observationRestrictionCode_spec {m n : ℕ} (h : m ≤ n) (x : ℕ) :
247     (observationRestrictionCode m x : ZMod (observationModulus m)) =
248       observationRestriction h (x : ZMod (observationModulus n)) := by
249   simp [observationRestrictionCode, observationRestriction]
250 
251 @[simp] theorem observationRestriction_natCast {m n : ℕ} (h : m ≤ n) (x : ℕ) :
252     observationRestriction h (x : ZMod (observationModulus n)) =
253       (x : ZMod (observationModulus m)) :=
254   map_natCast (ZMod.castHom (observationModulus_dvd h) (ZMod (observationModulus m))) x
255 
256 /-- The computably indexed fixed diagram of actual finite cyclic groups. -/
257 def computableObservation : OrderDual ℕ ⥤ FiniteAddGrp where
258   obj n := FiniteAddGrp.of (ZMod (observationModulus n.ofDual))
259   map f := FiniteAddGrp.ofHom (observationRestriction f.le)
260   map_id n := by
261     ext x
262     change observationRestriction (le_refl n.ofDual) x = x
263     rw [← ZMod.natCast_zmod_val x]
264     rw [observationRestriction_natCast]
265   map_comp f g := by
266     ext x
267     change observationRestriction (le_trans g.le f.le) x =
268       observationRestriction g.le (observationRestriction f.le x)
269     rw [← ZMod.natCast_zmod_val x]
270     rw [observationRestriction_natCast, observationRestriction_natCast,
271       observationRestriction_natCast]
272 
273 /-- Prefix coordinate reindexing of the actual source-free coordinate diagram. -/
274 def observationPrefixFunctor : OrderDual ℕ ⥤ CoordinateIndex :=
275   (show OrderDual ℕ →o CoordinateIndex from
276     ⟨fun n => OrderDual.toDual (observationPrimes n.ofDual),
277       fun _ _ h => observationPrimes_mono h⟩).monotone.functor
278 
279 instance observationPrefixFunctor_initial : observationPrefixFunctor.Initial := by
280   apply (Functor.initial_iff_of_isCofiltered _).mpr
281   constructor
282   · intro s
283     obtain ⟨n, hn⟩ := observationPrimes_cofinal s.ofDual
284     exact ⟨OrderDual.toDual n, ⟨hn.hom⟩⟩
285   · intro s n f g
286     exact ⟨n, 𝟙 n, Subsingleton.elim _ _⟩
287 
288 /-- CRT identifies the actual fixed cyclic stage with exactly the corresponding
289 finite prime-coordinate group, not merely another group of the same cardinality. -/
290 def observationCrtEquiv (n : ℕ) :
291     ZMod (observationModulus n) ≃+* FiniteCoordinates (OrderDual.toDual (observationPrimes n)) := by
292   classical
293   let s := observationPrimes n
294   have hc : Pairwise (fun p q : {p : Prime // p ∈ s} => Nat.Coprime p.val.val q.val.val) := by
295     intro p q hpq
296     exact (Nat.coprime_primes p.val.property q.val.property).mpr
297       (fun h => hpq (Subtype.ext (Subtype.ext h)))
298   exact (ZMod.ringEquivCongr (Finset.prod_coe_sort s (fun p : Prime => p.val)).symm).trans
299     (ZMod.prodEquivPi (fun p : {p : Prime // p ∈ s} => p.val.val) hc)
300 
301 @[simp] theorem observationCrtEquiv_natCast (n x : ℕ)
302     (p : {p : Prime // p ∈ observationPrimes n}) :
303     observationCrtEquiv n (x : ZMod (observationModulus n)) p = (x : Coordinate p.val) := by
304   exact congrArg (fun z : FiniteCoordinates (OrderDual.toDual (observationPrimes n)) => z p)
305     (map_natCast (observationCrtEquiv n) x)
306 
307 /-- The CRT identifications commute with all actual restriction maps. -/
308 theorem observationCrtEquiv_restriction {m n : ℕ} (h : m ≤ n)
309     (x : ZMod (observationModulus n)) :
310     finiteCoordinateRestriction (observationPrimes_mono h) (observationCrtEquiv n x) =
311       observationCrtEquiv m (observationRestriction h x) := by
312   rw [← ZMod.natCast_zmod_val x]
313   funext p
314   change observationCrtEquiv n (x.val : ZMod (observationModulus n))
315       ⟨p.val, observationPrimes_mono h p.property⟩ =
316     observationCrtEquiv m (observationRestriction h (x.val : ZMod (observationModulus n))) p
317   have hr : observationRestriction h (x.val : ZMod (observationModulus n)) =
318       (x.val : ZMod (observationModulus m)) :=
319     map_natCast (ZMod.castHom (observationModulus_dvd h) (ZMod (observationModulus m))) _
320   rw [hr, observationCrtEquiv_natCast, observationCrtEquiv_natCast]
321 
322 /-- A compatible isomorphism of finite-group diagrams ties the native tables to
323 the already checked coordinate-observation inverse system. -/
324 def computableObservationIso : computableObservation ≅ observationPrefixFunctor ⋙ coordinateObservation :=
325   NatIso.ofComponents (fun n => {
326     hom := FiniteAddGrp.ofHom (observationCrtEquiv n.ofDual).toAddMonoidHom
327     inv := FiniteAddGrp.ofHom (observationCrtEquiv n.ofDual).symm.toAddMonoidHom
328     hom_inv_id := by ext x; exact (observationCrtEquiv n.ofDual).symm_apply_apply x
329     inv_hom_id := by ext x; exact (observationCrtEquiv n.ofDual).apply_symm_apply x
330   }) (by
331     intro n m f
332     ext x
333     change observationCrtEquiv m.ofDual (observationRestriction f.le x) =
334       finiteCoordinateRestriction (observationPrimes_mono f.le) (observationCrtEquiv n.ofDual x)
335     exact (observationCrtEquiv_restriction f.le x).symm)
336 
337 /-- For every actual rational preimage, the same native fixed system represents
338 its entire finite-quotient observation after certified cofinal reindexing. -/
339 def computableObservationQuotientIso (W : Submodule ℚ TailSpace) :
340     observationPrefixFunctor ⋙ coordinateIndexFunctor W ⋙
341       ProfiniteAddGrp.ProfiniteCompletion.finiteAddGrpDiagram (AddGrpCat.of (preimage W)) ≅
342         computableObservation :=
343   (Functor.isoWhiskerLeft observationPrefixFunctor (coordinateObservationIso W)).trans
344     computableObservationIso.symm
345 
346 /-- The full finite observation can be presented by this one fixed native
347 computable diagram, with an explicitly certified cofinal comparison. -/
348 def fixedComputableObservation : FiniteObservation where
349   Index := OrderDual ℕ
350   diagram := computableObservation
351 
352 /-- The prefix index maps are cofinal in all actual finite quotients. -/
353 instance computableObservationIndex_initial (W : Submodule ℚ TailSpace) :
354     (observationPrefixFunctor ⋙ coordinateIndexFunctor W).Initial :=
355   Functor.initial_comp observationPrefixFunctor (coordinateIndexFunctor W)
356 
357 theorem allFiniteObservation_fixed_computable (W : Submodule ℚ TailSpace) :
358     CommonCofinalObservation (allFiniteObservation W) fixedComputableObservation := by
359   refine ⟨OrderDual ℕ, inferInstance,
360     observationPrefixFunctor ⋙ coordinateIndexFunctor W, 𝟭 (OrderDual ℕ),
361     inferInstance, computableObservationIndex_initial W, inferInstance, ?_⟩
362   exact ⟨(computableObservationQuotientIso W).trans (Functor.leftUnitor computableObservation).symm⟩
363 
364 end RealizationBoundaries

Back to source controls