Metatheoretic consistency lower bound for NMSC

Given: The metatheory $\mathrm{Z}\mathrm{F}\mathrm{C}$; the fixed arithmetization of the calculus of The standard certified provability predicate.

$\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{N}\mathrm{M}\mathrm{S}\mathrm{C}$ proves that there is an inner model with a measurable cardinal (NMSC gives an inner model with a measurable cardinal). In the first-order class convention this has the following finite-fragment meaning: for each externally fixed finite set $\mathrm{\Delta }$ of target axioms, one uses a single class-defining formula (with its fixed parameters) for the asserted inner model, and the source theory proves nonemptiness of that class and every ${\sigma }^M$ for $\sigma \in \mathrm{\Delta }$. This is separate relativization for each fixed formula, not quantification over a class truth predicate (Relativization to sets and definable classes).

Every actual derivation is finite. If an actual $U$-refutation uses the finite set $\mathrm{\Delta }$ of nonlogical axioms, apply [F1] only to that $\mathrm{\Delta }$. Relativization to its one nonempty class predicate is an interpretation of the finite theory $\mathrm{\Delta }$ in the source theory, so the finite derivation translates to a source refutation (Interpretation transports derivations and inconsistency, Finite-fragment model transfer proves relative consistency).

This per-refutation, externally selected finite translation proves only the external consistency implication. It does not provide one fixed interpretation of all of $U$, an effective selector of class predicates from proof codes, or a base-verifiable total refutation-code map. Any assertion that an arithmetic base $B$ proves the implication would require exactly such additional uniform data (Formal consistency transfer from a verified reduction).