minIndex
plain-language theorem explainer
minIndex selects the smallest natural number at which a given event appears under the fixed enumeration of all events. Researchers constructing deterministic schedules for finite recognition histories cite this definition to anchor topological orderings. The definition is a direct one-line wrapper applying Nat.find to the surjectivity witness of the enumeration map.
Claim. Let $enum : ℕ → ℰ$ be a surjective enumeration of the event set ℰ. For any event $e ∈ ℰ$, $minIndex(e)$ is the least $n ∈ ℕ$ such that $enum(n) = e$.
background
The Atomicity module supplies a constructive, axiom-free serialization of finite recognition histories. It works over an abstract event type E equipped with a precedence relation that encodes ledger and causal constraints. The module produces one-per-tick schedules that respect precedence via deterministic minimal-index selection, while preserving any conservation predicate that holds for single postings.
proof idea
The definition is a one-line wrapper that applies Nat.find directly to the surjectivity lemma enum_surjective (E:=E) e. No further tactics or reductions are used; the minimal index is extracted from the existence proof that every event appears somewhere in the enumeration.
why it matters
minIndex supplies the canonical selector that feeds the lemmas minIndex_min and minIndex_spec, which in turn support the definition of scheduleByMinIndex. That schedule realizes the one-per-tick serialization result for T2. The construction remains independent of cost or convexity assumptions and relies only on countability of events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.