Conjectured characterizations and reductions of intuitionistic provability logics of arithmetic

Let ${\sf HA}$ and ${\sf PA}$ denote Heyting and Peano arithmetic, respectively, let $\mathbb{N}$ be the standard natural numbers, and let $\mathcal{PL}(T,U)$ and $\mathcal{PL}_{\Sigma_1}(T,U)$ denote the provability logics of $U$ with respect to $T$, using arbitrary and $\Sigma_1$ substitutions, respectively. Write ${\sf iH}$ for the intuitionistic provability logic of ${\sf HA}$, ${\sf iH}^{*}$ for the logic defined in the cited work, ${\sf iH\underline{P}}$ for ${\sf iH}$ extended by $\underline{\sf P}$, and ${\sf iH\underline{SP}}$ for ${\sf iH}$ extended by $\underline{\sf S}$ and $\underline{\sf P}$. The notations ${\sf iH_\sigma}$, ${\sf iH_\sigma\underline{P}}$, ${\sf iH_\sigma\underline{SP}}$, and ${\sf iH_\sigma^{*\!*}}$ are the corresponding $\Sigma_1$-substitution logics.

Characterizations and reductions conjecture. The following characterizations and reductions hold:

$${\sf iH}=\mathcal{PL}({\sf HA},{\sf HA})\leq\mathcal{PL}_{\Sigma_1}({\sf HA},{\sf HA})={\sf iH_\sigma}.$$ $${\sf iH}=\mathcal{PL}({\sf HA},{\sf HA})\leq\mathcal{PL}({\sf HA},\mathbb{N})={\sf iH\underline{SP}}.$$ $${\sf iH\underline{P}}=\mathcal{PL}({\sf HA},{\sf PA})\leq\mathcal{PL}_{\Sigma_1}({\sf HA},{\sf PA})={\sf iH_\sigma\underline{P}}.$$ $${\sf iH\underline{SP}}=\mathcal{PL}({\sf HA},\mathbb{N})\leq\mathcal{PL}_{\Sigma_1}({\sf HA},\mathbb{N})={\sf iH_\sigma\underline{SP}}.$$ $${\sf iH}^{*}=\mathcal{PL}({\sf HA}^{*},{\sf HA}^{*})\leq\mathcal{PL}_{\Sigma_1}({\sf HA}^{*},{\sf HA}^{*})={\sf iH}_\sigma^{*\!*}.$$

Moreover, all these reductions are computable, and consequently all the provability logics are decidable.