 Solution

Let $\perp$ abbreviate the fixed false arithmetic equality, and fix an actual proof of $\neg \perp$ with code $m$. For a proposed proof code $y\ge m$, that known proof of the negation already violates the bounded negative-proof test in $R(┌\perp ┐)$.

For the finitely many codes $y<m$, either one is an actual proof of $\perp$, in which case Peano arithmetic is inconsistent and proves the requested conclusion by explosion, or none is. In the latter case the finitely many true bounded facts $\neg \mathrm{Prf}(┌\perp ┐,\overline{y})$ are all provable by bounded completeness. Their conjunction excludes every code below $m$. The positive bounded fact that $m$ proves $\neg \perp$ is likewise provable. Splitting $y<m$ and $y\ge m$ inside arithmetic now givesThus the consistency statement for this Rosser provability predicate is provable. The argument uses only a fixed finite initial segment of proof codes; it does not prove the usual unbounded consistency statement.