Precedence
plain-language theorem explainer
Precedence is the binary relation type on events that encodes the requirement that one event must occur before another in a finite recognition history. Atomicity lemmas on topological ordering and conservation preservation cite it as the input interface. The declaration is a direct abbreviation to the Prop-valued function E → E → Prop with no computational content.
Claim. Let $E$ be a type of events. A precedence relation on $E$ is a binary relation $e_1 prec e_2$ of type $E to E to Prop$, read as “$e_1$ must occur before $e_2$”.
background
The Atomicity module supplies constructive, axiom-free serialization for finite recognition histories over an abstract event type $E$. The precedence relation supplies the causal or ledger constraints that any valid schedule must respect. The module deliberately stays independent of cost convexity (T5) and assumes only finiteness together with decidable precedence on the history. Upstream, isMinimalIn defines an element $e$ in a finite set $H$ to be minimal when $e in H$ and no $e'$ in $H$ satisfies $prec e' e$.
proof idea
The declaration is a one-line abbreviation that directly equates Precedence E to the function type E → E → Prop. No tactics or lemmas are applied; the abbreviation simply provides a named interface for the relation used by isMinimalIn, exists_minimal_in, and the schedule existence theorems.
why it matters
Precedence supplies the ordering primitive for atomic_tick and exists_sequential_schedule, which deliver a one-per-tick serialization of any finite history that respects the relation. It thereby tightens T2 by furnishing a deterministic topological order without new axioms. The same relation appears in sequential_preserves_conservation, allowing conservation predicates to be lifted from single postings to full schedules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.