Proposition: Finite-program channel accounting

A finite acyclic instruction tree built from declared allocations, gates, destructive readouts, classical control, and discard has path maps $K_h$ with

Its reported selective maps are

Its complete denotation is CPTP and reference preserving.

Proof. A complete history fixes the classical choices. Compose the corresponding allocation isometries, gates, and measurement bras. Branch normalizations cancel against branch probabilities. At a readout, ${\sum }_x{M}_x^{†}{M}_x=I$; gates and allocations are isometric. Backward induction over the finite tree proves the completeness identity. Group histories by reported output and tensor the path maps with a reference identity.