Theorem: Spectator consistency for Contract E

Under Assumption ass:blind, compare a finite execution with an extension satisfying ${\mathrm{Tr}}_N\tilde{\rho }=\rho$ on the original accessible interface. Use the same initial geometric and control labels and original-name locations.

At every step the executions have the same geometric trace, the same accessible reduced matter state, and the same original-name locations. The spectator extension may initially be entangled.

Proof. For any linear map $\Phi$,

This follows by expansion in matrix units on $N$. A matter step therefore preserves equality of accessible reductions. Equal reductions give equal declared state functionals, so geometric and coupling steps choose the same successors. Blindness makes guards, certificates, and resource checks identical, and the same fixed location maps apply. Induction proves the assertion.