Equivalence of a Gödel sentence and a consistency statement ($T⊢G\leftrightarrow \mathrm{Con}(T)$)

For a Gödel sentence $G\leftrightarrow \neg \square G$ with the Hilbert-Bernays-Löb derivability conditions, fix a refutable contradiction sentence $\perp$. Since $\perp \to G$ is provable, $\square \perp \to \square G$, giving $G\to \neg \square \perp$. For the reverse direction, $\square G$ implies both $\square \square G$ and $\square \neg \square G$, hence $\square \perp$. Contraposition gives $\neg \square \perp \to \neg \square G\to G$. This is an internal equivalence of sentences, not a rule asserting the theory's own consistency.