exists_minimal_eligible
plain-language theorem explainer
In a finite collection of events under a well-founded precedence relation, if any events remain unpicked then at least one unpicked event has all its predecessors already posted. Atomicity arguments in Recognition Science invoke this to start building a sequential posting order. The proof extracts a minimal unpicked event via the ledger well-ordering and shows eligibility by contradiction on any missing predecessor.
Claim. Let $P$ be a finite set of posted events. If there exists at least one event outside $P$, then there exists an event $e$ outside $P$ such that every predecessor $v$ of $e$ under the precedence relation lies in $P$.
background
The Atomicity module supplies serialization results that tighten the T2 axiom of discrete causal structure in Recognition Science. It works over an abstract event type equipped with a precedence relation encoding ledger and causal constraints, assuming only finiteness and decidable precedence on finite histories. The central auxiliary definition states that an event is eligible with respect to the posted set once every predecessor under the precedence relation has already been posted.
proof idea
The argument begins by invoking classical logic to access the well-founded ledger precedence relation. It forms the nonempty set of unpicked events and applies the has_min property to extract a minimal element m. Eligibility of m follows by supposing a predecessor v is unpicked, placing v in the unpicked set, and invoking minimality to obtain a contradiction.
why it matters
This lemma initiates the inductive construction of sequential schedules over finite histories and is invoked directly by the exists_candidate_index lemma to locate the next event via enumeration. It realizes the constructive serialization step described in the Atomicity module documentation for tightening T2. Within the Recognition framework it supports gap-free causal posting that underpins the eight-tick octave and three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.