Formal consistency transfer by forcing

On input p first check whether it is a certified T-proof with contradictory conclusion, using F3. For a valid such proof scan its finitely many lines, collecting each nonlogical axiom sentence with its certificate and retaining the line references. Denote the finite support by Delta(p); the same derivation is a refutation from that support. This is a bounded loop over the decoded list, using the operations in F3, and is among the B-verified constructors in the hypothesis. On any invalid input use the fixed default output zero.

On a valid refutation input, apply the stipulated total constructors to Delta(p). They return ZFC proofs of existence of a suitable finite-fragment CTM and of its conversion to a nonempty model N of Delta(p), the two proof roles in F1. Concatenate those proofs with renamed variables and corrected references. Append the stipulated soundness-constructor proof for the particular finite derivation p: a model of all its axiom lines satisfies every line by the logical axiom and inference checks, hence satisfies its contradictory final sentence. The nonempty set model N cannot satisfy that sentence, so the combined proof is a ZFC refutation. Denote its code by r(p).

Every operation used in r has a totality and correctness verification in B by the stated hypothesis; composition with the bounded parser and the invalid-input branch therefore gives a total r whose verified property is $\mathrm{\forall }p({\mathrm{Prf}}_T(p,<mi\; mathvariant="normal">⌜</mi>\mathrm{\perp }<mi\; mathvariant="normal">⌝</mi>)\to {\mathrm{Prf}}_{\mathrm{Z}\mathrm{F}\mathrm{C}}(r(p),<mi\; mathvariant="normal">⌜</mi>\mathrm{\perp }<mi\; mathvariant="normal">⌝</mi>))$. This step uses the actual constructor verifications as inputs, rather than inferring them from the external fragment-existence scheme.

Apply F2 to r with source theory ZFC and target theory T. It yields the displayed Con implication in B. All CTMs used in constructing the proof code were confined to their fixed finite source fragments; neither the reduction nor its arithmetic consequence constructs a CTM of full ZFC.