Theorem: Programme-to-channel and ledger theorem

Every legal finite programme induces a CPTP map on its declared accessible input. Its action on reference-entangled inputs is the same map tensored with the reference identity. Register counting along every branch bounds its declared peak and storage costs.

Proof. Associate a CP map with each branch prefix by composing its operation maps, tensoring fresh states, and tracing explicit discards. For an instrument, summing the children yields the parent's trace-preserving continuation. Induction from the leaves to the root shows that the sum of complete branch maps is CP and TP. Replacing an abort by a fixed state is a TP continuation of that abort branch.

Every operation has support only on declared registers. Tensoring with an untouched reference commutes with all compositions and branch sums, proving the reference statement. The live-set update at each node is specified by arrivals, preparations, operations, and discards. Its cardinality and holding intervals therefore give the stated pathwise bounds.