Assumption: Blindness of the complete transition specification

Adding the spectator does not change:

1. the label dictionary or any input-label interpretation;

2. the selected branch maps, except for tensoring with ${\mathrm{id}}_N$;

3. guard results, successor labels, certificates, or transport of original names;

4. controller updates or the declared resource reserve.

Spectator storage and any spectator location history are separately reserved. Spectator outcomes are not read by the controller.