The Blass ultrafilter-free construction is finitely formalizable

Expand the proofs of the finitely many ZF instances in $\mathrm{\Delta }$ and the displayed all-ultrafilters proof recorded at F1. Retain every actually used fixed formula: the Cohen forcing and truth recursions; finite-parameter definition and hereditary-closure formulas; tail automorphisms; ultrafilter and least-partition calculations; the finite-coordinate forcing relation; every fixed instance in the small-forcing restriction and normal ultrapower; the Scott $V=L$ calculation; bounded definition-code satisfaction; and the two $W$-rank inductions. By F5 a formal proof has finite assumption support, so this expansion uses only finitely many Separation, Replacement, Reflection, recursion, satisfaction, and forcing-absoluteness instances. Let $\mathrm{\Sigma }$ be their finite source union, including the finite assertion that the source is constructible.

Enlarge $\mathrm{\Sigma }$ by the finitely many ZFC+GCH instances needed to define $\mathrm{Fn}(\omega \times \omega ,2)$, form its generic extension, and prove the following conditional contradiction used at F1: if the assumed free ultrafilter first produces a nonprincipal $\kappa$-complete ultrafilter in a finite-coordinate extension, then the small-forcing restriction produces one in the ground; its normal ultrapower gives Scott's contradiction to $V=L$. The source fragment contains the finite ultrapower and Łoś derivations under that displayed hypothesis. It contains no measurable-cardinal axiom and does not assert that a normal measure exists outright. Apply F3 to obtain a finite $\mathrm{\Gamma }\subseteq \mathrm{Z}\mathrm{F}$ proving the $L$-relativizations of all those source instances; include the finite proof that the interpretation domain satisfies $V=L$. This does not assert that one finite fragment proves every ZFC theorem: $\mathrm{\Gamma }$ depends externally on the fixed proof expansion in step 1.1.

Use the source-model and generic construction of F2 with enough of ambient ZFC to obtain a countable transitive $C\models \mathrm{\Gamma }$. The external set $M=L^C$ is countable and transitive, and step 2.1 makes it satisfy every retained source instance as well as $V=L$. Enumerate its dense subsets of the Cohen forcing and construct an $M$-generic $G$. The parameter-HOD class defined in $M[G]$ is an external subset of the set $M[G]$, hence is itself a set structure. Every verification retained in step 1.1 is valid over this $M$ and shows that the structure satisfies each member of $\mathrm{\Delta }$, including the assertion that all its ultrafilters are principal. Thus it is a set model of $\mathrm{\Delta }$.

The construction is repeated separately for each externally supplied finite $\mathrm{\Delta }$. If the selected ZF subfragment is empty, the all-ultrafilters sentence and the finite source proof it requires are still retained; duplicate instances do no harm. Ambient AC is used only in F2's reflected countable source and in the explicitly retained source-side cardinal and ultrapower steps, as recorded by F4. The resulting parameter-HOD structure verifies only the selected target formulas and the displayed sentence: no full-ZF set model, uniform satisfaction predicate, or internal quantification over fragments has been inferred.