Finite SDPs and feasibility directions

Use output-first, unnormalized Choi matrices

For a decoder $R=\mathsf{J}(\mathcal{D})$,

For a difference $\Delta$ of CPTP channels, the half-diamond primal and dual are

and

Their common value is ${\Vert \Delta \Vert }_{\diamond }/2$ Watrous.

For noise $\mathcal{N}$, unrestricted recovery minimizes $\lambda$ over

All these constraints are tested in the implementation.

For every channel $\Lambda$, the independent acceptance checks include $\mathsf{J}(\Lambda )⪰0$ and ${\mathrm{Tr}}_O\mathsf{J}(\Lambda )=I_M$. A fixed-channel distance primal lower-bounds only that decoder's error, not the optimal recovery over other decoders. Here the benchmark's matching recovery lower bound is analytical.

For a raw decoder Choi matrix, the explicit numerical repair is

It is positive and trace preserving in exact arithmetic. The implementation verifies these properties numerically and archives the repair size. Floating-point residual acceptance is not formal or interval-certified feasibility.