eligible
plain-language theorem explainer
The definition marks an event e as eligible relative to a picked Finset precisely when every predecessor v under the precedence relation satisfies v in picked. Researchers constructing deterministic topological orders for finite event histories cite this predicate to select the next minimal candidate at each tick. The definition is a direct universal quantification over the precedence relation with no additional premises.
Claim. An event $e$ is eligible with respect to a posted set $S$ if, for every predecessor $v$ satisfying the precedence relation, $v$ belongs to $S$.
background
Atomicity supplies a constructive, axiom-free serialization of finite recognition histories. It works abstractly over an event type E equipped with a precedence relation that encodes ledger and causal constraints. The upstream definition E from SpectralEmergence counts the edges of the D-cube, giving |E| = D * 2^(D-1) with each edge shared by two vertices. The local setting deliberately omits cost or convexity assumptions, retaining only finiteness and decidable precedence.
proof idea
The declaration is a direct definition consisting of a single universal quantifier over the precedence relation Prec.
why it matters
This predicate supplies the eligibility test used by every subsequent construction in the module, including the Candidate structure, chooseCandidate, exists_minimal_eligible, and the sequential schedule existence theorem. It therefore realizes the constructive half of the T2 serialization result for finite histories. The predicate appears in downstream lemmas that preserve conservation properties across any topological ordering.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.