Theorem: Restricted destructive deferred readout

Start with common geometry and declared control data and a state $\rho$ on $S\otimes B$. Compare:

1. immediate ${\mathrm{Enter}}_S$, followed by continuation on $B$;

2. allocation of $A$, coherent recording, the corresponding continuation on $B$, and terminal ${\mathrm{Enter}}_A$.

Between recording or initial readout and terminal carrier readout, assume:

1. matter commands act only on the current continuation interface $B_k$, not on $S,A$, or the immediate record $R$;

2. coupling inputs and state-dependent guards use only the reduction on $B_k$;

3. geometric rules inspect only declared geometric labels;

4. control, supports, capacities, and transport of continuation names are blind to the excluded registers, with separately reserved storage as in ass:sched.

Then geometric traces coincide at aligned continuation events. After terminal carrier readout, the deferred output restricted away from $S$ equals the immediate output on $R\otimes B_T$.

Proof. Both initial continuation reductions equal ${\mathrm{Tr}}_S\rho$:

Induction using (D1)–(D4) gives common commands, guards, geometry, continuation transports, and reductions at every event. For this fixed input, compose the matter channels selected along the common trace into $\Lambda$. They act only on the continuation interface. Equation (eq:continuation) gives equality of the complete common record–matter output.