Lemma: Decoder physicality

The map ${\mathcal{D}}_{\star }$ is CPTP on every input state on ${\mathcal{H}}_R$.

Proof. Use the retained Kraus operator $W^{†}$, together with

Their effects sum to $P+|01⟩⟨01|+|10⟩⟨10|=I_R$. Their Kraus sum is exactly (eq:decoder).