minIndex_spec
plain-language theorem explainer
The specification for the minimal enumeration index shows that applying the surjective enumeration to this index recovers the original event exactly. Workers on constructive serialization of finite recognition histories cite it to validate deterministic ordering via minimal indices. The term proof unfolds the Nat.find definition of minIndex and applies the specification property of the surjectivity lemma.
Claim. For every event $e$, $enum(minIndex(e)) = e$, where $minIndex(e)$ is the least natural number $n$ such that $enum(n) = e$ and $enum$ is any surjective enumeration of the event type.
background
The Atomicity module tightens T2 by supplying an axiom-free serialization result for finite recognition histories. It works abstractly over an event type equipped with a precedence relation that encodes causal constraints, assuming only finiteness and decidable precedence. The enumeration $enum$ is the surjective map from naturals to events obtained by classical choice from countability. The function $minIndex$ selects the smallest index at which this map hits a given event, using $Nat.find$ on the surjectivity predicate. This construction relies on the upstream lemma establishing surjectivity of $enum$ and on the event structure imported from SpectralEmergence.
proof idea
The proof is a one-line term wrapper. It opens classical reasoning, unfolds the definition of $minIndex$ to expose the $Nat.find$ call on the surjectivity predicate for the target event, and applies $Nat.find_spec$ directly to the surjectivity lemma instantiated at that event.
why it matters
This lemma supports the downstream definition of $scheduleByMinIndex$, which builds a canonical countable schedule by placing each event at its minimal index. It completes the atomicity component of the forcing chain by ensuring the pick-minimal topological ordering is faithful to the enumeration. Within Recognition Science it contributes to the constructive one-per-tick schedule for finite histories while remaining independent of cost or convexity assumptions from T5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.