Theorem: Restricted destructive deferred readout

Start from geometry $g_0$ and a state $\rho$ on $S\otimes B$. Compare:

1. immediate ${\mathsf{Enter}}_S$, followed by a finite continuation;

2. coherent recording into a fresh $A$, the corresponding continuation, and terminal ${\mathsf{Enter}}_A$.

During the continuation assume:

1. matter commands act only on the current complement $B_k$, never on the retained $S$, carrier $A$, or immediate record $R$;

2. coupling inputs and state-dependent guards depend only on the reduced state on $B_k$;

3. geometric rules inspect only their declared geometric labels;

4. control, support, and resources are blind to the excluded registers, as in ass:blind.

Align executions by their common continuation events. Their geometric traces and complement reductions coincide at every aligned event. After terminal carrier readout, restricting the deferred output away from the retained factor $S$ gives the immediate output on $R\otimes B_T$.

Proof. Immediately after the two initial operations,

Thus the complement reductions agree.

Suppose they agree at a continuation event, together with geometry and control. Conditions (D2)–(D4) and ass:blind give the same guard result, rule, resource certificate, and geometric update. Condition (D1) gives the same matter channel on the complement. By lem:partial-trace, its application preserves equality of complement reductions. Induction establishes the common trace.

For this fixed pair of inputs, compose the matter channels selected along the common trace into a channel $\Lambda$ on the continuation interface. Equation eq:continuation gives equality of the final outputs on $R\otimes B_T$.