The exact equiconsistency of ZFC and the all-Baire-property model

Given: Fixed arithmetizations of the three theories and of ZFC as in the formal-consistency items.

Formal consistency of ZFC plus GCH relative to ZF: a verified proof transformation gives $\mathrm{Con}(\mathrm{Z}\mathrm{F})\to \mathrm{Con}(\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{G}\mathrm{C}\mathrm{H})$, without a transitive model assumption.

Shelah's CH-length homogeneous sweet construction: under ZFC+CH there is a CH-length sweet construction whose final algebra is ccc and has the stated homogeneity, free-amalgamation and $\mathrm{U}\mathrm{M}$-quotient properties. This interface supplies that mathematical construction, not a uniform formal forcing verification.

Shelah's numbered conclusion cited in the source block states exactly that ZFC, ZFC plus the real-and-ordinal-definable Baire-property assertion, and ZF+DC plus universal Baire property are equiconsistent. Its proof remark supplies both forward models: Theorem 7.16 gives the definable-set Baire property in the full forcing extension, while $HOD(S)$ gives the ZF+DC model with universal Baire property. It invokes Gödel's $L$ for the reverse implications. This item uses that published equiconsistency theorem directly; it does not infer a proof-code compiler from [F2].

The Shelah inner model satisfies ZF and Dependent Choice with Every real set in the Shelah inner model has the Baire property: inside the extension, $N$ satisfies ZF+DC and every set of reals in $N$ has the Baire property. This interface supplies only the inner model; it is not used to transfer Baire-property witnesses or arbitrary definable sets upward to the full extension.

Semantic and formal inner-model theorem for L with The constructible universe satisfies AC: for every model of any of the three theories, its constructible universe satisfies ZFC internally.