Rigidification of arithmetic $\mathscr{D}$-modules and an overconvergent Riemann-Hilbert correspondence

In this article, I define triangulated categories of constructible isocrystals on varieties over a perfect field of positive characteristic, in which Le Stum's abelian category of constructible isocrystals sits as the heart of a natural t-structure. I then prove a Riemann-Hilbert correspondence, showing that, for objects admitting some (unspecified) Frobenius, this triangulated category is equivalent to the triangulated category of overholonomic $\mathscr{D}^\dagger$-modules in the sense of Caro. I also show that the cohomological functors $f^!$, $f_+$ and $\otimes$ defined for $\mathscr{D}^\dagger$-modules have natural interpretations on the constructible side of this correspondence. Finally, I use this to prove that, for any variety $X$ admitting an immersion into a smooth and proper formal scheme, rigid cohomology (with lisse coefficients) agrees with cohomology defined using arithmetic $\mathscr{D}$-modules.