Solovay-model regularity is consistent relative to an inaccessible cardinal

Put $T=\mathrm{Z}\mathrm{F}\mathrm{C}+$“there is an inaccessible cardinal” and let $U$ be the explicitly countable target theory in the Statement. For each external finite $\mathrm{\Delta }\subseteq U$, F1 explicitly supplies a finite source fragment $\mathrm{\Gamma }$ together with a $T$-proof that a suitable countable transitive model of $\mathrm{\Gamma }$ exists and a $T$-proof converting that model into a set model of $\mathrm{\Delta }$. These are exactly the two externally indexed hypotheses of F2. Hence external $\mathrm{Con}(T)$ implies $\mathrm{Con}(U)$. No uniform arithmetic proof-code map is used.

The finite target formulas available in F1 include ZF, DC, universal LM/BP/PSP and failure of AC; F3 supplies the advertised named exclusions in that same target model, so any finite proof using them is covered by the same fragment construction. The inaccessible occurs only in $T$. Thus the displayed one-way consistency implication, and no converse or internal large-cardinal assertion, follows.