Lemma: Complete finite-circuit semantics

A frozen instance defines a CPTP logical channel on every message operator, and hence on every message-reference extension. If finite measurement branches are added, their path maps $K_h$ obey

The reported selective maps are

Proof. The initialized circuit is an isometry. Partial trace gives a CPTP map. For measurement branches, compose the branch Kraus operators, unitaries, and allocation isometries. Backward induction on the finite instruction tree gives the displayed completeness identity. The formulas are linear-map identities and remain true after tensoring with an untouched identity channel.