Berthelot's original conjecture on rigid cohomology

Let $(S,\overline{S},\mathfrak{S})$ be a smooth and proper $\mathcal{V}$-frame, and let $f:X\to S$ be a smooth and proper morphism of $k$-varieties. The $j\text{-}S^\dagger\mathcal{O}_{]\overline{S}[_{\mathfrak{S}}}$-module with integrable connection $\mathbf{R}^qf_{\mathfrak{S},\mathrm{rig}*}\mathcal{O}_{X/K}^\dagger$ is defined by an overconvergent $(F)$-isocrystal.

Berthelot's conjecture. There is a unique object

$$\mathbf{R}^qf_{\mathrm{rig}*}\mathcal{O}_{X/K}^\dagger\in (F)\text{-}\mathrm{Isoc}^\dagger(S/K)$$

whose realization is the stated module with connection. Equivalently, it is coherent, its connection is overconvergent, and the resulting object of $\mathrm{Isoc}^\dagger(S/K)\cong\mathrm{MIC}^\dagger((S,\overline{S},\mathfrak{S})/K)$ depends only on $S$, not on the frame; it moreover has a canonical Frobenius structure.

This is Berthelot's original formulation concerning the overconvergence and frame-independence of relative rigid cohomology.