exists_candidate_index
plain-language theorem explainer
Given a finite set of posted events with at least one event remaining, there exists a natural-number index n into the enumeration such that the nth event lies outside the posted set and every predecessor of that event has already been posted. Atomicity arguments in the Recognition Science foundation cite this to guarantee a deterministic next candidate for sequential schedules. The argument first extracts a minimal eligible event via well-foundedness of precedence and recovers its index under the surjective enumeration.
Claim. Let $P$ be a finite subset of events from a countable event type equipped with a precedence relation. If $E$ minus $P$ is nonempty, then there exists $n$ in the naturals such that the $n$th enumerated event is not in $P$ and every predecessor of that event lies in $P$.
background
The Atomicity module tightens T2 by supplying constructive, axiom-free serialization for finite recognition histories. It works over an abstract event type with a precedence relation that encodes ledger and causal constraints. An event is eligible once all predecessors have been posted: formally, for picked finite set and event e, every v with Prec v e satisfies v in picked. The enumeration is the noncomputable surjective map from naturals onto the event type obtained from countability. This lemma depends on the existence of a minimal eligible event, which itself rests on the well-foundedness of the precedence relation.
proof idea
The term-mode proof invokes classical logic to obtain a minimal eligible event outside the picked set. It then applies the surjectivity of the enumeration to recover a natural-number index for that event. The two conjuncts of the goal are discharged by simplification after substitution of the recovered index.
why it matters
This lemma supplies the index used by chooseCandidate to select the next event in a sequential schedule. It contributes directly to the existence of a one-per-tick schedule that respects precedence for any finite history, a key outcome of the Atomicity module. The module keeps the result independent of cost or convexity to isolate the serialization step in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.