scheduleByMinIndex
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.