scheduleByMinIndex
A canonical countable schedule for events is obtained by assigning each event to the smallest index consistent with precedence constraints. Researchers formalizing atomic serialization of finite recognition histories cite this when establishing one-event-per-tick enumerations. The construction uses classical choice on the existence predicate for each index and verifies no-duplicates together with completeness via injectivity of the minimal-index map.
claimLet $E$ be an event type equipped with a precedence relation. Let $m(e)$ denote the minimal natural-number index assigned to event $e$. Define the schedule function by $s(n) = e$ whenever $m(e) = n$ for some $e$, and $s(n)$ undefined otherwise. Then $s$ posts at most one event per tick, posts every event exactly once, and never repeats an event.
background
The Atomicity module supplies constructive serialization for finite recognition histories. It works abstractly over an event type $E$ with a precedence relation that encodes ledger and causal constraints. The central auxiliary notions are the minimal-index function, which returns the smallest tick consistent with precedence for each event, and its specification lemma, which asserts that this index is attained. The module deliberately avoids cost or convexity assumptions and relies only on finiteness together with decidable precedence. Upstream results include the shifted cost $H(x) = J(x) + 1$ and the fundamental tick unit equal to 1, although neither enters the present construction.
proof idea
The definition sets the posting function to return the classically chosen event whose minimal index equals the given tick when such an event exists, otherwise none. The no-duplicates clause proceeds by classical case analysis on the existence predicates, extracts the chosen events via their specification lemmas, and concludes equality of indices from injectivity of the minimal-index map. The completeness clause directly exhibits the minimal index of an arbitrary event and applies the specification lemma to witness that the event appears there.
why it matters in Recognition Science
This definition supplies the concrete schedule object required by the atomic_tick_countable theorem, which asserts existence of a countable atomic schedule that posts exactly one event per tick and visits every event without repetition. It realizes the constructive serialization result stated in the Atomicity module, thereby tightening the T2 forcing step with an axiom-free topological ordering for finite histories. In the larger framework the construction supports the eight-tick octave and the atomic tick as the fundamental time quantum while remaining independent of the phi-ladder and the recognition composition law.
scope and limits
- Does not extend to infinite event collections.
- Does not incorporate conservation predicates or cost preservation.
- Does not invoke the J-cost functional or the recognition composition law.
- Does not assume any specific numerical value for phi or the fine-structure constant.
- Does not address continuous time or non-discrete tick structures.
Lean usage
refine ⟨scheduleByMinIndex (ev := ev), ?_, ?_⟩formal statement (Lean)
385noncomputable def scheduleByMinIndex : CountableSchedule E.Event :=
proof body
Definition body.
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. -/