Existence of a universal lower-semicomputable semi-density matrix

A lower-semicomputable semi-density matrix is a positive operator of trace at most one that admits effective approximation from below. For such matrices, write $\rho\leq c\mu$ when $c\mu-\rho$ is positive semidefinite.

Universal semi-density matrix conjecture. There is a lower-semicomputable semi-density matrix $\mu$ dominating every other such matrix: for every lower-semicomputable semi-density matrix $\rho$, there is a constant $c>0$ such that

$$\rho\leq c\mu.$$

This is the quantum analogue of the existence of a universal lower-semicomputable semimeasure and is needed for Gács' quantum algorithmic entropy. The supplied text identifies it as one of two crucial results whose proofs in the earlier work have a flaw; its resolution is not given here.