Theorem: Matched replacement invariance

Consider two runs on the same net, partitions, and record interfaces. Suppose:

1. their initial states agree on $\mathfrak{A}(N_{t_0}(Y))$;

2. at every tick $s$, their specified global block devices agree on every block meeting $N_{s+1}(Y)$.

Then their terminal snapshots on $\mathfrak{A}(Y)$ agree. Devices outside the backward recursion may be replaced by arbitrary devices from the stated localized class.

For the reference version, the initial restrictions must agree jointly on $\mathfrak{A}(N_{t_0}(Y))\otimes M_r$.

Proof. Pull an arbitrary terminal observable backward. At each layer only the meeting block devices contribute by Theorem thm:onelayer, and these are common. Thus the two terminal pullbacks are equal and belong to $\mathfrak{A}(N_{t_0}(Y))$. Their expectations agree by (i). The amplified calculation is identical.