Proposition: Coherent insertion and displaced carrier

The map $W$ is an isometry implemented by one message-independent unitary. It preserves every logical matrix unit and arbitrary reference entanglement.

After insertion, the carrier marginal is independent of the diary, but the carrier can be correlated with the remaining source. It must therefore remain in the complete residual.

If the carrier Hamiltonian is degenerate and preparation interactions are absent before and after the swap, the change in mean source energy satisfies

for every logical density operator $\rho$.

Proof. Composition of the isometry $J_D$, a fixed pure ancillary preparation, and a unitary proves $W^{†}W=I_C$. Linearity gives the action on all matrix units; tensoring the unitary with $I_Q$ proves the reference statement.

Exchanging the entire two-mode subsystems transfers the old source two-mode marginal to the carrier. Its correlations with the remaining source are also transferred, rather than erased. Fermionic permutation signs are fixed by the mode ordering and the even logical code; they do not create a message-dependent operation.

Both source energy expectations lie in $[0,M_N]$, proving the final inequality.