Fixed finite-fragment verification for the MA iteration

Fix the actual ZFC axiom and MA instances in $\mathrm{\Delta }$. Expand the finite-support iteration proof F3 for those formulas. Its ccc induction, size and bounded-stage capture calculations, bookkeeping argument, and Cohen-coordinate argument use only finitely many ZFC schema instances and the GCH cardinal arithmetic needed at the relevant cardinals. Collect these in a finite source support. The iteration and its forcing relation are set definitions in that support; AC is used in the ccc, cardinal and bookkeeping choices.

Apply F1 to the fixed GCH part of that support. Add its finitely many $L$-relativized certificates and the source instances required to construct the $L$ model. Enlarge the resulting finite $\mathrm{\Gamma }$ to cover the forcing theorem and the finite target formulas. F2 gives a countable transitive source model of $\mathrm{\Gamma }$; its constructible inner model has the particular source GCH instances, and the generic iteration over that model satisfies each member of $\mathrm{\Delta }$ by F3. These are ZFC-formalizable fixed-fragment steps, so ZFC proves the existence of the resulting set model of $\mathrm{\Delta }$.

The argument chooses a finite proof separately for the actual $\mathrm{\Delta }$. A semantic schedule for all MA instances does not by itself verify a numerical proof constructor or its PA checker invariant.