Formal relative consistency of not SH

By [F2], ZF has fixed derivations saying internally that $L$ satisfies ZFC and $V=L$. Translate the fixed ZF proof [F3] into $L$: internal $V=L$ yields a normal splitting Suslin tree. Since $L$ satisfies AC, translate the fixed ZFC proof [F4] there to obtain a strong-convention Suslin line. By [F5] this conclusion is exactly $(\mathrm{\neg }\mathrm{S}\mathrm{H}{)}^L$. Concatenating the finitely many fixed derivations, with capture-free substitutions and the interpretation's domain guards, gives one fixed certified ZF proof $d_{\mathrm{\neg }\mathrm{S}\mathrm{H}}$ of the literal $L$-relativization. Ambient Choice is not used; [A1] holds internally in $L$.

Extend the axiom-certificate dispatcher of [F1]. On every certified ZFC axiom use its existing branch; a GCH certificate branch may remain available but is never required by the target theory. On the one new literal $\mathrm{\neg }$SH tag, return the constant proof $d_{\mathrm{\neg }\mathrm{S}\mathrm{H}}$ from step 1.1. On malformed input retain the dispatcher's fixed tautology output. Adding one decidable tag and one constant finite proof block preserves primitive recursiveness, and PA verifies the new branch's checker acceptance by the same finite line-prefix verification used for the old constant branches.

Feed any certified ZFC+$\mathrm{\neg }$SH derivation through the extended dispatcher and the guarded $L$-translation from [F1]. Logical lines are translated structurally; ZFC axiom lines use the old branches; every $\mathrm{\neg }$SH axiom line uses step 2.1. A translated source contradiction is converted by the interpretation's fixed contradiction block to the chosen ZF contradiction. Regard the resulting ZF proof also as a ZFC proof. Thus PA verifies a total primitive-recursive map $r$ satisfying ${\mathrm{Prf}}_{\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{\neg }\mathrm{S}\mathrm{H}}(p,<mi\; mathvariant="normal">⌜</mi>\mathrm{\perp }<mi\; mathvariant="normal">⌝</mi>)⟶{\mathrm{Prf}}_{\mathrm{Z}\mathrm{F}\mathrm{C}}(r(p),<mi\; mathvariant="normal">⌜</mi>\mathrm{\perp }<mi\; mathvariant="normal">⌝</mi>)\mathrm{.}$ The zero-occurrence case uses only the old dispatcher, and repeated $\mathrm{\neg }$SH occurrences reuse the same constant block.

Apply [F6] in PA to the verified map of step 3.1, with source theory ZFC and target theory ZFC+$\mathrm{\neg }$SH in the consistency direction. This gives the displayed formal implication; its truth on standard proof codes yields the external relative-consistency consequence.

This proof constructs a syntactic reduction only. Neither [F2] nor the consistency implication supplies a transitive set model of ZFC. All object-level Choice occurs inside $L$ at step 1.1; the proof-code dispatcher and its PA verification make no choice from a family of sets.