 Strict Gödel-to-Rosser implication

For the standard Gödel sentence and Rosser sentence, the formalized Rosser unprovability theorem and $G\leftrightarrow \mathrm{Con}(T)$ yield $T⊢G\to R$. If $T+\mathrm{Con}(T)$ is consistent, the converse is unprovable under the usual formalized incompleteness hypotheses. A proof of $R\to G$ would give $\square \neg G\to \square \neg R$. Formalized negative unprovability identifies $\neg \square \neg R$ with $\mathrm{Con}(T)$ and $\neg \square \neg G$ with $\mathrm{Con}(T+\mathrm{Con}(T))$. The strengthened theory would then prove its own consistency, contradicting the Gödel second incompleteness theorem. The consistency assumption belongs to this strictness conclusion.