Formal consistency of ZFC plus GCH relative to ZF

Write the fixed target contradiction as $\mathrm{\perp }=\mathrm{\exists }{v}_0\mathrm{\neg }(v_0=v_0)$. In F1's specialized raw $D$-relativization, its guarded $L$-translation is $\mathrm{\top }\to \mathrm{\exists }{v}_0(D(v_0)\wedge \mathrm{\neg }(v_0=v_0))$, where $\mathrm{\top }$ is the fixed empty guard. Let $A(v_0)$ denote the exact fixed translation of the equality atom if a term-graph presentation is used instead; its graph witnesses express that both occurrences of $v_0$ have value $v_0$ and that those values are equal. Under $D(v_0)$, equality reflexivity and existential introduction prove $A(v_0)$, so either presentation admits the same fixed refutation block. Fix once and for all a finite ZF block which proves $\mathrm{\top }$, applies the translated conclusion, derives the negation of its existential matrix from this equality instance and quantified Boolean reasoning, and concludes the selected ZF contradiction by explosion. Such a block exists by F3 and the reflexivity axiom after the fixed formula $D$ and abbreviations are expanded. Define $r(p)$ by appending this block, with shifted line references, to the translator output of F1. List append, addition of the input proof length to finitely many fixed references, and the malformed-input default are primitive recursive. PA checks each of the finitely many new line templates and combines those checks with F1's uniform checker-acceptance proof. Hence PA proves totality and $\mathrm{\forall }p({\mathrm{Prf}}_{\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{G}\mathrm{C}\mathrm{H}}(p,<mi\; mathvariant="normal">⌜</mi>\mathrm{\perp }<mi\; mathvariant="normal">⌝</mi>)\to {\mathrm{Prf}}_{\mathrm{Z}\mathrm{F}}(r(p),<mi\; mathvariant="normal">⌜</mi>\mathrm{\perp }<mi\; mathvariant="normal">⌝</mi>))$. This is one assertion about all proof codes, not an external selection of a new finite fragment after entering PA.

Apply F2 with $T=\mathrm{Z}\mathrm{F}$ and $U=\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{G}\mathrm{C}\mathrm{H}$ to the map $r$. It yields $\mathrm{P}\mathrm{A}⊢\mathrm{Con}(\mathrm{Z}\mathrm{F})⟶\mathrm{Con}(\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{G}\mathrm{C}\mathrm{H})$. Only numerical proof codes occur in this argument. In particular, neither step constructs nor assumes a set model, a well-founded model, or a transitive model of ZF.