This may look like a problem that could easily be looked up, but it's not quite as easy as it first appears, hence my asking. I'm going to phrase my question in terms of the "Schroedinger picture" version of the Stinespring dilation theorem, which is more familiar with physicists than the "Heisenberg picture" version, which is perhaps more familiar with mathematicians.
Consider a completely positive trace preserving (CPTP) map $\mathcal{F}$ from bounded linear operators on the Hilbert space $\mathcal{S}_i$ to bounded linear operators on the Hilbert space $\mathcal{S}_f$ where, in general, $\mathcal{S}_i\not\cong\mathcal{S}_f$. The Stinepring dilation theorem states that such a CPTP map can always be written by specifying some projector, $|0\rangle\langle 0|$, on a dilation Hilbert space $\mathcal{E}_i$ and applying some unitary operator $U$ to the bounded linear operators on $\mathcal{S}_i \otimes\mathcal{E}_i$ followed by tracing over the Hilbert space $\mathcal{E}_f$, where $\mathcal{E}_f$ is defined such that $\mathcal{S}_i \otimes\mathcal{E}_i\cong\mathcal{S}_f\otimes \mathcal{E}_f$. In other words $\mathcal{F}$ may always be achieved via some unitary $U$: $$ \mathcal{F}(\rho)=\mathrm{Tr}_{\mathcal{E}_f} [U(\rho\otimes|0\rangle_{\mathcal{E}_i}\langle0|)U^\dagger]. $$ Note that I am not assuming that any of these Hilbert spaces are isomorphic, with the exception that I am assuming $\mathcal{S}_i \otimes\mathcal{E}_i\cong\mathcal{S}_f\otimes \mathcal{E}_f$ (so that $U$ is unitary rather than just an isometry).
My question: in this context, how large do I need to allow $\mathcal{E}_i$ (or $\mathcal{E}_f$) to be so that I am guaranteed that such a dilation exists. I know that if $\mathcal{E}_i\cong\mathcal{E}_f$ and $U$ is an isometry then $\dim \mathcal{E}_i\leq\dim\mathcal{S}_i\dim\mathcal{S}_f $, but I'm preferring unitarity over isomorphism.