The derived $\infty$-category of Frobenius modules

We prove that for $X$ a quasi-compact $\mathbb{F}_p$-scheme with affine diagonal (e.g.\ $X$ quasi-compact
and separated) there is a t-exact equivalence
$\mathcal D(\mathrm{Frob}(\mathrm{QCoh}(X),F_*)) \to \mathrm{Frob}(\mathcal D(\mathrm{QCoh}(X)),\mathcal D(F_*))$
of stable $\infty$-categories.
Here, $\mathrm{Frob}(-,-)$ denotes the $\infty$-category of generalized Frobenius modules
as introduced in arXiv:2410.17102.
This generalizes our result from arXiv:2410.17102,
where we proved the above for regular Noetherian $\mathbb{F}_p$-schemes.
As a byproduct we prove that the derived $\infty$-category of Frobenius (and Cartier) modules
satisfies Zariski descent.