Proposition: Complete record accounting

The map $\hat{T}$ is UCP. The outcome probability in state $\omega$ is $\omega (T_y(1))$. Discarding the record gives the nonselective channel

These constructions preserve all independent matrix references.

Proof. At every matrix level, positivity in a direct sum is blockwise. Each summand is mapped positively, so their sum is completely positive. The stated completeness identity is unitality. The central unit of outcome block $y$ pulls back to $T_y(1)$, giving its probability. Embedding an unrecorded observable diagonally gives $T_{\mathrm{ns}}$. Amplification preserves the identities.