Theorem: Scheduled locality

The complete network satisfies

Equal input reductions on $N_{s,t}(Y)$ give equal output reductions on $Y$. For a joint reference conclusion, the equalities must include the reference. A deterministic intervention outside the complete backwards region does not change the output.

If each dependency edge has a supplied future-causal host embedding, its ancestors lie in the prescribed metric past of the output.

Proof. An excluded block sees an identity factor in the pulled-back observable. Its adjoint is unital. An included block enlarges support only inside itself. Backward induction proves the inclusion. Testing all output observables proves the reduced-state statements and the intervention conclusion. Adjoining the reference algebra gives the joint version. Concatenation of the separately certified causal edges proves the geometric containment.