Every real set in the Shelah inner model has the Baire property

First let $A\subseteq 2^{\omega }$ belong to $N$. By [F1], $A$ has a rank-bounded definition from one parameter $s\in S$ and finitely many ordinals. Applying [F2] to that exact defining formula gives a Borel code $c$ and a coded meagre set $E_0$ in the ambient extension with $A\mathrm{△}{C}_c\subseteq E_0$. This uses the claim as written; no open set is read directly from the Borel representative.

This proves the all-Baire-property assertion for the standard set-theoretic real space $2^{\omega }$. To compare with the usual real line, let $D\subseteq 2^{\omega }$ be the infinitely-many-$1$s subspace of [F6]. Its complement is explicitly at most countable and hence meagre; likewise $\mathbb{Q}$ is countable and meagre in $\mathbb{R}$. Composing the two homeomorphisms in [F6] gives $h:D⟶\mathbb{R}\setminus \mathbb{Q}\mathrm{.}$

Apply only the uniform construction clause of [F5] to $c$. It yields an open code $u$ and a coded sequence of closed nowhere-dense sets covering $C_c\mathrm{△}{U}_u$. Pair the Borel/open code and both meagre-error sequences into finitely many binary reals. By [F3], every such code real belongs to $N$.

We verify the needed absoluteness directly, rather than use the Solovay-intermediate-model clause of [F5]. A code from [F7] is a labelled tree on ${\omega }^{<\omega }$ and hence a real. If its child relation were ill-founded in either of the two transitive same-real models, DC in $N$ (and Choice in the ambient extension) would produce a descending sequence of nodes, itself a real; therefore well-foundedness agrees. For a shared real $x$, if the two evaluations first differed at a node, an $R$-minimal such node would have agreeing child evaluations, and the leaf, complement and union rules would force agreement at that node, a contradiction. Thus $C_c$ and $U_u$ have identical evaluations on the common reals. For a binary tree code, closedness is immediate and nowhere density is the arithmetic finite-cylinder test: every finite word has an extension above which some finite level has no tree node. That test is absolute, so every displayed closed-nowhere-dense code remains such in $N$.

Membership in $A\in N$ is absolute between the transitive model $N$ and the ambient extension. Hence the ambient inclusions from steps 1.1 and 2.1, together with step 3.1, give $N\models A\mathrm{△}{U}_u\subseteq E_0\cup E_c\mathrm{.}$ Dependent Choice in [F3] supplies Countable Choice, and the two actual coded sequences of nowhere-dense sets therefore witness in $N$ that the right side is meagre.

Let $A\subseteq \mathbb{R}$ belong to $N$. The coded set $A^{\ast }=h^{-1}[A\cap (\mathbb{R}\setminus \mathbb{Q})]\subseteq D$, viewed as a subset of $2^{\omega }$ by putting no points outside $D$, belongs to $N$. Step 4.1 gives $A^{\ast }\mathrm{△}U$ meagre in $2^{\omega }$. Restrict to the dense subspace $D$ and transport by $h$: the image differs from the relatively open set $h[U\cap D]$ by a meagre subset of $\mathbb{R}\setminus \mathbb{Q}$. A nowhere-dense subset of a dense subspace is nowhere dense in the whole space after taking ambient closure, so that error is meagre in $\mathbb{R}$. Write the relatively open image as $W\cap (\mathbb{R}\setminus \mathbb{Q})$ for an open $W\subseteq \mathbb{R}$. Adding the countable rational set shows $A\mathrm{△}W$ is meagre in $\mathbb{R}$. All maps, countable complements and codes used here are the fixed objects of [F6] and belong to $N$.

Since $A$ was arbitrary, steps 4.1 and 5.1 prove the assertion for both the set-theoretic and usual-real conventions, with witnesses in $N$. This is the Statement.