minIndex_min
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not assume or use any precedence relation prec on events.
- Does not prove uniqueness of the minimal index beyond the Nat.find property.
- Does not extend to infinite or non-countable event collections.
- Does not incorporate J-cost, defect distance, or phi-ladder structure.
- Does not construct the full schedule, only the index bound.
formal statement (Lean)
377lemma minIndex_min (e : E.Event) {n : ℕ} (h : enum (E:=E) n = e) :
proof body
Tactic-mode proof.
378 minIndex (E:=E) e ≤ n := by
379 classical
380 unfold minIndex
381 exact Nat.find_min' (enum_surjective (E:=E) e) h
382
383/-- A canonical countable schedule derived from `minIndex`. Each event appears
384 exactly once at its minimal enumeration index. -/