minIndex_min
plain-language theorem explainer
The lemma establishes that the minimal index of an event in a fixed surjective enumeration from naturals is at most any index where the event occurs. Researchers constructing deterministic topological schedules for finite causal histories cite it when proving that pick-minimal recursion yields a valid linear extension. The proof is a one-line wrapper that unfolds the Nat.find definition of the minimal index and applies the standard minimality property of Nat.find to the surjectivity witness.
Claim. Let $E$ be a countable event type equipped with a surjective enumeration $f:ℕ→E$. For any event $e$ and natural number $n$ such that $f(n)=e$, the minimal index $m(e)$ defined by $m(e)=ℕ.find(λk.f(k)=e)$ satisfies $m(e)≤n$.
background
The Atomicity module supplies a constructive serialization of finite recognition histories that respects a decidable precedence relation prec, tightening T2 without invoking cost or convexity. It works over an abstract event type E that is merely assumed countable, producing a one-per-tick schedule via deterministic minimal-index selection. The key supporting definitions are the surjective enumeration enum obtained by classical choice from Countable.exists_surjective_nat and the minimal index minIndex(e) defined as Nat.find applied to the predicate λn.enum n = e. Upstream, the canonical arithmetic object supplies the underlying Peano structure, while the PrimitiveDistinction theorem reduces the setup to four structural conditions plus definitional facts.
proof idea
The tactic proof opens with classical, unfolds the definition of minIndex, and finishes with an exact application of Nat.find_min' to the surjectivity lemma enum_surjective together with the hypothesis that enum n equals the target event.
why it matters
This lemma is the basic minimality fact needed to guarantee that the pick-minimal recursion in Atomicity produces a well-defined sequential schedule for any finite history. It directly supports the existence of a canonical countable schedule in which each event appears exactly once at its earliest admissible tick, feeding the preservation lemma for conservation predicates under sequential posting. Within the Recognition framework it closes the constructive half of T2 atomicity before the module hands off to later results on eight-tick periodicity and D=3 emergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.