Finite instruments can be coherently deferred

By [F12], $K$ is nonzero. By [F1], choose finite branch Kraus families, pad them to a common positive length, and form the coherent record isometry $V:H\to K\otimes E$. By [F2], pad the input by a finite clean register and extend $V$ to a surjective isometry $W$ satisfying $W(x\otimes a_0)=Vx\otimes b_0$.

Reorder $K\otimes E$ so the observed label register is first, followed by $K$, the hidden register, and the padding register; this is the canonical basis permutation of [F7]. Apply the block operation from [F3] on the observed label and $K$, acting identically on the hidden register, padding register, and reference, then undo the permutation. On the label-$a$ subspace this applies $S_a$ and leaves the two environment registers unchanged.

Let $Jx=x\otimes a_0$ be the input-padding inclusion. Checking on each elementary vector $x\otimes r$ gives $(W\otimes I_R)(J\otimes I_R)(x\otimes r)=Vx\otimes b_0\otimes r$; these vectors span, and [F6] makes the tensor extensions well-defined. Hence the inclusion maps agree on all vectors, and conjugating any operator $X$ by them gives the corresponding equality of extended output operators. This remains true for vectors and operators entangled across $H$ and $R$.

Put $r=\dim R$. If $r=0$, [F10] gives $R=0$, hence $X=0$ and the amplification identity is immediate. Otherwise choose an ordered orthonormal basis $(c_k{)}_{k<r}$ of $R$ by [F10] and use it to identify the reference with ${\mathbb{C}}^r$. Write $X=[X_{kl}]$ in blocks. By [F4], block $(k,l)$ of ${\mathcal{I}}_a^{(R)}(X)$ is ${\mathcal{I}}_a(X_{kl})={\sum }_j{M}_{a,j}{X}_{kl}{M}_{a,j}^{†}$ by [F5]. By [F6], the same is block $(k,l)$ of ${\sum }_j(M_{a,j}\otimes I_R)X(M_{a,j}^{†}\otimes I_R)$. Equality of all blocks proves this finite-Kraus formula for every $X$.

For each $a$, the observed-label projection keeps only the terms with label $a$ in the coherent isometry. Retain that label and take the partial trace [F8] only over the hidden Kraus register and the padding register; the trace keeps equal hidden indices $j$, and [F13] gives $⟨b_0,b_0⟩=1$ for the returned padding. The label factor is $\mathrm{\mid }{e}_a⟩⟨e_a\mathrm{\mid }$ by [F11]. Thus, after canonical factor permutation, the label-resolved branch operator is $({\sum }_j(S_a{M}_{a,j}\otimes I_R)X(S_a{M}_{a,j}\otimes I_R{)}^{†})\otimes \mathrm{\mid }{e}_a⟩⟨e_a\mathrm{\mid }=(S_a\otimes I_R){\mathcal{I}}_a^{(R)}(X)(S_a^{†}\otimes I_R)\otimes \mathrm{\mid }{e}_a⟩⟨e_a\mathrm{\mid }\mathrm{.}$ This equals ${\mathcal{J}}_a^{(R)}(X)\otimes \mathrm{\mid }{e}_a⟩⟨e_a\mathrm{\mid }$ by step 2.1 and step 2.2 and [F6]. Taking the partial trace of the label factor gives exactly ${\mathcal{J}}_a^{(R)}(X)$ because $e_a$ is unit by [F13].

Taking traces of equal branch operators gives the same outcome probabilities. Division gives the same conditional operator only when the shared branch weight is positive; when it is zero both descriptions assign $\mathrm{\perp }$ by [F9]. Equality for arbitrary $X$ on $H\otimes R$ preserves all reference correlations. The finite-dimensional operator construction asserts no additional implementation or cost.