Theorem: Exact operational realization

On every admissible graph, the network (eq:or) satisfies:

1. every reduction touches finitely many linearly owned channels;

2. every finite experiment terminates, and every maximal legal schedule completes it;

3. distinct simultaneously enabled operations have disjoint channel ownership and commute exactly;

4. all schedules produce the same joint records;

5. for each event,

   $$b_v=\underset{p\le v}{\bigvee }{u}_p;$$

6. for distinct events, $p⇝q$ if and only if $p<q$;

7. an intervention outside the dependency past of an observation does not change it;

8. every finite collection of records is determined by a finite down-set.

Proof. The degree bound bounds the number of consumed and produced channels. In a finite experiment, each reduction decreases $|D\setminus H|$ by one. If this set is nonempty, one of its minimal elements is enabled. Hence every maximal legal schedule terminates with all events completed.

Two distinct simultaneously enabled events cannot be connected by a dependency edge. Unique producers, unique consumers, and distinct edge names make their channel operations disjoint. They also write distinct private records, so they commute exactly. Corollary cor:schedules gives schedule independence.

Induct along a topological order of the finite past of $v$. Every strict ancestor of $v$ is an ancestor of an immediate predecessor. Associativity and idempotence of disjunction give (eq:ancestoror).

If $p<q$, set all controls other than $u_p$ to zero. Changing $u_p$ changes $b_q$. If $p\nleqq q$, the expression for $b_q$ contains no $u_p$, proving the converse. The same dependency induction proves invariance under changes outside the past of the observed records. It also allows replacement operations, provided they preserve the specified channel interface and introduce no external dependencies.

Finally, the union of the principal pasts of finitely many observed events is a finite down-set.