Theorem: Spectator-extension invariance

Consider an original certified run

and an initial admissible spectator extension with the same original geometry, locations, control, and declared resources. Suppose:

1. original matter maps extend by ${\mathrm{id}}_N$;

2. coupling algebras extend by $A\mapsto A\otimes I_N$, or coupling inputs are specified functions only of the original reduced state;

3. ass:sched holds, including spectator transport and separate storage legality;

4. spectator outcomes are neither read nor used during the run.

Then a paired extended run is legal and, at every aligned step,

Original transports and declared control outputs also agree.

Proof. Induct on the steps. Equal declared inputs select the same command, guard, support, and certificate.

A geometric rule receives equal geometric and resource labels and leaves matter unchanged. A matter rule has the common parameter $q_k$, and lem:trace preserves the reduction identity. For a coupling rule,

so its complete input functional and output agree. The transport and separate-reservation clauses establish legality and equality of original locations and control data at each step.