Formal consistency of PFA from a supercompact

Apply F2 with arithmetic base PA, source theory $T_0=S$, target theory $U=T$, and reduction $R$ from F1. Its verified premise has the required orientation: a proof of contradiction in ZFC+PFA is sent to a proof of contradiction in ZFC plus a supercompact. Therefore PA proves $\mathrm{Con}(S)⟶\mathrm{Con}(T)\mathrm{.}$

Equivalently, inside PA assume $\mathrm{Con}(S)$ and let $p$ be arbitrary. If $p$ were a certified $T$-refutation, F1 would make $R(p)$ a certified $S$-refutation, contradicting the assumption. Universal generalization over $p$ gives $\mathrm{Con}(T)$. This spells out both quantifiers and confirms that no converse implication is being used.

On standard natural numbers the formal implication gives the corresponding external relative-consistency consequence. F1 constructs only finite proof codes, and F2 explicitly requires no model extraction. Hence neither step produces a generic extension or a countable transitive model from the bare consistency hypothesis.