Remark: Finite descriptions and stability

The Haar existence statement is an ideal-control theorem. It does not assert that a generic Haar matrix has a finite exact description in a discrete gate alphabet.

A finite-description approximation can be obtained without changing the operational interpretation. Apply Theorem thm:joint with a stricter leakage target, for example $\zeta /2$. For a successful unitary, $z_{k_{\ast }}<\zeta$ has a margin, and the entropy inequalities have a strictly positive gap. Channels and finite-dimensional entropy are continuous in $U$; more explicitly,

Hence sufficiently accurate finite gate approximations preserve the leakage target and the strict entropy gap. Dense finite gate families provide such approximations Barenco, while Proposition prop:transfer prices the same decoder's return error.

This proves robustness and existence of finite-precision realizations, not an executed search or an efficient compilation.