Proposition: Finite-program soundness

A finite acyclic instruction tree built from specified pure allocation, specified unitary constants, destructive Enter, classical control, classical discard, and a fixed returned hybrid type denotes a CPTP channel. Every quantum name is returned or explicitly consumed. There are refined path maps $K_h$ with

and each reported output block is the sum of its unnormalized path maps $X\mapsto K_{h}X{K}_h^{†}$. The denotation retains arbitrary references, and every branch terminates.

Proof. Allocation is isometric, unitaries are trace preserving, and readout bras are complete. Classical control selects a complete continuation on each block; discard sums blocks. Backward induction on the finite tree proves path completeness. Grouping histories proves the block formula. Tensoring path maps with $I_Q$ proves the reference statement. A finite tree has finite maximum branch length.