Theorem: Typed schedule locality

Every terminal observable on $Y$ pulls back to an observable on $N_{0,n}(Y)$, and

Equal input reductions on the backward region, including any retained reference, give equal corresponding output reductions.

Proof. A block disjoint from the current backward support acts on an identity factor. Its adjoint fixes that identity. A block meeting the support can enlarge it only within that block. Backward induction proves the support inclusion. Each added point is within one block diameter of an existing point; the triangle inequality proves the radius bound. Equality of all pulled-back expectations proves the reduction statement.