isMinimalIn
plain-language theorem explainer
The predicate isMinimalIn identifies an event e in a finite set H as minimal under a precedence relation prec if e belongs to H and no other element in H precedes it. Researchers constructing sequential schedules for finite recognition histories cite this predicate when enforcing causal constraints. The definition is realized directly as the conjunction of membership and the universal negation of precedence.
Claim. Let $E$ be a type of events and let $H$ be a finite subset of $E$. Let $e$ be an event in $E$ and let $prec$ be a precedence relation on $E$. Then $e$ is minimal in $H$ under $prec$ when $e$ belongs to $H$ and no $e'$ in $H$ satisfies $prec$ $e'$ $e$.
background
The Atomicity module supplies a constructive, axiom-free serialization result for finite recognition histories. It works abstractly over an event type $E$ equipped with a precedence relation $prec$, where $prec$ $e_1$ $e_2$ means $e_1$ must occur before $e_2$. This setting tightens T2 by providing deterministic one-per-tick schedules that respect the relation, remaining independent of cost or convexity assumptions from T5.
proof idea
The definition directly encodes the minimality condition as the conjunction of membership in the finite set $H$ together with the assertion that no element $e'$ in $H$ satisfies the precedence relation to $e$. No lemmas are applied; it is the primitive predicate used by subsequent existence results such as exists_minimal_in.
why it matters
This definition enables the existence of sequential schedules for finite histories, supporting the serialization outcome that tightens T2 in the forcing chain. It is referenced by the Precedence abstraction and by downstream constructions such as exists_minimal_in and topoSort in the same module. By providing an axiom-free way to pick minimal events, it contributes to deterministic ordering without relying on the J-uniqueness or phi fixed point from T5-T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.