Corollary: Constraint compatibility on the deferred boundary

Compare an immediate destructive-readout execution with a coherent-recording execution. During their continuations suppose:

1. source and control inputs use only the evolving complement $B$, not $R$, $A$, or retained $S$;

2. initial geometry, controller data, permissions, resource inputs, and original complement locations agree;

3. all continuation matter channels act only on $B$, are selected equally from equal accessible inputs, and extend by identities on excluded factors;

4. excluded-factor storage and transport are separately legal and cannot affect guards or geometric decisions.

Their geometric outputs and certification decisions agree at every aligned continuation step. After terminal readout of $A$, the record–complement outputs agree when the deferred output is additionally restricted away from $S$.

Proof. Initially, both $B$-reductions are ${\mathrm{Tr}}_S\rho$. Equal complement reductions give equal accessible source functionals. Constraint-blindness selects the same geometric and control outputs, and the common complement channel preserves equality by A:lem:restriction. Induction proves the continuation assertion.

For the fixed initial pair, these common choices select the same finite sequence of complement channels. Their composition is a common channel $\Lambda$. Apply A:lem:deferred to $\Lambda$ to obtain the terminal record–complement equality.