Theorem: D': exact one-shot environment ledger

In Definition def:oneshot:

1. the minimum environment dimension is $R$;

2. full computational readout followed by classical coarse-graining needs

   $$e=\lceil {\log }_{2}R\rceil$$

   environment qubits;

3. within a rectangular outcome/index register split, the exact register cost is

   $$e_{\mathrm{split}}=\lceil {\log }_2\left|X_{+}\right|\rceil +\lceil {\log }_2\underset{x}{\max }{r}_x\rceil ;$$

4. the full-readout one-shot peak is $s^{\prime }+e$. For an input already occupying $s$ slots in a region with $o_{\mathrm{other}}$ unrelated occupied slots, realization is possible precisely when

   $$o_{\mathrm{other}}+s^{\prime }+e\le \mathrm{cap}(v).$$

   Equivalently, the additional free slots must cover $s^{\prime }+e-s$.

Proof. A positive Choi matrix of rank $r_x$ has a spectral decomposition with exactly $r_x$ nonzero vectors. Unvectorizing them gives a Kraus family of size $r_x$. Conversely, a family of $d_x$ Kraus operators gives a Choi sum of $d_x$ rank-one matrices, so $r_x\le d_x$.

If an environment block for outcome $x$ has dimension $d_x$, expanding the dilation in a basis of that block gives at most $d_x$ Kraus operators for ${\Phi }_x$. Thus

For the upper bound, choose minimum Kraus families and define

Completeness gives $V^{†}V=I$. The environment has $R$ basis states, and its block readout realizes the instrument.

Encode those states in $e$ qubits and measure the full fine index. On reporting only $x$, the conditional output density operator is

This is a classical mixture of fine pure branches, not a single pure primitive residual. No unmeasured quantum environment needs an affine discard operation; classical forgetting is explicit.

For a prescribed product split, the outcome register must encode $\left|X_{+}\right|$ labels and the common index register must encode at least ${\max }_x{r}_x$ indices. The displayed cost is both necessary within that model and sufficient.

The isometry embeds a $2^s$-dimensional space in a $2^{s^{\prime }}R$-dimensional one, so $s^{\prime }+e\ge s$. Allocate $s^{\prime }+e-s$ zero ancillas, embed the isometry in the $s^{\prime }+e$-qubit space, and extend it to a unitary. The peak and local-capacity condition follow.