Tsuzuki's conjecture on relative overconvergent isocrystals

Suppose that $(X,\overline{X})\to(S,\overline{S})$ is a proper Cartesian morphism of $k$-pairs with $X\to S$ smooth, $(S,\overline{S},\mathfrak{S})$ is a smooth $\mathcal{V}$-frame, and $E\in(F)\text{-}\mathrm{Isoc}^\dagger((X,\overline{X})/K)$. The module with integrable connection $\mathbf{R}^qf_{\mathfrak{S},\mathrm{rig}*}E$ should arise from an overconvergent $(F)$-isocrystal.

Tsuzuki's conjecture. There is a unique object

$$\mathbf{R}^qf_{\mathrm{rig}*}E\in(F)\text{-}\mathrm{Isoc}^\dagger((S,\overline{S})/K).$$

If $\overline{S}$ is proper, this object depends only on $f:X\to S$ and $E$.

This generalizes Berthelot's original formulation from smooth proper morphisms of varieties to proper Cartesian morphisms of pairs. The source records it as one of the open versions of Berthelot's conjecture.