Theorem: C1: reference-preserving sequential soundness

Under specified Born semantics and Assumption ass:stream, a legal finite programme with such a certificate implements its declared channel, including every reference, and obeys its stated storage ledgers.

Proof. Decoder operations act only on emitted names and fresh laboratory ancillas. Each subsequent emission acts on the remnant. These operations commute after identifying their distinct tensor factors. Semantically, one may therefore place the fixed emissions before the decoder operations, without claiming that this rearranged batch schedule has the same memory cost.

On each complete decoder history, compose allocation isometries, unitaries, and destructive measurement bras into a linear path map $K_h$. Branch normalizations cancel against their probabilities. Backward induction on the finite instruction tree gives

Reported selective maps are

Their sum is CPTP.

Equality on all input matrix units is equality of channels. Tensoring with a reference preserves it. A diamond-error certificate already controls every such extension.

The two ledgers count all named quantum factors at every actual event, including supplier holdings. Their maxima are precisely the declared resource bounds. Commutation in the correctness proof does not erase storage in the actual schedule.