Proposition: Finite path accounting

Every finite acyclic program built from the specified primitives has linear path maps $K_h$ satisfying

For reported outcome $y$, its selective map is

The sum over reported outcomes is a complete channel, including every untouched reference.

Proof. A complete history fixes the classical choices. Compose allocation isometries, gates, wiring maps, and destructive measurement bras along that history to obtain $K_h$. Successive branch normalizations cancel against their probabilities.

At a readout node, ${\sum }_x{M}_x^{†}{M}_x=I$. Allocation is isometric and gates are unitary. Backward induction over the finite instruction tree gives the completeness identity. Grouping histories gives the reported maps. Tensoring every path map with a reference identity proves the referenced statement.