Theorem: Spectator-extension invariance

Consider a finite certified execution

and an admissible initial extension satisfying eq:extension, with the same geometry, finite control state, and original-name locations. Assume:

1. each original matter map in the extended execution is tensored with ${\mathrm{id}}_N$;

2. each coupling algebra is embedded as ${\mathcal{A}}_v\otimes I_N$, or its input is a specified function only of the original reduced state;

3. spectator-blind control and resources, ass:blind, hold;

4. spectator locations have the required certified transport, and no spectator outcome is used during the comparison.

Then a paired extended execution is legal and, at every step,

Original-name locations also agree.

Proof. The assertions hold initially. Assume they hold at step $k$. By ass:blind, both executions select the same rule, guard result, support, and resource certificate.

For a geometric rule, the geometric and resource inputs agree. Its output geometry and original-name transport therefore agree. The matter states are unchanged.

For a matter rule, the geometric parameter is common. By lem:partial-trace,

For a coupling rule, every $A\in {\mathcal{A}}_v$ has equal expectation:

The rule receives identical state functionals and returns identical certified geometry and original-name transport. The same conclusion holds when its input is a specified function of the original reduction.

The common control selection gives the same successor control state. Admissibility and the transport certificates establish legality of the next paired configurations. Induction completes the proof.