[Improved version!!]
Suppose $\mathsf{Prov}_R$ is a Rosserized proof predicate for PA (or some other suitable theory). To fix ideas, suppose
$$\mathsf{Prov}_R(\overline{\ulcorner\varphi\urcorner}) = \mathsf{\exists x(Prf(x, \overline{\ulcorner\varphi\urcorner}) \land (\forall y \leq x)\neg Prf(y, \overline{\ulcorner\bot\urcorner}))}$$
where $\mathsf{Prf}$ represents the relation that $m$ has to $n$ when $m$ numbers a proof of the sentence numbered $n$. We can construct a $\Delta_0$ wff $\mathsf{Prf}$, making $\mathsf{Prov}_R$ $\Sigma_1$.
Then, as is familiar,
PA $\vdash \neg\mathsf{Prov}_R(\overline{\ulcorner\bot\urcorner})$
So the HBL derivability conditions can't all hold for $\mathsf{Prov}_R$.
The first condition still holds. And it is reasonably easy to see why the second condition might fail (suppose that ordered by Gödel numbers the proof of $A$ and $A \to C$ precede the first proof of $\bot$ which precedes the first proof of $C$). But we also know that using Jereslow's trick we can get a version of the unprovability of consistency without appeal to the second condition, so the third condition should be the crucial failure.
Well the usual proof of the third condition runs by showing PA $\vdash \psi \to \mathsf{Prov}(\overline{\ulcorner\psi\urcorner})$ for any $\Sigma_1$ $\psi$, and then remarking that $\mathsf{Prov}(\overline{\ulcorner\varphi\urcorner})$ is itself $\Sigma_1$. But this line of argument is presumably going to be blocked at the first stage when we turn to the Rosserized predicate $\mathsf{Prov}_R$: i.e. we won't have PA $\vdash \psi \to \mathsf{Prov}_R(\overline{\ulcorner\psi\urcorner})$ for every $\Sigma_1$ $\psi$. [And it is plausible this should fail, I guess.]
So we know the third condition fails. But -- and here at last is the questions:
Is there a simple counterexample to PA $\vdash \psi \to \mathsf{Prov}_R(\overline{\ulcorner\psi\urcorner})$ for $\Sigma_1$ $\psi$,
and if that counterexample doesn't already involve $\mathsf{Prov}_R$,
Are there known constructions of suitable wffs $\theta$ such that we have a nice illustration of a case where PA $\nvdash \mathsf{Prov}_R(\overline{\ulcorner\theta\urcorner}) \to \mathsf{Prov}_R(\overline{\ulcorner\mathsf{Prov}_R(\overline{\ulcorner\theta\urcorner})\urcorner})$
either for the given Rosserized predicate, or some cousin?
