IndisputableMonolith.Foundation.Atomicity
IndisputableMonolith/Foundation/Atomicity.lean · 444 lines · 26 declarations
show as:
view math explainer →
1import Mathlib
2
3/-!
4 Atomicity.lean
5
6 Purpose: Tighten T2 by providing a constructive, axiom‑free serialization
7 result for finite recognition histories. We work abstractly over an event
8 type `E` with a precedence relation `prec` encoding ledger/causal constraints.
9
10 Key outcomes:
11 - Existence of a one‑per‑tick (sequential) schedule for any finite history
12 that respects `prec` (topological ordering via a deterministic pick‑minimal
13 recursion).
14 - A generic preservation lemma: if a conservation predicate is preserved by
15 single postings, then it is preserved by any sequential schedule over a
16 finite history.
17
18 Notes:
19 - We deliberately keep this module independent of cost/convexity (T5) and
20 only assume finiteness and decidable precedence on the finite history.
21 - Proofs are constructive over `Finset`; we avoid adding axioms.
22-/
23
24namespace IndisputableMonolith
25namespace Foundation
26
27noncomputable section
28
29open scoped BigOperators
30open Finset
31
32/-- A precedence relation on events. Read `prec e₁ e₂` as “e₁ must occur before e₂”. -/
33abbrev Precedence (E : Type _) := E → E → Prop
34
35namespace Atomicity
36
37variable {E : Type _}
38
39/-- `isMinimalIn prec H e` means `e` is in `H` and has no predecessors in `H`. -/
40def isMinimalIn (prec : Precedence E) [DecidableEq E] [DecidableRel prec]
41 (H : Finset E) (e : E) : Prop :=
42 e ∈ H ∧ ∀ e' ∈ H, ¬ prec e' e
43
44lemma isMinimalIn.mem {prec : Precedence E} [DecidableEq E] [DecidableRel prec]
45 {H : Finset E} {e : E} :
46 isMinimalIn (E:=E) prec H e → e ∈ H :=
47 And.left
48
49/-- Minimality existence on a finite, nonempty `H` under well‑founded precedence. -/
50lemma exists_minimal_in
51 (prec : Precedence E) [DecidableRel prec] [DecidableEq E]
52 (wf : WellFounded prec) {H : Finset E} (hH : H.Nonempty) :
53 ∃ e ∈ H, ∀ e' ∈ H, ¬ prec e' e := by
54 classical
55 refine hH.elim ?_
56 intro a ha
57 have : ∀ x : E, x ∈ H → ∃ m ∈ H, ∀ y ∈ H, ¬ prec y m := by
58 intro x hx
59 -- Well-founded recursion down the precedence relation until a minimal element is reached.
60 refine wf.induction x (C := fun x => x ∈ H → ∃ m ∈ H, ∀ y ∈ H, ¬ prec y m) ?_ hx
61 intro x ih hx
62 by_cases hmin : ∀ y ∈ H, ¬ prec y x
63 · exact ⟨x, hx, hmin⟩
64 · have hnot : ¬ (∀ y ∈ H, ¬ prec y x) := hmin
65 push_neg at hnot
66 obtain ⟨y, hyH, hy⟩ := hnot
67 have hyx : prec y x := not_not.mp hy
68 exact ih y hyx hyH
69 exact this a ha
70
71/-- Topological ordering on finite histories by iteratively removing minimal elements. -/
72def topoSort
73 (prec : Precedence E) [DecidableRel prec] [DecidableEq E]
74 (wf : WellFounded prec) :
75 ∀ H : Finset E, List E
76 | H =>
77 if h : H.Nonempty then
78 let ⟨e, heH, hmin⟩ := exists_minimal_in (E:=E) prec wf h
79 e :: topoSort prec wf (H.erase e)
80 else []
81 termination_by H => H.card
82 decreasing_by
83 classical
84 simp_wf
85 have : (H.erase _) .card < H.card := by
86 simpa [Nat.lt_iff_add_one_le, Nat.succ_le_succ_iff] using
87 Finset.card_erase_lt_of_mem heH
88 simpa using this
89
90/-- `topoSort` covers exactly the elements of `H` with no duplicates. -/
91lemma topoSort_perm
92 (prec : Precedence E) [DecidableRel prec] [DecidableEq E]
93 (wf : WellFounded prec) (H : Finset E) :
94 (topoSort (E:=E) prec wf H).Pairwise (· ≠ ·) ∧
95 (topoSort (E:=E) prec wf H).toFinset = H := by
96 classical
97 have hAux : ∀ n, ∀ H : Finset E, H.card = n →
98 (topoSort (E:=E) prec wf H).Pairwise (· ≠ ·) ∧
99 (topoSort (E:=E) prec wf H).toFinset = H := by
100 refine Nat.rec ?base ?step
101 · intro H hcard
102 have hH : H = (∅ : Finset E) :=
103 Finset.card_eq_zero.mp (by simpa [hcard] : H.card = 0)
104 have hTop : topoSort (E:=E) prec wf H = [] := by
105 simp [topoSort, hH]
106 simpa [hTop, hH]
107 · intro n ih H hcard
108 have hnpos : 0 < H.card := by
109 simpa [hcard] using Nat.succ_pos n
110 have hn : H.Nonempty := Finset.card_pos.mp hnpos
111 obtain ⟨e, heH, hmin⟩ := exists_minimal_in (E:=E) prec wf hn
112 have hcard' : (H.erase e).card = n := by
113 have : (H.erase e).card + 1 = H.card := Finset.card_erase_add_one heH
114 have : (H.erase e).card + 1 = n + 1 := by simpa [hcard] using this
115 exact Nat.succ.inj this
116 have htail := ih (H.erase e) hcard'
117 set tail := topoSort (E:=E) prec wf (H.erase e)
118 have hTop : topoSort (E:=E) prec wf H = e :: tail := by
119 simp [topoSort, hn, heH, hmin]
120 have hxneq : ∀ x ∈ tail, x ≠ e := by
121 intro x hx
122 have hxErase : x ∈ H.erase e := by
123 have : x ∈ tail.toFinset := by
124 simpa using List.mem_toFinset.mpr hx
125 simpa [tail, htail.2] using this
126 exact (Finset.mem_erase.mp hxErase).1
127 have hxneq' : ∀ x ∈ tail, e ≠ x := by
128 intro x hx
129 have hxne := hxneq x hx
130 exact fun h => hxne h.symm
131 have pairTail : tail.Pairwise (· ≠ ·) := by
132 simpa [tail] using htail.1
133 refine And.intro ?pair ?cover
134 · exact List.Pairwise.cons.2 ⟨hxneq', pairTail⟩
135 · simp [hTop, tail, htail.2, Finset.insert_erase, heH]
136 exact hAux H.card H rfl
137
138/-- Respect of precedence: earlier elements in `topoSort` have no incoming edges from later ones. -/
139lemma topoSort_respects
140 (prec : Precedence E) [DecidableRel prec] [DecidableEq E]
141 (wf : WellFounded prec) (H : Finset E) :
142 ∀ {e₁ e₂}, e₁ ∈ H → e₂ ∈ H → prec e₁ e₂ →
143 (topoSort (E:=E) prec wf H).indexOf e₁ <
144 (topoSort (E:=E) prec wf H).indexOf e₂ := by
145 classical
146 have hAux : ∀ n, ∀ H : Finset E, H.card = n →
147 ∀ {e₁ e₂}, e₁ ∈ H → e₂ ∈ H → prec e₁ e₂ →
148 (topoSort (E:=E) prec wf H).indexOf e₁ <
149 (topoSort (E:=E) prec wf H).indexOf e₂ :=
150 by
151 refine Nat.rec ?base ?step
152 · intro H hcard e₁ e₂ h₁ _ _
153 have hEmpty : H = (∅ : Finset E) :=
154 Finset.card_eq_zero.mp (by simpa [hcard] : H.card = 0)
155 simpa [hEmpty] using h₁
156 · intro n ih H hcard e₁ e₂ h₁ h₂ h12
157 have hnpos : 0 < H.card := by
158 simpa [hcard] using Nat.succ_pos n
159 have hn : H.Nonempty := Finset.card_pos.mp hnpos
160 obtain ⟨e, heH, hmin⟩ := exists_minimal_in (E:=E) prec wf hn
161 have hcard' : (H.erase e).card = n := by
162 have : (H.erase e).card + 1 = H.card := Finset.card_erase_add_one heH
163 have : (H.erase e).card + 1 = n + 1 := by simpa [hcard] using this
164 exact Nat.succ.inj this
165 set tail := topoSort (E:=E) prec wf (H.erase e)
166 have hTop : topoSort (E:=E) prec wf H = e :: tail := by
167 simp [topoSort, hn, heH, hmin]
168 have h2ne : e₂ ≠ e := by
169 intro h
170 have : prec e₁ e := by simpa [h] using h12
171 exact (hmin e₁ h₁) this
172 by_cases h1e : e₁ = e
173 · subst h1e
174 have hIndex₁ : (topoSort (E:=E) prec wf H).indexOf e = 0 := by
175 simp [hTop, List.indexOf_cons]
176 have hIndex₂ :
177 (topoSort (E:=E) prec wf H).indexOf e₂ =
178 (topoSort (E:=E) prec wf (H.erase e)).indexOf e₂ + 1 := by
179 simp [hTop, List.indexOf_cons, h2ne]
180 have hPos :
181 0 < (topoSort (E:=E) prec wf (H.erase e)).indexOf e₂ + 1 :=
182 Nat.succ_pos _
183 simpa [hIndex₁, hIndex₂] using hPos
184 · have h1ne : e₁ ≠ e := h1e
185 have h₁mem : e₁ ∈ H.erase e := by
186 simpa [Finset.mem_erase, h1ne, h₁]
187 have h₂mem : e₂ ∈ H.erase e := by
188 simpa [Finset.mem_erase, h2ne, h₂]
189 have hIH := ih (H.erase e) hcard' h₁mem h₂mem h12
190 have hIndex₁ :
191 (topoSort (E:=E) prec wf H).indexOf e₁ =
192 (topoSort (E:=E) prec wf (H.erase e)).indexOf e₁ + 1 := by
193 simp [hTop, List.indexOf_cons, h1ne]
194 have hIndex₂ :
195 (topoSort (E:=E) prec wf H).indexOf e₂ =
196 (topoSort (E:=E) prec wf (H.erase e)).indexOf e₂ + 1 := by
197 simp [hTop, List.indexOf_cons, h2ne]
198 simpa [hIndex₁, hIndex₂] using Nat.succ_lt_succ hIH
199 exact hAux H.card H rfl
200
201/-- A sequential, one‑per‑tick schedule for a finite history `H`. -/
202structure Schedule (E : Type _) where
203 order : List E
204 nodup : order.Pairwise (· ≠ ·)
205
206namespace Schedule
207
208variable [DecidableEq E]
209
210/-- Event at a given tick (index into the order), if any. -/
211def postAtTick (σ : Schedule E) (n : ℕ) : Option E :=
212 (σ.order.get? n)
213
214end Schedule
215
216/-- Existence of a one‑per‑tick schedule (finite history version). -/
217theorem exists_sequential_schedule
218 (prec : Precedence E) [DecidableRel prec] [DecidableEq E]
219 (wf : WellFounded prec) (H : Finset E) :
220 ∃ σ : Schedule E,
221 σ.order.Pairwise (· ≠ ·) ∧
222 σ.order.toFinset = H ∧
223 (∀ {e₁ e₂}, e₁ ∈ H → e₂ ∈ H → prec e₁ e₂ →
224 σ.order.indexOf e₁ < σ.order.indexOf e₂) := by
225 classical
226 refine ⟨⟨topoSort (E:=E) prec wf H, ?_⟩, ?_, ?_, ?_⟩
227 · exact (topoSort_perm (E:=E) prec wf H).1
228 · exact (topoSort_perm (E:=E) prec wf H).2
229 · intro e₁ e₂ h₁ h₂ h12; exact topoSort_respects (E:=E) prec wf H h₁ h₂ h12
230
231/-- Generic preservation: if conservation holds initially and is preserved
232 by single postings, then conservation holds along any sequential schedule
233 for a finite history. -/
234theorem sequential_preserves_conservation
235 {S : Type _} (Conservation : S → Prop) (post : S → E → S)
236 (prec : Precedence E)
237 [DecidableRel prec] [DecidableEq E]
238 (H : Finset E) (σ : Schedule E)
239 (hcover : σ.order.toFinset = H)
240 (s0 : S)
241 (h0 : Conservation s0)
242 (preserve_single : ∀ s e, e ∈ H → Conservation s → Conservation (post s e)) :
243 Conservation (σ.order.foldl post s0) := by
244 classical
245 revert s0 h0
246 refine σ.order.rec ?base ?step
247 · intro s h; simpa using h
248 · intro e tail ih s h
249 have heH : e ∈ H := by
250 have : e ∈ (e :: tail).toFinset := by
251 simpa using List.mem_toFinset.mpr (by simp)
252 simpa [hcover] using this
253 have h' : Conservation (post s e) := preserve_single s e heH h
254 simpa using ih (post s e) h'
255
256/-- Atomic tick (finite history): any finite recognition history admits a
257 serialization with exactly one posting per tick that respects precedence. -/
258theorem atomic_tick
259 (prec : Precedence E) [DecidableRel prec] [DecidableEq E]
260 (wf : WellFounded prec) (H : Finset E) :
261 ∃ σ : Schedule E,
262 σ.order.toFinset = H ∧
263 ∀ {e₁ e₂}, e₁ ∈ H → e₂ ∈ H → prec e₁ e₂ →
264 σ.order.indexOf e₁ < σ.order.indexOf e₂ := by
265 classical
266 obtain ⟨σ, _nodup, hcover, hrespect⟩ :=
267 exists_sequential_schedule (E:=E) prec wf H
268 exact ⟨σ, hcover, hrespect⟩
269
270/-- ## Countable serialization --/
271
272section Countable
273
274variable {E : DiscreteEventSystem}
275variable (ev : EventEvolution E)
276variable [DecidableEq E.Event]
277
278open LedgerNecessity
279
280local notation:max "Prec" => Precedence ev
281
282noncomputable def enum : ℕ → E.Event :=
283 Classical.choose (Countable.exists_surjective_nat (E.countable))
284
285lemma enum_surjective : Function.Surjective (enum (E:=E)) :=
286 Classical.choose_spec (Countable.exists_surjective_nat (E.countable))
287
288/-- An event is eligible once all predecessors have been posted. -/
289def eligible (picked : Finset E.Event) (e : E.Event) : Prop :=
290 ∀ {v}, Prec v e → v ∈ picked
291
292lemma eligible_mono {picked₁ picked₂ : Finset E.Event}
293 (hsubset : picked₁ ⊆ picked₂) {e : E.Event}
294 (helig : eligible (ev:=ev) picked₁ e) :
295 eligible (ev:=ev) picked₂ e := by
296 intro v hv
297 exact hsubset (helig hv)
298
299lemma exists_minimal_eligible (picked : Finset E.Event)
300 (h : ∃ e, e ∉ picked) :
301 ∃ e, e ∉ picked ∧ eligible (ev:=ev) picked e := by
302 classical
303 have wf := ledger_prec_wf (ev:=ev)
304 let S : Set E.Event := {x | x ∉ picked}
305 have hS : S.Nonempty := by
306 rcases h with ⟨e, he⟩
307 exact ⟨e, he⟩
308 obtain ⟨m, hmS, hmin⟩ := wf.has_min S hS
309 refine ⟨m, hmS, ?_⟩
310 intro v hv
311 by_contra hvPicked
312 have hvS : v ∈ S := hvPicked
313 exact (hmin v hvS hv)
314
315structure Candidate (picked : Finset E.Event) where
316 idx : ℕ
317 event : E.Event
318 event_def : enum (E:=E) idx = event
319 not_mem : event ∉ picked
320 eligible_event : eligible (ev:=ev) picked event
321
322lemma exists_candidate_index (picked : Finset E.Event)
323 (h : ∃ e, e ∉ picked) :
324 ∃ n, enum (E:=E) n ∉ picked ∧ eligible (ev:=ev) picked (enum (E:=E) n) := by
325 classical
326 obtain ⟨e, heNot, helig⟩ := exists_minimal_eligible (ev:=ev) (E:=E) picked h
327 obtain ⟨n, hn⟩ := enum_surjective (E:=E) e
328 refine ⟨n, ?_, ?_⟩
329 · simpa [hn]
330 · simpa [hn] using helig
331
332noncomputable def chooseCandidate (picked : Finset E.Event) :
333 Option (Candidate (ev:=ev) (E:=E) picked) :=
334 if h : ∃ e, e ∉ picked then
335 let hx := exists_candidate_index (ev:=ev) (E:=E) picked h
336 let n := Nat.find hx
337 let hn := Nat.find_spec hx
338 let e := enum (E:=E) n
339 some
340 { idx := n
341 , event := e
342 , event_def := rfl
343 , not_mem := hn.left
344 , eligible_event := hn.right }
345 else
346 none
347
348lemma chooseCandidate_none_iff (picked : Finset E.Event) :
349 chooseCandidate (ev:=ev) (E:=E) picked = none ↔
350 ¬∃ e, e ∉ picked := by
351 classical
352 unfold chooseCandidate
353 split_ifs with h
354 · simp [h]
355 · simp [h]
356
357lemma chooseCandidate_some_spec {picked : Finset E.Event}
358 {c : Candidate (ev:=ev) (E:=E) picked}
359 (h : chooseCandidate (ev:=ev) (E:=E) picked = some c) :
360 c.not_mem ∧ eligible (ev:=ev) picked c.event := by
361 classical
362 unfold chooseCandidate at h
363 split_ifs at h with hExists
364 · rcases h with ⟨⟩
365 simp
366 · cases h
367
368/-- Minimal index (in the fixed enumeration `enum`) where an event appears. -/
369noncomputable def minIndex (e : E.Event) : ℕ :=
370 Nat.find (enum_surjective (E:=E) e)
371
372lemma minIndex_spec (e : E.Event) : enum (E:=E) (minIndex (E:=E) e) = e := by
373 classical
374 unfold minIndex
375 exact Nat.find_spec (enum_surjective (E:=E) e)
376
377lemma minIndex_min (e : E.Event) {n : ℕ} (h : enum (E:=E) n = e) :
378 minIndex (E:=E) e ≤ n := by
379 classical
380 unfold minIndex
381 exact Nat.find_min' (enum_surjective (E:=E) e) h
382
383/-- A canonical countable schedule derived from `minIndex`. Each event appears
384 exactly once at its minimal enumeration index. -/
385noncomputable def scheduleByMinIndex : CountableSchedule E.Event :=
386{ postAt := fun n =>
387 if h : ∃ e : E.Event, minIndex (E:=E) e = n then
388 some (Classical.choose h)
389 else none
390, nodup := by
391 intro n₁ n₂ e h₁ h₂
392 classical
393 unfold scheduleByMinIndex at h₁ h₂
394 simp only at h₁ h₂
395 rcases Classical.decEq (∃ e, minIndex (E:=E) e = n₁) with hdec₁ | hdec₁
396 · simp [scheduleByMinIndex._match_1, hdec₁] at h₁
397 · rcases h₁
398 rcases Classical.decEq (∃ e, minIndex (E:=E) e = n₂) with hdec₂ | hdec₂
399 · simp [scheduleByMinIndex._match_1, hdec₂] at h₂
400 · rcases h₂
401 -- In the `some` branches on both sides
402 have hsome₁ : ∃ e, minIndex (E:=E) e = n₁ := by
403 by_contra H; simp [scheduleByMinIndex._match_1, H] at h₁
404 have hsome₂ : ∃ e, minIndex (E:=E) e = n₂ := by
405 by_contra H; simp [scheduleByMinIndex._match_1, H] at h₂
406 let e₁ := Classical.choose hsome₁
407 let e₂ := Classical.choose hsome₂
408 have he₁ : minIndex (E:=E) e₁ = n₁ := (Classical.choose_spec hsome₁)
409 have he₂ : minIndex (E:=E) e₂ = n₂ := (Classical.choose_spec hsome₂)
410 -- The `some` payloads must coincide with `e`
411 have : e₁ = e := by
412 have : some e₁ = some e := by simpa [scheduleByMinIndex._match_1, he₁] using h₁
413 exact by cases this; rfl
414 have : e₂ = e := by
415 have : some e₂ = some e := by simpa [scheduleByMinIndex._match_1, he₂] using h₂
416 exact by cases this; rfl
417 -- Conclude equality of indices by injectivity of `minIndex`
418 simpa [this, he₁, he₂]
419, complete := by
420 intro e
421 classical
422 refine ⟨minIndex (E:=E) e, ?_⟩
423 simp [scheduleByMinIndex, scheduleByMinIndex._match_1, minIndex_spec (E:=E) e]
424 -- exhibits the chosen `e` at its minimal index
425}
426
427/-- Countable atomic schedule (enumerative). Posts exactly one event per tick,
428 visits every event, with no duplicates. -/
429theorem atomic_tick_countable :
430 ∃ σ : CountableSchedule E.Event,
431 (∀ e, ∃ n, σ.postAt n = some e) ∧
432 (∀ {n₁ n₂ e}, σ.postAt n₁ = some e → σ.postAt n₂ = some e → n₁ = n₂) := by
433 classical
434 refine ⟨scheduleByMinIndex (ev:=ev), ?_, ?_⟩
435 · intro e; exact (scheduleByMinIndex (ev:=ev)).complete e
436 · intro n₁ n₂ e h₁ h₂; exact (scheduleByMinIndex (ev:=ev)).nodup h₁ h₂
437
438end Countable
439
440end Atomicity
441
442end Foundation
443end IndisputableMonolith
444