Theorem: Complete finite-program soundness

Every finite acyclic legal program denotes a CPTP hybrid-output channel and has path maps $K_h$ satisfying

Reported outcomes group the unnormalized branch maps $X\mapsto K_{h}X{K}_h^{†}$. The same statement holds with arbitrary untouched references. Every branch terminates within the finite height of its instruction tree.

Proof. Allocation and unitary gates are isometric. Readout satisfies ${\sum }_x{M}_x^{†}{M}_x=I$. Classical discard sums blocks without conditional normalization.

Backward induction on the instruction tree proves completeness. Sequential composition composes the path maps; coarse-graining adds their CP maps. Tensoring each path map with a reference identity proves the complete-channel statement. A finite acyclic tree has finite maximum branch length.