Coherence conjecture for holonomic arithmetic $\mathcal{D}$-modules over the generic fibre

Let $S$ be the base formal scheme, let $\eta$ denote its generic point, and let $\mathbb{D}_S$ and $\mathbb{D}_{\mathfrak{S}}$ be the corresponding arithmetic differential-operator spaces. Let $\operatorname{Hol}(\eta,\mathbb{D}_S,\mathbb{D}_{\mathfrak{S}})$ denote the category of holonomic objects on $\eta$. Coherence conjecture. Every object

$$E\in\operatorname{Hol}(\eta,\mathbb{D}_S,\mathbb{D}_{\mathfrak{S}})$$

is coherent as an $\mathcal{O}_{\mathbb{D}_{\mathfrak{S}}}(^{\dagger}s)_{\mathbb{Q}}$-module. This would imply finite-dimensionality of the arithmetic $\mathcal{D}$-module cohomology of suitable holonomic complexes over $\mathcal{E}^{\dagger}_K$, including $H^i_{\mathcal{D}}(X_\eta/\mathcal{E}^{\dagger}_K)$; the source gives no resolution status.