Two distinct outputs of a consistency construction

A semantic theorem $\mathrm{CTM}(T)\to \mathrm{CTM}(U)$ and a formal theorem $B⊢\mathrm{Con}(T)\to \mathrm{Con}(U)$ have different premises and conclusions.

Use Transitive models and finite-fragment transfer data to specify actual membership and external countability. A later model construction must identify its finite target fragment, source fragment, auxiliary hypotheses and proof of source-model existence when applying Finite-fragment model transfer proves relative consistency. An internal consistency implication also needs the verified total proof-code reduction in Formal consistency transfer from a verified reduction. The obstruction in The transitive-model consistency-strength gap prevents replacing a transitive-model hypothesis by bare consistency. These are proved interfaces and methodological instructions, not a new unproved consistency claim.