Fixed finite-fragment verification for the Solovay construction

Expand the finitely many formulas in $\mathrm{\Delta }$ and the particular proofs in F1 that establish them. Retain only the finitely many source axioms, forcing-recursion clauses, relativized-satisfaction formulas, Borel-code inductions, and closure instances that occur in those finite derivations. If $\kappa$ is inaccessible in the ambient source, then it remains inaccessible in $L$: regularity is downward absolute, and an $L$-cofinal map or an $L$-injection $\kappa \to {\mathcal{P}}^L(\lambda )$ for $\lambda <\kappa$ would be the same forbidden map or injection in the ambient universe. Apply F3 to the fixed ZFC+GCH part interpreted in $L$, adjoining the finitely used instances of this direct preservation proof. This produces one finite source family $\mathrm{\Gamma }$, depending on $\mathrm{\Delta }$, together with a finite verification of the F0 construction over any transitive model of $\mathrm{\Gamma }$ containing an inaccessible cardinal.

Work in $\mathrm{Z}\mathrm{F}\mathrm{C}+$“there is an inaccessible cardinal” and choose such a $\kappa$. Apply finite reflection to the formulas of $\mathrm{\Gamma }$ together with the assertion that $\kappa$ is inaccessible, taking a reflected stage above $\kappa$. Then take a countable elementary submodel containing $\kappa$ and collapse it. The result is a countable transitive set model $C$ of $\mathrm{\Gamma }$ in which the collapsed image $\bar{\kappa }$ is inaccessible. The setup in F0 identifies this as the exact parameter required by the retained construction. Only the fixed finite formulas are reflected; no model of the full source theory is claimed.

Enumerate in the ambient source universe the dense subsets, belonging to $C$, of the Lévy collapse computed in the constructible ground of $C$, and recursively build a generic filter. Execute inside the resulting set extension the fixed construction retained at step 1.1. Because $C$ and its extension are sets, the retained F1 derivations from step 1.1 show that the hereditary definability predicate cuts out a set structure satisfying every sentence in $\mathrm{\Delta }$. Thus $T$ proves both required assertions: the countable transitive source model $C$ exists, and the displayed construction converts it into a set model of $\mathrm{\Delta }$.

The argument is indexed externally by the fixed finite $\mathrm{\Delta }$. An empty $\mathrm{\Delta }$ is handled by any nonempty reflected structure. Nothing selects all such proofs inside arithmetic, constructs a model of full ZFC from consistency, or establishes a primitive-recursive all-proof transformer.