pith. machine review for the scientific record. sign in
def definition def or abbrev high

isMinimalIn

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  40def isMinimalIn (prec : Precedence E) [DecidableEq E] [DecidableRel prec]
  41    (H : Finset E) (e : E) : Prop :=

proof body

Definition body.

  42  e ∈ H ∧ ∀ e' ∈ H, ¬ prec e' e
  43
  44lemma isMinimalIn.mem {prec : Precedence E} [DecidableEq E] [DecidableRel prec]
  45    {H : Finset E} {e : E} :
  46    isMinimalIn (E:=E) prec H e → e ∈ H :=
  47  And.left
  48
  49/-- Minimality existence on a finite, nonempty `H` under well‑founded precedence. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.