Lemma: Finite completeness

Equation (eq:pathmaps) defines completely positive selective maps whose recorded channel is trace preserving. All identities extend by the identity on every untouched reference.

Proof. Each path gives a completely positive summand. Backwards induction on the finite instruction tree gives the completeness relation: isometries preserve the identity in the adjoint calculation, and at a readout the squared measurement bras sum to the identity. Grouping complete histories changes no sum. Tensoring every path map with a reference identity proves the extension.