Theorem: Reference-preserving adequacy

For every finite acyclic instruction tree, and each fixed classical input block:

1. the denotation is a CPTP channel to the declared hybrid output;

2. there are quantum path maps $K_h$ satisfying

   $$\sum _h{K}_h^{†}{K}_h=I;$$

3. each reported output block is the sum of its unnormalized maps $X\mapsto K_{h}X{K}_h^{†}$;

4. the same denotation holds with an arbitrary untouched quantum reference;

5. every evaluation branch terminates within the finite height of the tree.

Proof. Allocation is an isometry, and a unitary gate is trace preserving. Destructive readout satisfies ${\sum }_x{M}_x^{†}{M}_x=I$. Classical control selects a complete channel on each classical block. Classical discard sums blocks without conditional normalization.

Induction composes path maps. Backward induction, using completeness at each readout node, gives ${\sum }_h{K}_h^{†}{K}_h=I$. Grouping histories with the same reported output gives the corresponding hybrid block. Tensoring each quantum path map with the reference identity proves complete positivity and the reference statement.

A finite acyclic tree has a finite maximum branch length.