Real names are captured and coded meagre unions are absorbed

Capture of reals: let $\dot{x}$ be a $B$-name for a real. For each $n<\omega$, [F3] makes the set of conditions deciding the value of $\dot{x}(n)$ dense; use Choice to take a maximal antichain $A_n$ in that dense set, labelled by the decided value $0$ or $1$. Each $A_n$ is countable by the ccc in [F1]. Thus $A={\bigcup }_{n<\omega }{A}_n$ is countable, and the set of stages in which its members occur is countable and bounded by some $\alpha <{\omega }_1$ by [F4]. Since $B_{\alpha }$ is complete in $B$, every $A_n$ remains maximal in $B_{\alpha }$. The labelled antichains therefore define a $B_{\alpha }$-name ${\dot{x}}_{\alpha }$; for every generic $G$, the unique member of $A_n\cap G$ gives both ${\dot{x}}_G(n)$ and $({\dot{x}}_{\alpha }{)}_{G\cap B_{\alpha }}(n)$, so the two names have the same value coordinatewise. Hence every real name is equivalent to a $B_{\alpha }$-name.

Capture of countable ordinal sequences and Borel codes: for a name forced to be a function from $\omega$ to the ordinals, apply [F3] to each coordinate and choose a maximal antichain every member of which decides that coordinate as a check ordinal. The forcing theorem guarantees that this deciding set is dense; no upper bound on the decided ordinals is assumed in advance. The union of the antichains is countable by [F1] and Choice, so [F4] bounds the birth stages of all its Boolean conditions below one $\alpha$. The ordinal labels are ground objects and may be used unchanged in the resulting $B_{\alpha }$-name. A Borel-code name is a name for a hereditarily countable code; decide the entries of a fixed real/ordinal coding in the same way.

Suppose now that the ground is $L$. The original name $\dot{s}$ is a ground set, and [F6] assigns it an ordinal code. For every coordinate choose the ${<}_L$-least maximal deciding antichain and its ${<}_L$-least enumeration $⟨a_{n,k}:k<\omega ⟩$ (padding a finite antichain). The entire sequence of labelled enumerations is a constructible set and therefore has one further ordinal code. The generic meets exactly one $a_{n,k}$ for each $n$; encode the resulting sequence of indices $k(n)$ by one real $r$. From $r$ and the two ordinal codes, the canonical $L$ well-order reconstructs the name, every labelled antichain, and hence every value $s(n)$. Thus $s$ is definable from one real and finitely many ordinals. This argument uses the complete stage embeddings to locate the antichains; it does not claim that an ultrafilter on an arbitrary countably generated complete algebra is generated by algebra generators.

Absorption at a later UM quotient: let $\alpha$ capture $s$, so $s\in V[G\cap B_{\alpha }]$. Choose $\beta \ge \alpha$ for which the next quotient has the canonical UM presentation from [F1]. Then every closed nowhere-dense code in $V[s]\subseteq V[G\cap B_{\beta }]$ is old for that exact UM forcing. By [F5], their union is contained in one meagre $F_{\sigma }$ envelope coded by the quotient generic. Every meagre Borel code includes a countable closed-nowhere-dense cover, so the same envelope contains the union of all meagre Borel sets coded in $V[s]$. No transport of absorption through bare forcing equivalence is invoked.

The steps above prove the capture clauses and the absorption clause, and step 3.1 gives the constructible real-and-ordinal presentation; this is the Statement.