Proposition: Complete branch soundness

For a finite programme built from isometries, unitaries, complete instruments, classical controls, and specified discards, let $K_{\gamma }$ be its complete-history Kraus maps. Then

Its reported selective maps and complete channel preserve all references. Equality on every input matrix unit proves equality of the complete channels.

Proof. At the final instruction, instrument completeness gives the identity sum. Backward induction through each instrument, unitary, and isometry gives the displayed identity. The branch maps therefore define a CPTP sum.

Matrix units span the input operator space. Equality on them gives equality of linear maps and hence of every reference extension. Normalized branch states are not substituted for the unnormalized Kraus sums.