Proposition: Agreement on the admitted finite events

For the declared preparation, labels, rods, and causally embedded schedule:

1. the record $k$ labels the event $\kappa (k)$ with $T(\kappa (k))=t_k$ and the external datum $\delta (k)$;

2. each accessible surviving name has its prescribed rod coordinates;

3. every scheduled ancestor of an output lies in the output's metric past.

Proof. The first two statements are the specified maps evaluated on their domains. Their operational probabilities and residuals are Theorem thm:instrument. The third follows by concatenating the certified causal edges.