SH is not equivalent to CH

Put $T_{mathrmMA}=\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{M}\mathrm{A}+\mathrm{\neg }\mathrm{C}\mathrm{H}$ and $S_0=\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{S}\mathrm{H}+\mathrm{\neg }\mathrm{C}\mathrm{H}$. By [F1], the given consistency hypothesis makes $T_{\mathrm{M}\mathrm{A}}$ externally consistent. Fix the finite $T_{\mathrm{M}\mathrm{A}}$ proof of SH supplied by [F2]. If $S_0$ had a certified finite refutation, replace every occurrence of its added SH axiom by a fresh copy of that fixed proof; its ZFC and $\mathrm{\neg }$CH axiom lines already belong to $T_{\mathrm{M}\mathrm{A}}$. The resulting finite derivation would refute $T_{\mathrm{M}\mathrm{A}}$, contrary to [F1] and [F11]. Hence $S_0$ is consistent. It asserts SH and $\mathrm{\neg }$CH together, so it refutes the implication SH$\to$CH. Zero, one, or repeated SH-axiom occurrences are handled by the same finite splice.

Build the other branch inside the verified $L$-interpretation. By [F4], there are fixed ZF proofs that internally $L$ satisfies ZFC, $V=L$, and AC. Translate [F5] and then [F6] inside $L$ to obtain one fixed certified ZF proof $d_{\mathrm{C}\mathrm{H}}$ of ${\mathrm{C}\mathrm{H}}^L$. Independently, translate [F7] and [F8] inside $L$ and use [F9] to obtain one fixed certified ZF proof $d_{\mathrm{\neg }\mathrm{S}\mathrm{H}}$ of $(\mathrm{\neg }\mathrm{S}\mathrm{H}{)}^L$. These are literal guarded relativizations in the fixed calculus, with capture-free substitutions. Object-level Choice is used inside $L$ by the diamond, tree and tree-to-line suppliers as recorded in [A1]; ambient ZF makes no family choice here.

Let $S_1=\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{C}\mathrm{H}+\mathrm{\neg }\mathrm{S}\mathrm{H}$. Extend the verified dispatcher [F3] by two decidable axiom tags: on the CH tag return the constant block $d_{\mathrm{C}\mathrm{H}}$, and on the $\mathrm{\neg }$SH tag return $d_{\mathrm{\neg }\mathrm{S}\mathrm{H}}$. Retain the existing ZFC branches, capture guards, malformed-input tautology, and the terminal relativized-contradiction block supplied by [F12]. Two finite case branches and two constant certified blocks preserve primitive recursiveness, and PA verifies their line-prefix checker acceptance. Thus PA verifies a total map sending every certified $S_1$ refutation first to a ZF refutation and then, by identical axiom lines, to a ZFC refutation. Zero or repeated occurrences of either added axiom reuse the same dispatcher branches.

Apply [F10] to the map of step 2.1, with source ZFC and target $S_1$. It yields $\mathrm{P}\mathrm{A}⊢\mathrm{Con}(\mathrm{Z}\mathrm{F}\mathrm{C})⟶\mathrm{Con}(S_1),$ and therefore the required external consistency consequence. The theory $S_1$ asserts CH and $\mathrm{\neg }$SH, so it refutes CH$\to$SH. This is a syntactic consistency transfer through $L$, not an extraction of a transitive model from consistency.

By steps 1.1 and 3.1, under external $\mathrm{Con}(\mathrm{Z}\mathrm{F}\mathrm{C})$ there is a consistent extension refuting SH$\to$CH and a consistent extension refuting CH$\to$SH. A certified ZFC proof of either implication would also be a proof in the corresponding extension and, together with that extension's two added axioms, would give a fixed propositional refutation. Hence ZFC proves neither implication and cannot prove SH$\leftrightarrow$CH. The empty or malformed proof-code cases do not witness derivability; each joint theory has both advertised axioms, including CH and SH in opposite truth patterns. No actual generic or set model is inferred. The only Choice uses are already inside the two ZFC branches and internally in $L$; the final proof-code transformations use finite recursion only.