External relative consistency of the Suslin Hypothesis

Let $p$ be a standard certified ZFC+SH refutation. It has finitely many lines and therefore finitely many occurrences at which the added SH axiom is used; zero occurrences are allowed. All its remaining nonlogical axiom lines are ZFC axioms.

Fix once and for all the finite ZFC+MA+$\mathrm{\neg }$CH derivation $d_{\mathrm{S}\mathrm{H}}$ supplied by [F2]. Scan $p$ in proof order. Copy logical and ZFC-axiom lines and their inference certificates, and replace each SH-axiom line by a fresh variable-renamed copy of $d_{\mathrm{S}\mathrm{H}}$, redirecting later line references to its concluding SH line. Finite recursion on the line number produces a finite certified ZFC+MA+$\mathrm{\neg }$CH derivation with the same final contradiction. If $p$ contains no SH-axiom line, this is just the original ZFC refutation regarded in the stronger theory; a single occurrence receives one copy.

Thus an actual inconsistency of ZFC+SH would give an actual inconsistency of ZFC+MA+$\mathrm{\neg }$CH. By [F1] the latter would give an inconsistency of ZFC. Contraposition proves the displayed external implication.

The first transformation is an explicit standard finite-proof splice, but [F1] promises only an external fixed-fragment assembly. Since no arithmetic base and no base-verified total code map for that second leg have been supplied, [F3] forbids upgrading step 3.1 to an internal PA proof of the consistency implication. Likewise, consistency alone is not a transitive-model existence theorem, so no such model is inferred.