Proof. Run the usual coiteration by least disagreement, producing trees \(\mathcal{T}\) on \(\mathcal{M}\) and \(\mathcal{U}\) on \(\mathcal{N}\). The \(\mathcal{M}\)-side is governed by the strategy inherited from \(M_1\). The \(\mathcal{N}\)-side is governed by the winning strategy witnessing \(\Pi^1_2\)-iterability.

There is no new issue at successor stages. Consider a countable limit stage and suppose first that both sides have reached the same comparison height, so that \(\delta(\mathcal{T})=\delta(\mathcal{U})\). Let \(b\) be the branch selected on the \(\mathcal{M}\)-side. Since \(\mathcal{M}\triangleleft M_1\) and \(M_1\) is \(1\)-small below its Woodin, the branch model \(\mathcal{M}_b^{\mathcal{T}}\) has a \(\mathcal{Q}\)-structure witnessing the relevant failure of Woodinness at this common \(\delta\). Write this \(\mathcal{Q}\)-structure as \(L_\alpha(\mathcal{M}(\mathcal{T}))\), using the standard coding of the common part.

Apply the \(\Pi^1_2\)-iterability of \(\mathcal{N}\) to the tree \(\mathcal{U}\) with ordinal parameter \(\alpha\). Player II supplies a maximal \(\alpha\)-good branch \(c\). Because the two sides of the comparison agree below the common \(\delta\), the initial segment \(L_\alpha(\mathcal{M}(\mathcal{T}))\) is also the corresponding \(\mathcal{Q}\)-structure for \(c\) on the \(\mathcal{N}\)-side, provided the branch model is well-founded past that structure. If there were a second sufficiently good cofinal branch through \(\mathcal{U}\), then the zipper lemma, applied with a code for the common \(\mathcal{Q}\)-structure as parameter \(A\), would produce strength below \(\delta(\mathcal{U})\). This contradicts the witness to the failure of Woodinness coded by the \(\mathcal{Q}\)-structure. Hence the good branch through \(\mathcal{U}\) is unique, and it is fully well-founded.

If one side has stopped using extenders, the same argument applies with the last model on the stopped side replacing the common branch model. Its relevant initial segment supplies the \(\mathcal{Q}\)-structure which witnesses that the remaining comparison height is not Woodin, and therefore determines the unique well-founded branch on the other side.

It remains to rule out a comparison of length \(\omega_1\). Suppose that such a putative comparison existed. Force with the Lévy collapse \(\operatorname{Col}(\omega,\omega_1)\) over the ambient model. In the collapse extension, the putative tree becomes countable, and \(\Pi^1_2\)-iterability is preserved. Thus there is a branch supplied by the \(\Pi^1_2\) strategy. By the uniqueness just proved, this branch is ordinal definable from the ground-model data of the comparison. Homogeneity of the collapse therefore puts the branch back in the ground model, contradicting the assumption that the comparison had no branch at stage \(\omega_1\).

Thus the comparison terminates below \(\omega_1\). The terminal models are linearly ordered by initial segment. Since both premice are \(\omega\)-sound and project to \(\omega\), the usual no-drop argument for the shorter side pulls the conclusion back to the original premice. Hence \(\mathcal{M}\trianglelefteq\mathcal{N}\) or \(\mathcal{N}\trianglelefteq\mathcal{M}\). ◻

Proof. The clauses saying that a real codes a countable ordinary premouse, that the premouse is \(1\)-small, that it is \(\omega\)-sound, and that \(\rho_\omega=\omega\) are arithmetic, after fixing the usual coding of countable premice by reals. By Steel’s analysis of the weak iteration games, \(\Pi^1_2\)-iterability is a \(\Pi^1_2\) condition in the code. Hence the displayed definition of \(\mathcal{I}\) is \(\Pi^1_2\).

We next show that no nonstandard premouse enters \(\mathcal{I}\). Work in \(M_1[G]\) and let \(\mathcal{N}\in\mathcal{I}\). Since \(\omega_1\) is preserved, \(\mathcal{N}\) has countable height below the true \(\omega_1^{M_1}\). Choose \(\eta<\omega_1\) such that \(\operatorname{Ord}^{\mathcal{N}}<\eta\) and such that \(\mathcal{J}_\eta^{M_1}\) is \(\omega\)-sound and projects to \(\omega\). The initial segment \(\mathcal{J}_\eta^{M_1}\) is an ordinary premouse and is realizable inside \(M_1\); hence it is \(\Pi^1_2\)-iterable in the present extension by Paragraph 2.1.0.1. Applying Lemma 1 to \(\mathcal{J}_\eta^{M_1}\) and \(\mathcal{N}\), the alternative \(\mathcal{J}_\eta^{M_1}\triangleleft\mathcal{N}\) is impossible by the choice of \(\eta\). Therefore \(\mathcal{N}\trianglelefteq\mathcal{J}_\eta^{M_1}\), so \(\mathcal{N}\) is itself an initial segment of \(M_1\).

Finally, the fine structure of \(M_1\) gives cofinally many \(\eta<\omega_1\) such that \(\mathcal{J}_\eta^{M_1}\) is \(\omega\)-sound and projects to \(\omega\). These levels are ordinary premice, \(1\)-small, and realizable, hence \(\Pi^1_2\)-iterable in the present extension by the same preservation convention. Therefore they belong to \(\mathcal{I}\), proving cofinality. ◻

Proof. By Lemma 2, every member of \(\mathcal{I}\) is an initial segment \(\mathcal{J}^{M_1}_\eta\) with \(\eta<\omega_1\). Hence the union in Definition 3 is contained in \(M_1|\omega_1\). Conversely, the same lemma gives cofinally many \(\eta<\omega_1\) with \(\mathcal{J}_\eta^{M_1}\in\mathcal{I}\). Their union is \(\mathcal{J}^{M_1}_{\omega_1}\). The same formula defining \(\mathcal{I}\) is used in every such extension. We do not assert that the same real codes belong to \(\mathcal{I}\) in different extensions, since new reals may code new countable putative iteration trees. Rather, applying Lemma 2 inside the given extension identifies the union of the premice satisfying that formula with the true \(\mathcal{J}^{M_1}_{\omega_1}\). ◻

Proof. This is the standard condensation theorem for the Steel \(M_1\)-construction; see [2]. We only spell out why the ultrapower alternative does not occur in the present application. The hulls below are chosen so that their collapse has projectum equal to its internal \(\omega_1\). If the second alternative held, there would be an extender on the \(M_1\)-sequence indexed exactly at this internal \(\omega_1\). The lower part below that index is the collapse of the corresponding lower part of the hull and sees the index as the successor cut reached by the construction. An extender indexed there would make the index inaccessible in the relevant extender model. This contradicts the fact that the collapsed lower part computes it as its \(\omega_1\). Therefore only the initial-segment alternative remains. ◻

Proof. Work in \(M_1\). Use the canonical well-order \(<_{M_1}\) of the construction to define \(\vec{D}\) recursively. At a limit ordinal \(\alpha<\omega_1\), suppose \(\langle D_\beta\mid\beta<\alpha\rangle\) has been defined. If there is a pair \((A,C)\) such that \(A\subseteq\alpha\), \(C\subseteq\alpha\) is club in \(\alpha\), and \[\forall\beta\in C\, (D_\beta\neq A\cap\beta),\] then let \((A_\alpha,C_\alpha)\) be the \(<_{M_1}\)-least such pair and set \(D_\alpha=A_\alpha\). If there is no such pair, set \(D_\alpha=\emptyset\). At successor stages we may again set \(D_\alpha=\emptyset\).

The recursion is carried out over \(M_1|\omega_1\). Indeed, all objects considered at stage \(\alpha\) are subsets of the countable ordinal \(\alpha\) in \(M_1\), and the order used to choose the least pair is the restriction of the canonical \(M_1\) construction order. Hence the resulting sequence is uniformly definable over \(M_1|\omega_1\).

It remains to verify that \(\vec{D}\) is a diamond sequence. Suppose not. Let \((A,C)\) be the \(<_{M_1}\)-least counterexample, so \(A\subseteq\omega_1\), \(C\subseteq\omega_1\) is club, and \[\forall\alpha\in C\,(D_\alpha\neq A\cap\alpha).\] Choose an \(\omega\)-sound initial segment \(\mathcal{J}^{M_1}_\theta\) containing \(A\), \(C\), and the sequence \(\vec{D}\), and then take a countable elementary substructure \[X\prec \mathcal{J}^{M_1}_\theta\] with \(A,C,\vec{D}\in X\) and with \(\alpha=X\cap\omega_1\in C\). Let \[\pi:\bar X\rightarrow X\] be the inverse of the transitive collapse. By Theorem 3, \(\bar X\) is an initial segment of \(M_1\). Consequently the recursive construction of \(\vec{D}\) inside \(\bar X\) is exactly the initial part \[\langle D_\beta\mid\beta<\alpha\rangle.\] Moreover the collapse sends \(A\) to \(A\cap\alpha\) and \(C\) to \(C\cap\alpha\), and by elementarity \(\bar X\) sees \((A\cap\alpha,C\cap\alpha)\) as the \(<_{M_1}\)-least witness that the previous sequence is not diamond on \(\alpha\). Therefore the recursion at stage \(\alpha\) gives \[D_\alpha=A\cap\alpha.\] Since \(\alpha\in C\), this contradicts the choice of \((A,C)\). Thus no counterexample exists, and \(\vec{D}\) is a \(\diamondsuit_{\omega_1}\)-sequence in \(M_1\). ◻

Proof. This is the \(\eta=0\) instance of Steel’s comparison theorem for \(n\)-small \(\Pi_n\)-iterable mice. Since \(\mathcal{M}\triangleleft M_n\), the premouse \(\mathcal{M}\) is realizable in the background construction of \(M_n\). Since \(\mathcal{N}\) is \(n\)-small and \(\Pi_n\)-iterable, the \(\mathcal{N}\)-side has exactly the amount of iterability required by Steel’s comparison lemma. Because both premice are ordinary premice in the parameter-free sense fixed above, the lower parts agree trivially.

The proof is the usual least-disagreement coiteration. The \(\mathcal{M}\)-side uses the realization strategy inherited from the construction of \(M_n\), while the \(\mathcal{N}\)-side uses the \(\Pi_n\)-iterability strategy. At limit stages, the good branch is characterized by the corresponding \(\mathcal{Q}\)-structure: for \(n=1\) this is the branch uniqueness argument described in Subsection 2.1, and for \(n>1\) the assertion is proved by induction on \(n\), because the \(\mathcal{Q}\)-structure appearing at a limit stage is \((n-1)\)-small and \(\Pi_{n-1}\)-iterable above the new cutpoint. If two distinct good branches were available, Steel’s zipper argument would produce the forbidden strength below the comparison height, contradicting \(n\)-smallness at the relevant level. Thus the comparison has well-founded branches and reaches terminal models which are linearly ordered by initial segment.

Finally, since both premice are \(\omega\)-sound and project to \(\omega\), the standard no-drop pullback argument gives the initial-segment relation already between the original premice. Hence \(\mathcal{M}\trianglelefteq\mathcal{N}\) or \(\mathcal{N}\trianglelefteq\mathcal{M}\). ◻

Proof. The clauses saying that a real codes a countable passive ordinary premouse, that the premouse is lower-part, \(n\)-small, \(\omega\)-sound, and satisfies \(\rho_\omega=\omega\), are arithmetic in the usual code for countable premice. By Fact 4, the \(\Pi_n\)-iterability clause is \(\boldsymbol{\Pi}^1_{n+1}\). Therefore \(\mathcal{I}_n\) is \(\boldsymbol{\Pi}^1_{n+1}\) in the codes.

We next prove that no nonstandard lower-part premouse enters \(\mathcal{I}_n\). Work in \(M_n[G]\) and let \(\mathcal{N}\in\mathcal{I}_n\). Since \(\omega_1\) is preserved, the height of \(\mathcal{N}\) is below the true \(\omega_1^{M_n}\). Choose \(\eta<\omega_1\) such that \(\operatorname{Ord}^{\mathcal{N}}<\eta\) and such that \(\mathcal{J}^{M_n}_\eta\) is passive, lower-part, \(\omega\)-sound, and projects to \(\omega\). The fine structure of \(M_n\) gives cofinally many such \(\eta\). The initial segment \(\mathcal{J}^{M_n}_\eta\) is realizable inside \(M_n\), and hence is \(\Pi_n\)-iterable in the present extension by the preservation convention.

Apply Lemma 5 to \(\mathcal{J}^{M_n}_\eta\) and \(\mathcal{N}\). The alternative \(\mathcal{J}^{M_n}_\eta\trianglelefteq\mathcal{N}\) is impossible by the choice of \(\eta\), because \(\operatorname{Ord}^{\mathcal{N}}<\eta\). Therefore \[\mathcal{N}\trianglelefteq \mathcal{J}^{M_n}_\eta,\] and hence \(\mathcal{N}\) is itself an initial segment of \(M_n\).

Conversely, let \(\eta<\omega_1\) be such that \(\mathcal{J}^{M_n}_\eta\) is passive, lower-part, \(\omega\)-sound, and projects to \(\omega\). Then \(\mathcal{J}^{M_n}_\eta\) is \(n\)-small and realizable in the Steel construction of \(M_n\), and by the preservation convention it is \(\Pi_n\)-iterable in \(M_n[G]\). Thus \(\mathcal{J}^{M_n}_\eta\in\mathcal{I}_n\). Since such \(\eta\) are cofinal in \(\omega_1\), the cofinality assertion follows. ◻

Proof. By Lemma 6, every member of \(\mathcal{I}_n\) is an initial segment \(\mathcal{J}^{M_n}_\eta\) with \(\eta<\omega_1\). Hence the union in Definition 7 is contained in \(M_n|\omega_1\). Conversely, the same lemma gives cofinally many \(\eta<\omega_1\) with \(\mathcal{J}^{M_n}_\eta\in\mathcal{I}_n\). The union of these initial segments is \(\mathcal{J}^{M_n}_{\omega_1}\).

The same formula defining \(\mathcal{I}_n\) is used in every relevant extension. We do not assert that the same real codes belong to \(\mathcal{I}_n\) in different extensions, since new reals may code new countable putative iteration trees. Rather, applying Lemma 6 inside the given extension identifies the union of the premice satisfying the formula with the true \(\mathcal{J}^{M_n}_{\omega_1}\). ◻

Proof. This is the condensation theorem for initial segments of the Steel \(M_n\)-construction. The proof is the same fine-structural argument as in the \(M_1\) case, with \(n\)-smallness replacing \(1\)-smallness. The only point needed below is the exclusion of the ultrapower alternative. The hulls in the diamond argument are chosen so that the collapsed structure has projectum equal to its internal \(\omega_1\). If the ultrapower alternative occurred, an extender on the \(M_n\)-sequence would be indexed at this internal \(\omega_1\). The lower part below that index computes the index as its first uncountable cardinal, while the presence of such an extender would make it inaccessible in the relevant extender model. This contradiction leaves only the initial-segment alternative. ◻

Proof. Work in \(M_n\). Use the canonical well-order \(<_{M_n}\) of the construction to define \(\vec{D}^{\,n}\) recursively. At a limit ordinal \(\alpha<\omega_1\), suppose \(\langle D^n_\beta\mid\beta<\alpha\rangle\) has already been defined. If there is a pair \((A,C)\) such that \(A\subseteq\alpha\), \(C\subseteq\alpha\) is club in \(\alpha\), and \[\forall\beta\in C\,(D^n_\beta\neq A\cap\beta),\] then let \((A_\alpha,C_\alpha)\) be the \(<_{M_n}\)-least such pair and set \(D^n_\alpha=A_\alpha\). If there is no such pair, set \(D^n_\alpha=\emptyset\). At successor stages we again set \(D^n_\alpha=\emptyset\).

The recursion is carried out over \(M_n|\omega_1\), because at stage \(\alpha\) all relevant objects are subsets of the countable ordinal \(\alpha\) in \(M_n\), and the order used to choose the least pair is the restriction of the canonical construction order of \(M_n\).

Suppose toward a contradiction that \(\vec{D}^{\,n}\) is not a diamond sequence in \(M_n\). Let \((A,C)\) be the \(<_{M_n}\)-least counterexample, so \(A\subseteq\omega_1\), \(C\subseteq\omega_1\) is club, and \[\forall\alpha\in C\,(D^n_\alpha\neq A\cap\alpha).\] Choose an \(\omega\)-sound initial segment \(\mathcal{J}^{M_n}_\theta\) containing \(A\), \(C\), and the sequence \(\vec{D}^{\,n}\), and take a countable elementary substructure \[X\prec \mathcal{J}^{M_n}_\theta\] with \(A,C,\vec{D}^{\,n}\in X\) and with \(\alpha=X\cap\omega_1\in C\). Let \[\pi:\bar X\rightarrow X\] be the inverse of the transitive collapse. By Theorem 5, the collapse \(\bar X\) is an initial segment of \(M_n\). Therefore the recursive construction of \(\vec{D}^{\,n}\) inside \(\bar X\) is exactly the initial part \[\langle D^n_\beta\mid\beta<\alpha\rangle.\] The collapse sends \(A\) to \(A\cap\alpha\) and \(C\) to \(C\cap\alpha\), and by elementarity \(\bar X\) sees \((A\cap\alpha,C\cap\alpha)\) as the \(<_{M_n}\)-least witness that the previous sequence is not diamond on \(\alpha\). Hence the recursion at stage \(\alpha\) gives \[D^n_\alpha=A\cap\alpha.\] This contradicts \(\alpha\in C\). Therefore no counterexample exists, and \(\vec{D}^{\,n}\) is a \(\diamondsuit_{\omega_1}\)-sequence in \(M_n\). ◻

Proof. This is the Martin–Solovay theorem for weakly homogeneous trees. The key point is that a weak homogeneity system gives, for each real \(x\), a countable tree of possible measure towers. If one of these towers is countably complete, then \(x\in p[T]\). If no such tower is countably complete, the associated ill-foundedness is witnessed uniformly by a descending sequence of ordinal ranks; these ranks form a branch through \(\operatorname{ms}(\bar\mu,\Theta)_x\), provided \(\Theta\) is chosen above the size of the relevant tree.

Small forcing preserves the measure towers in the required way: the measures extend canonically to the forcing extension, and functions in the extension are represented modulo the lifted measures by ground-model functions. Consequently the same Martin–Solovay tree remains the complementing tree in every \(<\kappa\)-generic extension. This is exactly Steel’s proof of the weakly homogeneous case of the Martin–Solovay theorem. ◻

Proof. The first assertion is Theorem 7. For the final assertion, the projective formula is represented in \(M\) by the pair \((T,S)\), and the pair remains an absolute complementing pair in \(M[G]\). Thus exactly one of the trees has a branch over the real \(x\) in \(M[G]\), and this is the same truth value assigned by the projective definition in the small generic extension. ◻

Proof. We recall the construction, since the parity shift is a common source of confusion. One begins with the projective pointclass immediately below \(\boldsymbol{\Sigma}^1_{n+1}\). By the periodicity theorems and the Martin–Steel scale analysis, the relevant universal set at that lower level has a scale whose associated tree is homogeneous in \(M_{n-1}\). This is the higher analogue of the familiar Martin–Solovay representation of the complete \(\boldsymbol{\Sigma}^1_3\) set by the tree \(T_2\) over \(M_1\).

If the lower-level universal set occurs with the correct polarity, the tree of the scale already gives the required homogeneous representation. If the polarity is the complementary one, one applies the Martin–Solovay construction to the homogeneity system. The Martin–Solovay tree represents the complement by searching for coherent descending ordinal ranks in the corresponding ultrapowers. This is the step which accounts for the odd/even alternation in the projective hierarchy.

Finally, the passage from the lower-level matrix to the universal \(\boldsymbol{\Sigma}^1_{n+1}\) set is an existential real projection. Homogeneous representations are stable under this operation in the weak sense: the additional real witness is absorbed into the weak choice of a countably complete tower. Equivalently, the projection of a homogeneously Suslin representation is weakly homogeneously Suslin. Thus one obtains a tree \(T_n\) with \(p[T_n]=U_{n+1}\) and with \(\kappa\)-complete weak homogeneity systems for every \(\kappa<\delta_0\).

All objects used in this construction are chosen inside \(M_{n-1}\). The completeness of the systems below the least Woodin follows from the extender strength available in \(M_{n-1}\) and the standard Steel tree-production argument. ◻

Proof. By Definition 10, \(T_n\) is \(\kappa\)-weakly homogeneous in \(M_{n-1}\) via \(\bar\mu^n_\kappa\). Theorem 7 gives a Martin–Solovay complement \(S_n\) such that \(T_n\) and \(S_n\) are \(\kappa\)-absolute complements. Since \(|\mathbb{P}|^{M_{n-1}}<\kappa\), the complementing relation holds in \(M_{n-1}[G]\).

The tree \(T_n\) represents the universal \(\boldsymbol{\Sigma}^1_{n+1}\) set in the ground model, and the complementing pair remains absolute in the extension. Therefore a real \(x\) in the extension satisfies the projective universal formula exactly when the \(T_n\)-section above \(x\) is ill-founded. The final sentence is the same argument applied once more to the lifted homogeneity system. ◻

Proof. This is Lemma 9 with \(n=2\). The tree \(T_2\) is the Martin–Solovay tree in the form used by Hjorth and Solovay [13], [14]: it represents the universal \(\boldsymbol{\Sigma}^1_3\) set and carries weak homogeneity systems below the Woodin cardinal of \(M_1\). ◻

Proof. For \(i\ne j\) in \(I\), the set \(C_i\cap C_j\) is bounded in \(\omega_1\). Since \(I\) is countable, there is \(\theta_0<\omega_1\) such that \[C_i\cap C_j\subseteq\theta_0 \qquad(i\ne j\text{ in }I).\] Let \[B^\ast=\{\gamma<\omega_1\mid \exists k<\omega\;(\omega\cdot\gamma+k\in B)\}.\] Then \(B^\ast\) is countable.

For (1), choose \(\theta_1<\omega_1\) such that \[C\cap C_i\subseteq\theta_1 \qquad(i\in I).\] Every \(\gamma\in C\setminus(\theta_1\cup B^\ast)\) has the required property: it does not lie in any \(C_i\), and its \(\omega\)-block does not meet \(B\).

For (2), let \(n<\omega\) be such that \(w(n)\ne u_{i_0}(n)\). If \[\gamma\in (C\cap C_{i_0})\setminus(\theta_0\cup B^\ast),\] then \(\gamma\notin C_i\) for all \(i\ne i_0\), and the \(\omega\)-block of \(\gamma\) does not meet \(B\). At the area \(C_{i_0}\), the coordinate selected by \(u_{i_0}\) at \(n\) is the other member of the pair \[\{\omega\cdot\gamma+2n,\;\omega\cdot\gamma+2n+1\}.\] Hence \(\tau_w(\gamma,n)\notin \operatorname{Sel}(C_{i_0},u_{i_0})\), and it is not in any other \(\operatorname{Sel}(C_i,u_i)\). Thus \(\tau_w(\gamma,n)\notin U\). There are \(\omega_1\)-many such \(\gamma\). ◻

Proof. All decoding procedures used below are the fixed canonical ones. In particular, once \(r\) and an initial segment \(m\in\mathcal{I}\) are given, the almost-disjoint decoding below \(\omega_1^m\) is unique.

First \(L[r,m_\infty]\) can form the almost-disjoint decoding of \(r\) with respect to the canonical family computed from \(m_\infty\): \[Y_r=\{\alpha<\omega_1\mid r\cap d^{m_\infty}_\alpha \text{ is finite}\}.\] This set belongs to \(L[r,m_\infty]\) and is uniquely determined by \(r\) and \(m_\infty\).

We claim that the David decoding of \(Y_r\) in \(L[r,m_\infty]\) succeeds and produces the asserted model code and branch data. Suppose not. Then some finite part of the canonical decoding fails: either the reshaping test fails, or the odd part does not decode a well-founded extensional structure of the required kind, or the resulting collapse does not contain the required distinguished objects, or one of the branch-pattern clauses fails. Choose a sufficiently large regular \(\Theta\) and take, in the ambient universe, a countable elementary submodel \[X\prec H_\Theta\] containing \(r\), \(w\), \(m_\infty\), and a witness to this failure. Let \[\pi:X\longrightarrow \bar M\] be the transitive collapse, and put \(m=\pi(m_\infty)\). By the recovery and condensation facts for the cofinal system \(\mathcal{I}\), the model \(m\) is a member of \(\mathcal{I}\) and \[\omega_1^m=\omega_1^{\bar M}.\] Moreover \(\bar M\) is a countable transitive model of \(\mathsf{ZFC}^-+``\aleph_1\text{ exists}''\), and \(r,w,m\in\bar M\).

Inside \(\bar M\), the almost-disjoint decoding of \(r\) with respect to \(D^m\) is exactly \[Y_r\cap\omega_1^{\bar M}.\] Indeed, for every \(\alpha<\omega_1^{\bar M}\), the real \(d^m_\alpha\) is the corresponding initial member of the canonical almost disjoint family computed from \(m_\infty\), and hence \[\alpha\in Y_r\cap\omega_1^{\bar M} \quad\Longleftrightarrow\quad r\cap d^m_\alpha\text{ is finite}.\] The reshaping and odd/even decoding are first-order procedures over the relevant transitive model, so the failure chosen above reflects to \(\bar M\). Thus \[\bar M\not\models \operatorname{LocalCode}(Y_r\cap\omega_1^{\bar M},w,m).\] But \(\Psi(r,w)\) applies to the countable transitive model \(\bar M\) and the initial segment \(m\). It therefore yields some \(Y\in\bar M\) such that \[\forall\alpha<\omega_1^{\bar M}\, \bigl(\alpha\in Y\Longleftrightarrow r\cap d^m_\alpha \text{ is finite}\bigr)\] and \[\bar M\models\operatorname{LocalCode}(Y,w,m).\] By uniqueness of the almost-disjoint decoding, \(Y=Y_r\cap\omega_1^{\bar M}\), a contradiction. Hence the global decoding in \(L[r,m_\infty]\) succeeds. Let \(X_{\mathcal{N},r}\) be the model code decoded from the odd part of \(Y_r\), let \(\mathcal{N}_r\) be the transitive collapse of the structure coded by \(X_{\mathcal{N},r}\), and let \(C_r\) and the selected branch sequence be the distinguished objects decoded inside \(\mathcal{N}_r\).

It remains to see that the real read from this branch pattern is the original real \(w\). Since the global decoding has succeeded, \(L[r,m_\infty]\) defines a real \(w^*\) by reading the decoded branches: for \(n<\omega\), put \(n\in w^*\) iff, equivalently for every \(\gamma\in C_r\), the decoded branch sequence witnesses that \[S_{\omega\cdot\gamma+2n+1} \text{ has an }\omega_1\text{-branch}.\] The local-code clauses ensure that this definition is independent of the choice of \(\gamma\in C_r\).

Suppose toward a contradiction that \(w^*\neq w\), and choose \(n<\omega\) such that \(w^*(n)\neq w(n)\). Again take a sufficiently large countable elementary submodel \(X\prec H_\Theta\) in the ambient universe containing \(r,w,m_\infty,n\) and enough of the decoded global data to witness the value of \(w^*(n)\), and collapse it to \(\bar M\), with \(m=\pi(m_\infty)\). As above, \(\bar M\) is a relevant countable transitive model, \(m\in\mathcal{I}\), \(\omega_1^m=\omega_1^{\bar M}\), and the almost-disjoint decoding of \(r\) in \(\bar M\) is \(Y_r\cap\omega_1^{\bar M}\). By elementarity and the absoluteness of the decoding procedure, \(\bar M\) reads the \(n\)-th bit of the local branch pattern as \(w^*(n)\). On the other hand, \(\Psi(r,w)\) says that the same uniquely decoded set satisfies \[\bar M\models \operatorname{LocalCode}(Y_r\cap\omega_1^{\bar M},w,m),\] so \(\bar M\) reads the \(n\)-th bit of that same branch pattern as \(w(n)\). This contradicts \(w^*(n)\neq w(n)\).

Therefore \(w^*=w\). Since \(w^*\) is definable in \(L[r,m_\infty]\) from the decoded objects, we have \(w\in L[r,m_\infty]\). The decoded objects also belong to \(L[r,m_\infty]\) by construction, and the displayed branch-pattern equivalences hold there. This proves the lemma. ◻

Proof. For (1), observe that the first component of every successor stage is a fresh copy of the \(M_1\)-computed \(\omega_1\)-Cohen reservoir forcing. These coordinates are independent of one another and are ordered with countable support. They may therefore be moved to a single product part \(\mathbb{C}_{\mathrm{res}}\). The second-step forcing at a stage is then read over the product extension. If the stage is a relative regularity stage, the forcing remains the fixed forcing computed in the lifted admissible base; it is not recomputed in the larger universe. If the stage is an explicit coding stage, the almost-disjoint forcing is computed from the lifted localized name and from the corresponding reservoir generic. Ordinary Cohen and trivial stages are unaffected. Canonical lifting of localized presentations preserves the well-order comparison clauses. This gives the stated normal form, and the forcing over \(M_1\) is obtained by placing the initial branch product \(Br\) in front.

For (2), use the normal form from (1). The branch product \(Br\) is c.c.c. and has size \(\aleph_1\). The reservoir part \(\mathbb{C}_{\mathrm{res}}\) is the \(M_1\)-computed countable-support product of copies of \(\mathbb{C}_{M_1}\). We use its closure before the branch product is performed: over \(M_1\) this reservoir block is \(\sigma\)-closed, hence it preserves \(\omega_1\) and preserves the finite-product Suslinity of the fixed sequence \(\vec{S}\). Thus, in the reservoir extension, \(Br\) is still c.c.c. After the branch product, the real-adding part \(\dot{\mathbb{S}}\) is a finite-support iteration of c.c.c. forcings: ordinary Cohen forcing, fixed relative Random algebras, fixed relative amoeba forcings over admissible bases, Jensen–Solovay almost-disjoint coding forcings, and trivial factors. Hence \(\dot{\mathbb{S}}\) is c.c.c. and therefore proper. This commuted presentation proves preservation for the full forcing over \(M_1\), and therefore for the post-branch quotient over \(W\). Notice that we do not use the post-branch reservoir quotient as a literally \(\sigma\)-closed forcing over \(W\).

If \(\delta\leq\omega_2\), the same normal form gives preservation of \(\omega_2\). Since \(M_1\) satisfies \(\mathsf{GCH}\) and \(Br\) has size \(\aleph_1\), the branch extension \(W\) satisfies \(\mathsf{CH}\) and \((\omega_2)^\omega=\omega_2\). The usual \(\Delta\)-system argument therefore shows that the countable-support product of at most \(\omega_2\) many \(\aleph_1\)-sized reservoir coordinates has the \(\aleph_2\)-chain condition. In the reservoir extension, every real-adding iterand in \(\dot{\mathbb{S}}\) has size at most \(\aleph_1\): this is clear for ordinary Cohen forcing, Jensen–Solovay almost-disjoint coding, and trivial forcing, and for relative relative regularity forcing it follows because admissible bases have only \(\aleph_1\)-many relevant Borel codes. A second \(\Delta\)-system argument therefore shows that the finite-support real-adding iteration has the \(\aleph_2\)-chain condition. Thus \(\omega_2\) is preserved.

Clause (3) follows from the definition of the coding areas. If \(g\ne h\), let \(\xi<\omega_1\) be the first coordinate at which they differ. Then no proper initial segment of \(g\) of length above \(\xi\) can equal a proper initial segment of \(h\) of length above \(\xi\). Since \(\rho\) is one-to-one, \(C_g\cap C_h\) is contained in the codes of the initial segments of length at most \(\xi\), and is therefore bounded in \(\omega_1\).

For (4), the decoding predicate is local to a single reservoir area and to the almost-disjoint real added for the reshaped set associated with that area. Distinct reservoir areas are almost disjoint by (3), and all later stages use fresh reservoir coordinates. Thus later coding blocks may add new codes, but they do not change the old almost-disjoint pattern and cannot make a disjoint block decode the same old object. If a purported decoding uses the same reservoir area as an earlier explicit coding stage, then the David decoding on that area is the one produced at that stage, so it yields the intentionally coded real. If the reservoir area belongs to a non-coding stage, there is no corresponding almost-disjoint coding real and hence no coding block to decode.

For (5), after \(g_\beta\) is added, the set \(Y_{g_\beta,u_\beta}\) is exactly the David reshaping of the model code associated with \(u_\beta\), and the real \(r_\beta\) added by \(\mathbb{A}_D(Y_{g_\beta,u_\beta})\) almost-disjointly decodes this \(Y\) over every relevant countable model. Hence \(\Psi(r_\beta,u_\beta)\) holds by the definition of \(\Psi\). The persistence follows because later locally allowable stages preserve \(\omega_1\), use fresh reservoir coordinates, and do not change the already added real \(r_\beta\) or the initial segment of the almost-disjoint family used in the decoding. ◻

Proof. We prove the localization statement by induction on \(\delta\). We use the normal form from Lemma 12, but in the commuted full presentation over \(M_1\). Thus the full forcing is equivalent to \[\mathbb{C}_{\mathrm{res}}*(Br*\dot{\mathbb{S}}),\] where \(\mathbb{C}_{\mathrm{res}}\) is the \(M_1\)-computed countable-support product of the reservoir coordinates, and, in the \(\mathbb{C}_{\mathrm{res}}\)-extension, \(Br*\dot{\mathbb{S}}\) is a finite-support c.c.c. iteration of the branch product together with the real-adding second-step coordinates. The reservoir block is used here before the branch product. It is \(\sigma\)-closed over \(M_1\), and hence adds no reals, and no countable sequences of \(M_1\)-ordinals. We do not use the post-branch reservoir quotient over \(W=M_1[H]\) as a closed forcing.

Replace \(\vec{\tau}\) by equivalent names in this commuted presentation. In the \(\mathbb{C}_{\mathrm{res}}\)-extension, take nice names for these reals and natural numbers with respect to the c.c.c. forcing \(Br*\dot{\mathbb{S}}\). Thus, for each bit of each real name, and for each natural-number name, there is a countable maximal antichain deciding the relevant value. Each condition in such an antichain has finite branch support and finite support in the real-adding second-step coordinates. Since \(\mathbb{C}_{\mathrm{res}}\) adds no countable sequences of ground ordinals, the union of the second-step supports appearing in all these antichains is represented by a countable set of hybrid coordinates. Let this set be \(A_0\subseteq\delta\). The branch coordinates which occur in the \(W\)-parameters of these names are recorded separately in \(B_0\); they are not coordinates of the post-branch forcing.

We now close \(A_0\) under the dependencies needed to make the restricted hybrid presentation meaningful. Given \(A_n\), define \(A_{n+1}\) as follows. If \(\eta\in A_n\) is a relative Random, measure-amoeba, or category-amoeba stage, let \[(A^{\mathrm{reg}}_\eta, \dot{W}^{\mathrm{reg}}_\eta, B^{0,\mathrm{reg}}_\eta, \dot{B}^{\mathrm{reg}}_\eta)\] be the canonical support witness for the regularity base at \(\eta\). Thus \[\dot{W}^{\mathrm{reg}}_\eta =L[T_2,\dot{a}^\eta_0, \ldots,\dot{a}^\eta_{k_\eta-1}]\] for finitely many names for reals read on \(A^{\mathrm{reg}}_\eta\). Put \(A^{\mathrm{reg}}_\eta\subseteq A_{n+1}\). If \(\eta\in A_n\) is an explicit coding stage, apply the induction hypothesis below \(\eta\) to the name which is coded at \(\eta\), and add the resulting countable admissible support to \(A_{n+1}\). Ordinary Cohen and trivial stages require no additional support. Finally let \[A=\bigcup_{n<\omega}A_n.\] Then \(A\) is countable.

By construction, every nontrivial stage kept in \(A\) has all earlier data needed to interpret its tag: regularity stages have their finite real-parameter base read on the included support, and coding stages have the coded real read on the included support. Hence \(A\) is admissible in the sense of Definition 12, and the canonical embedding identifies \(\mathbb{P}_A\) with a complete subforcing of \(\mathbb{P}_\delta\). The nice names chosen above mention only stages in \(A\), after replacing every kept stage by its restricted version. Therefore they define a tuple \(\vec{\sigma}\) of \(\mathbb{P}_A\)-names such that \[\mathbb{P}_\delta\Vdash \vec{\tau}=\vec{\sigma}^{\uparrow\delta}.\] This proves the localization statement. The assertion for a real \(x\in W[G_\delta]\) follows by applying the first part to a name for \(x\).

It remains to record the footprint form. By definition, \(B_0(A,\vec{\sigma})\) is countable. Each explicit coding stage in \(A\) contributes one set \(\operatorname{Sel}(C,u)\). If \(\eta\in A\) is a relative Random, measure-amoeba, or category-amoeba stage, then the canonical support witness for its base contributes \[B^{0,\mathrm{reg}}_\eta \cup \bigcup_{\nu\in E(A^{\mathrm{reg}}_\eta)} \operatorname{Sel}(C_\nu,u_\nu).\] Here \(A^{\mathrm{reg}}_\eta\) is the countable support on which the finitely many real parameters generating the displayed \(L[T_2,\vec{a}]\)-base are read, and \(B^{0,\mathrm{reg}}_\eta\) is the countable branch-product support of the \(W\)-parameters occurring in those names. Since \(A\) is countable, all selected coding-area contributions can be enumerated as \[(C_j,u_j)_{j\in J} \qquad\text{with }J\text{ countable},\] together with one countable set \(B\subseteq\omega_1\). Hence \[U(A,\vec{\sigma},G_\delta) =B\cup\bigcup_{j\in J}\operatorname{Sel}(C_j,u_j).\] Lemma 10 applies to every set of this form. ◻

Proof. We argue by induction over the restricted presentation \(\mathcal{R}_A\). Since \(\xi\notin B_0(A,\vec{\sigma})\), every ground-model parameter from \(W=M_1[H]\) used by \(\vec{\sigma}\), by the bookkeeping on \(A\), or by a stage of \(\mathcal{R}_A\), is represented by a \(<_{M_1}\)-least \(Br\)-name whose support omits \(\xi\). Hence all such parameters are in \(W_\xi\). Moreover the product on the branch coordinates different from \(\xi\) preserves \(S_\xi\), by independence of \(\vec{S}\).

Suppose first that \(\eta\in A\) is a relative Random, measure-amoeba, or category-amoeba stage. Let \[(A^{\mathrm{reg}}_\eta, \dot{W}^{\mathrm{reg}}_\eta, B^{0,\mathrm{reg}}_\eta, \dot{B}^{\mathrm{reg}}_\eta)\] be the admissibility witness for its base. Since \(A\) is admissible, \[A^{\mathrm{reg}}_\eta\subseteq A\cap\eta.\] Also \[B^{0,\mathrm{reg}}_\eta\subseteq B_0(A,\vec{\sigma}) \quad\text{and}\quad (\dot{B}^{\mathrm{reg}}_\eta)^{G_{A^{\mathrm{reg}}_\eta}} \subseteq U(A,\vec{\sigma},G_\delta).\] Thus \(\xi\) is outside the branch footprint of the base. By Definition 14, this witness is obtained from finitely many \(\mathbb{P}_{A^{\mathrm{reg}}_\eta}\)-names for reals \[\dot{a}^\eta_0,\ldots,\dot{a}^\eta_{k_\eta-1}\] and \[\dot{W}^{\mathrm{reg}}_\eta =L[T_2,\dot{a}^\eta_0,\ldots,\dot{a}^\eta_{k_\eta-1}].\] The set \(B^{0,\mathrm{reg}}_\eta\) records the branch-product supports of the \(W\)-parameters occurring in the codes of these real names, and \((\dot{B}^{\mathrm{reg}}_\eta)^{G_{A^{\mathrm{reg}}_\eta}}\) records the branch coordinates generated by the explicit coding stages in \(A^{\mathrm{reg}}_\eta\). Since both are contained in \(U(A,\vec{\sigma},G_\delta)\) and \(\xi\notin U(A,\vec{\sigma},G_\delta)\), the finite tuple \[\langle \dot{a}^\eta_i\mid i<k_\eta\rangle\] is interpreted in \(W_\xi[G_{A^{\mathrm{reg}}_\eta}]\) with the same value as in \(W[G_{A^{\mathrm{reg}}_\eta}]\). Hence the base interpreted in the \(\xi\)-omitting model is the same model \[L[T_2,a^\eta_0,\ldots,a^\eta_{k_\eta-1}]\] as in the full extension; here \(T_2\in M_1\) is fixed ground-model data. The iterand at \(\eta\) is therefore the same relative Random, measure-amoeba, or category-amoeba forcing computed in this base; it is not recomputed in the ambient model. The relative Random algebra is Knaster, and the two amoeba forcings used here are \(\sigma\)-linked. Hence the iterand preserves \(S_\xi\).

If \(\eta\in A\) is an ordinary Cohen or trivial stage, the conclusion is immediate. The reservoir coordinate at \(\eta\) is the fixed \(M_1\)-Cohen forcing and is independent of the branch coordinate \(\xi\); in the normal form of Lemma 12 it is placed before the branch product and preserves \(S_\xi\).

It remains to consider an explicit coding stage \(\eta\in A\). Let \(\dot{u}_\eta\) be the name coded at \(\eta\), and let \(C_\eta^G\) be the coding area of the reservoir generic. By admissibility, \(\dot{u}_\eta\) is read on an earlier support contained in \(A\). The branch coordinates used by the David code at this stage are precisely \[\operatorname{Sel}(C_\eta^G,u_\eta^G).\] Since this set is contained in \(U(A,\vec{\sigma},G_\delta)\) and \(\xi\notin U(A,\vec{\sigma},G_\delta)\), the branch \(b_\xi\) is not used in forming \(Y_{g_\eta,u_\eta}\). Hence the same reshaped set and the same almost-disjoint coding forcing are computed over the \(\xi\)-omitting model. The Jensen–Solovay almost-disjoint forcing is Knaster, and so preserves \(S_\xi\).

At limit stages the restricted presentation uses mixed support. The support in \(A\) is countable on reservoir coordinates and finite on the c.c.c. real-adding coordinates at each condition. The preceding successor analysis therefore iterates along \(A\). Thus \(\mathcal{R}_A\) is defined over \(W_\xi\), \(G_A\) is generic over \(W_\xi\), the tuple \(\vec{\sigma}^{G_A}\) belongs to \(W_\xi[G_A]\), and no stage of the restricted forcing adds a branch through \(S_\xi\). Hence \(S_\xi\) remains Suslin in \(W_\xi[G_A]\). ◻

Proof. Fix \(r\in W[G_\delta]\) such that \(\Psi(r,w)\). Put \[m_\infty=\mathcal{J}^{M_1}_{\omega_1}.\] By Lemma 11, the model \(L[r,m_\infty]\) decodes a coding area \(C_r\subseteq\omega_1\) and a selected branch pattern. Thus \(|C_r|=\omega_1\), and for every \(\gamma\in C_r\) and \(n<\omega\), if \[\xi=\tau_w(\gamma,n),\] then \(L[r,m_\infty]\) contains an \(\omega_1\)-branch through \(S_\xi\).

First suppose that \(r\in W\). Since \(W=M_1[H]\) is obtained by the finite-support branch product, there is \(B\in[\omega_1]^\omega\) such that \(r\in M_1[H\upharpoonright B]\). Since \(w\in L[r,m_\infty]\), also \(w\in M_1[H\upharpoonright B]\). Choose \(\gamma\in C_r\) such that \[\{\omega\cdot\gamma+k\mid k<\omega\}\cap B=\emptyset.\] Choose \(n<\omega\), and set \(\xi=\tau_w(\gamma,n)\). Then \(\xi\notin B\). By independence of \(\vec{S}\), the tree \(S_\xi\) is Suslin in \(M_1[H\upharpoonright B]\). But \[L[r,m_\infty]\subseteq M_1[H\upharpoonright B]\] contains an \(\omega_1\)-branch through \(S_\xi\), a contradiction. Hence \(r\notin W\).

Choose a countable admissible support \(A\subseteq\delta\) and a \(\mathbb{P}_A\)-name \(\sigma\) such that \[\sigma^{G_A}=r, \qquad G_A=G_\delta\cap\mathbb{P}_A.\] Enlarge \(A\), if necessary, so that it contains the local supports needed for this name. Let \(\vec{\sigma}=(\sigma)\). By the definition of the footprint, there are a countable set \(J\), a countable set \(B\subseteq\omega_1\), coding areas \((C_j:j\in J)\), and reals \((u_j:j\in J)\), such that \[U(A,\vec{\sigma},G_\delta) = B\cup\bigcup_{j\in J}\operatorname{Sel}(C_j,u_j).\] Each pair \((C_j,u_j)\) comes from an explicit coding stage of \(\mathcal{R}_\delta\). The set \(B\) contains the branch-product supports of the \(W\)-parameters in the names under consideration and the countable parts of the regularity-base witnesses. The coding areas \((C_j:j\in J)\) are pairwise almost disjoint.

If there is \(j\in J\) such that \(u_j=w\), then \(w\) is the real explicitly coded at the corresponding stage, and we are done. We therefore assume \[\forall j\in J\quad u_j\ne w.\] Let \[J_1=\{j\in J\mid C_r\cap C_j\text{ is unbounded in }\omega_1\}.\]

If \(J_1\ne\emptyset\), choose \(j_0\in J_1\). Then \(u_{j_0}\ne w\). Choose \(n<\omega\) with \[u_{j_0}(n)\ne w(n).\] By Lemma 10, applied to the countable family \((C_j:j\in J)\), the set \(B\), the set \(C_r\), and the index \(j_0\), there is \(\gamma\in C_r\cap C_{j_0}\) such that \[\tau_w(\gamma,n)\notin U(A,\vec{\sigma},G_\delta).\] Set \(\xi=\tau_w(\gamma,n)\).

If \(J_1=\emptyset\), then every \(C_r\cap C_j\), \(j\in J\), is bounded. By Lemma 10 there is \(\gamma\in C_r\) such that \[\{\omega\cdot\gamma+k\mid k<\omega\} \cap U(A,\vec{\sigma},G_\delta)=\emptyset.\] Choose \(n<\omega\), and set \(\xi=\tau_w(\gamma,n)\).

In both cases \[\xi\notin U(A,\vec{\sigma},G_\delta),\] and \(L[r,m_\infty]\) contains an \(\omega_1\)-branch through \(S_\xi\). By Lemma 14, the restricted extension \(W_\xi[G_A]\) contains \(r\), and \(S_\xi\) remains Suslin in \(W_\xi[G_A]\). Since \(m_\infty\in M_1\subseteq W_\xi[G_A]\), we have \[L[r,m_\infty]\subseteq W_\xi[G_A].\] This contradicts the Suslinity of \(S_\xi\) in \(W_\xi[G_A]\). The contradiction shows that the earlier case must occur: \(w\) is explicitly coded at some stage \(\beta<\delta\). ◻

Proof. We prove the statement for the underlying hybrid presentation. The auxiliary name is allowed to change, and in general it should change, because the set of tentative values records the ranks at which values were selected.

If \(\beta\) is a limit ordinal, the assertion is immediate from Definition 16. If \(\alpha\) is a nonzero limit, it is enough to prove the assertion for all \(\xi<\alpha\). Thus it remains to consider the case in which \(\beta\) is a successor ordinal and \(\alpha\) is either \(0\) or a successor ordinal.

Write \(\beta=\theta+1\), and let \(F\in M_1\) witness that \((\mathcal{R}_\delta,\dot{I}^\beta_\delta)\) is \(\beta\)-allowable. We construct a new \(M_1\)-bookkeeping function \(F^\alpha\) such that the \(\alpha\)-allowable recursion guided by \(F^\alpha\) produces the same underlying hybrid presentation \[\langle\mathcal{R}_\eta\mid \eta\leq\delta\rangle.\] At trivial, relative Random, relative amoeba, Cohen, direct coding, and well-order coding stages we keep the same bookkeeping entry. These clauses are independent of the rank of allowability.

At a uniformization stage, suppose first that the original construction uses clause (b). Then no witness for clause (a) exists at any rank below \(\beta\), hence none exists at any rank below \(\alpha\). The \(\alpha\)-construction therefore also uses clause (b), coding the same real.

Suppose next that the original construction uses clause (a). Let \(\xi<\beta\) be the least rank witnessing clause (a), let \(\dot{y}_0\) be the chosen local name, and let \(\dot{u}\) be the name actually coded by the stage. If \(\xi<\alpha\), then the same witness is available in the \(\alpha\)-allowable construction, and the same name \(\dot{u}\) is coded. If \(\alpha\leq\xi<\beta\), then by minimality of \(\xi\) there is no witness to clause (a) of rank below \(\alpha\). In this case we alter the bookkeeping entry so that it decodes to the uniformization tuple \[(\dot{x},\dot{u},\dot{m}),\] where \(\dot{u}\) is the name actually coded by the original construction. If \(\alpha=0\), this is a \(0\)-allowable coding stage. If \(\alpha\) is a successor, clause (a) fails below \(\alpha\), so clause (b) prescribes the same coding operation. Thus the same underlying forcing stage is reproduced.

This defines \(F^\alpha\) recursively. The definition uses only \(M_1\)-codes for the original bookkeeping entries, the canonical localized presentations, the selected names, and the relevant ordinals. Hence \(F^\alpha\in M_1\), and the \(\alpha\)-allowable construction guided by \(F^\alpha\) produces the same underlying hybrid presentation. ◻

Proof. Restrict the bookkeeping construction witnessing the \(\rho\)-allowability of \((\mathcal{R}_\delta,\dot{I}_\delta)\) to the interval \([\beta,\gamma)\). This restricted construction starts with the already built pair \((\mathcal{R}_\beta,\dot{I}_\beta)\) and then appends exactly the same hybrid steps which occur in the original construction between stages \(\beta\) and \(\gamma\). At successor stages, the decision is made from the current full hybrid forcing, the current auxiliary name, the decoded bookkeeping entry, the localized presentations of the names involved, and the forcing relation over that current hybrid forcing. These are exactly the data available in the relative construction starting from \((\mathcal{R}_\beta,\dot{I}_\beta)\). If the stage is a relative Random or amoeba stage, its admissibility witness \[(A_{\mathrm{rb}},\dot{W}_{\mathrm{rb}},B^0_{\mathrm{rb}},\dot{B}_{\mathrm{rb}})\] is carried with the stage: the tail uses the forcing computed in \(\dot{W}_{\mathrm{rb}}\), and the lifted footprint name records the branch coordinates generated by the local support. At limit stages both constructions take the same mixed-support hybrid limit and the same canonical union of the preceding auxiliary names.

The quotient assertion follows by interpreting the relative presentation in \(W\) by a \(\mathbb{P}_\beta\)-generic filter. The assertion for lower ranks follows from Lemma 16, applied to the relative tail. Transitivity is obtained by concatenating the two relative tail presentations, renaming reservoir coordinates to fresh coordinates if necessary. ◻

Proof. We argue by induction on \(\rho\). Write \[\mathcal{R}^i=\langle \mathcal{R}^i_\beta\mid \beta\leq\delta_i\rangle \qquad (i<2),\] and let \(P^i_\beta\) denote the post-branch forcing over \(W\) represented by \(\mathcal{R}^i_\beta\); thus \(P^i=P^i_{\delta_i}\). The product presentation \(\mathcal{R}^\otimes\) is obtained by first running \(\mathcal{R}^0\), and then running a shifted copy of \(\mathcal{R}^1\). Every name \(\dot{\tau}\) occurring in the second block is replaced by its canonical lift \(\dot{\tau}^\uparrow\) to the corresponding product initial segment, and all reservoir coordinates in the second block are renamed to fresh coordinates. Let \(P^\otimes_\gamma\) denote the post-branch forcing associated with the initial product presentation \(\mathcal{R}^\otimes_\gamma\). Thus, for every \(\beta\leq\delta_1\), \[P^\otimes_{\delta_0+\beta} \cong P^0\times P^1_\beta .\] The auxiliary names are defined by \[\dot{I}^\otimes_{\delta_0+\beta} = \dot{I}^0\cup(\dot{I}^1_\beta)^\uparrow\] with the evident interpretation at stages \(\leq\delta_0\). Limit stages use the same mixed-support limits as the two original presentations.

For \(\rho=0\), this concatenation witnesses \(0\)-allowability. The ordinary Cohen, direct coding, well-order coding, and trivial stages are lifted second-block stages. If a shifted second-block stage is a relative regularity stage with tag \[(\mathrm{Rand};\dot{a}_0,\ldots,\dot{a}_{k-1}), \quad (\mathrm{Am}_{\mathcal{N}};\dot{a}_0,\ldots,\dot{a}_{k-1}), \quad\text{or}\quad (\mathrm{Am}_{\mathcal{M}};\dot{a}_0,\ldots,\dot{a}_{k-1}),\] then the product presentation uses the shifted tag obtained by lifting the finitely many real names to the product initial segment. If the original stage has canonical admissibility witness \[(A_{\mathrm{rb}},\dot{W}_{\mathrm{rb}},B^0_{\mathrm{rb}},\dot{B}_{\mathrm{rb}}),\] where \[\dot{W}_{\mathrm{rb}}=L[T_2,\dot{b}_0,\ldots,\dot{b}_{k-1}]\] for the least tuple of names reading the displayed real parameters, then the shifted stage has the lifted witness obtained from \[A_{\mathrm{rb}}^\otimes, \qquad \langle \dot{b}_i^\uparrow\mid i<k\rangle, \qquad B^0_{\mathrm{rb}}, \qquad \dot{B}_{\mathrm{rb}}^\uparrow.\] Here \(A_{\mathrm{rb}}^\otimes\) is the shifted copy of \(A_{\mathrm{rb}}\) in the second block, each \(\dot{b}_i^\uparrow\) is the canonical lift of \(\dot{b}_i\) to the product initial segment, and \(\dot{B}_{\mathrm{rb}}^\uparrow\) is the canonical lift of the branch-footprint name. The lifted regularity base is therefore \[L[T_2,\dot{b}_0^\uparrow,\ldots,\dot{b}_{k-1}^\uparrow]\] (with the evident meaning \(L[T_2]\) if \(k=0\)). The Random or amoeba forcing is computed in this lifted base, not in the larger product extension. Hence the displayed product equivalence is preserved at the shifted regularity stage.

Now assume \(\rho=\alpha+1\). By the successor uniformization clause we mean the two alternatives (a) and (b) in Definition 18, evaluated at a uniformization tag \[(\mathrm{UF},\dot{x},\dot{z},\dot{m}).\] Thus clause (a) searches through ranks \(\zeta<\rho\) for a localized name \(\dot{y}\) which is forced into the relevant \(A_{\dot{m}}\)-section and cannot be forced out by any relative \(\zeta\)-allowable tail; clause (b) is used when no such witness exists.

Consider a shifted uniformization stage \(\delta_0+\beta\), and let \[(\mathrm{UF},\dot{x},\dot{z},\dot{m})\] be the corresponding second-block bookkeeping value. For \(\zeta<\rho\) and a localized \(P^1_\beta\)-name \(\dot{y}\), write \[\mathsf{Kick}^1_\beta(\zeta,\dot{y})\] for the assertion that there are a relative \(\zeta\)-allowable extension \[(\mathcal{S},\dot{J})\triangleright_\zeta (\mathcal{R}^1_\beta,\dot{I}^1_\beta)\] and, writing \(P_{\mathcal{S}}\) for the terminal post-branch forcing associated with \(\mathcal{S}\), a quotient condition \(p\in P_{\mathcal{S}}/\dot{G}^1_\beta\) such that \[p\Vdash (\dot{x}^{\uparrow\mathcal{S}}, \dot{y}^{\uparrow\mathcal{S}}) \notin A_{\dot{m}^{\uparrow\mathcal{S}}}.\] Define \(\mathsf{Kick}^\otimes_\beta(\zeta,\dot{y}^\uparrow)\) analogously over the product initial segment \[(\mathcal{R}^\otimes_{\delta_0+\beta}, \dot{I}^\otimes_{\delta_0+\beta}).\] Then \[\mathsf{Kick}^1_\beta(\zeta,\dot{y}) \quad\Longleftrightarrow\quad \mathsf{Kick}^\otimes_\beta(\zeta,\dot{y}^\uparrow).\] The implication from left to right follows by taking the product of the fixed first block with the displayed relative \(\zeta\)-allowable tail and applying the induction hypothesis. The implication from right to left follows by restricting the witnessing product tail to the complete subpresentation generated by the lifted second-block support of \((\dot{x},\dot{y},\dot{m})\), using Lemmas 17 and 16.

Similarly, \[P^1_\beta\Vdash (\dot{x},\dot{y})\in A_{\dot{m}} \quad\Longleftrightarrow\quad P^0\times P^1_\beta \Vdash (\dot{x}^\uparrow,\dot{y}^\uparrow)\in A_{\dot{m}^\uparrow}.\] Hence the set of clause (a) witnesses in the product construction is exactly the lift of the set of clause (a) witnesses in the second construction. Thus clause (a) holds in the shifted product stage iff it holds in the original second-block stage. When it holds, the least rank and the \(<_{M_1}\)-least localized witness are the lifted ones. When it fails, clause (b) uses the lifted bookkeeping guess \(\dot{z}^\uparrow\). The auxiliary name is updated by \[\dot{I}^0\cup(\dot{I}^1_{\beta+1})^\uparrow.\] This proves the successor step.

Finally let \(\lambda\) be a nonzero limit ordinal. If both inputs are \(\lambda\)-allowable, then by the induction hypothesis the product presentation is \(\zeta\)-allowable for every \(\zeta<\lambda\). Since \[\mathcal{A}^W_\lambda = \bigcap_{\zeta<\lambda}\mathcal{A}^W_\zeta,\] the product presentation is \(\lambda\)-allowable. The bookkeeping witness at a limit level is obtained by packaging the lower-level witnesses together with the concatenation description. Thus \(F^\otimes\in M_1\) is definable from \(F_0\) and \(F_1\). ◻

Proof. Suppose that \(\beta\) is the stage at which the tuple \((x,y,m,\xi)\) is added to the auxiliary name. At that stage clause (a) of Definition 18 was used. Let \[\dot{x}_\beta,\qquad \dot{y}_\beta,\qquad \dot{m}_\beta\] be the canonical names chosen there, and let \(\xi_\beta=\xi\). Clause (a) gives \[\mathbb{P}_\beta\Vdash (\dot{x}_\beta,\dot{y}_\beta)\in A_{\dot{m}_\beta},\] and it also gives the preservation statement saying that no relative \(\xi_\beta\)-allowable tail over the stage-\(\beta\) initial segment can force the lifted pair out of the relevant section.

By Lemma 17, the interval from stage \(\beta\) to the terminal forcing is a relative \(\xi_\beta\)-allowable tail. Therefore no condition in the terminal forcing can force \[(\dot{x}_\beta,\dot{y}_\beta)\notin A_{\dot{m}_\beta}.\] The forcing theorem gives the membership in the final extension. If \((\mathcal{S},\dot{J})\triangleright_\xi(\mathcal{R},\dot{I})\) is any further relative \(\xi\)-allowable extension, then the concatenation of the interval from \(\beta\) to the terminal forcing with this further extension is again a relative \(\xi\)-allowable extension over stage \(\beta\). The same preservation statement therefore rules out any quotient condition forcing the pair out of \(A_m\). ◻

Proof. We argue by induction on the construction stages. At stage \(0\), the presentation is the trivial post-branch presentation, which is allowable by Lemma 12. At limit stages, the construction takes the countable-support direct limit of the earlier presentations. This is allowed by the limit clause in the derivative hierarchy defining \(\alpha\)-allowability.

Consider a successor stage. The relative regularity cases, the ordinary Cohen case, and the well-order case are instances of the successor clauses in the local allowable recursion. In each of these cases the construction first adds the fresh \(M_1\)-Cohen reservoir coordinate and then performs the specified second step, or the trivial second step if the relevant bookkeeping value is not meaningful. Therefore the resulting presentation remains \(\alpha^\ast\)-allowable over the preceding initial segment.

The first uniformization case is the stabilized successor clause from Definition 19. The chosen tentative value is added to the auxiliary name with its rank, and the construction intentionally codes only a competing reserved tag. Thus the new presentation is again \(\alpha^\ast\)-allowable over the preceding initial segment.

It remains to check the second uniformization case. In this case the construction starts with a relative \(\alpha^\ast\)-allowable continuation \[(\mathcal{S},\dot{J})\triangleright_{\alpha^\ast} (\mathcal{R}_\beta,\dot{I}_\beta),\] a quotient condition \(q\in P_{\mathcal{S}}/\dot{G}_\beta\), where \(P_{\mathcal{S}}\) is the terminal post-branch forcing associated with \(\mathcal{S}\), and a name \(\dot{r}\) such that \[q\Vdash \theta(\dot{r}, \dot{x}^{\uparrow\mathcal{S}}, \dot{y}^{\uparrow\mathcal{S}}, \dot{m}^{\uparrow\mathcal{S}}).\] By the local-support convention for hybrid presentations, the condition \(q\), the name \(\dot{r}\), the lifted names \[\dot{x}^{\uparrow\mathcal{S}},\qquad \dot{y}^{\uparrow\mathcal{S}},\qquad \dot{m}^{\uparrow\mathcal{S}},\] and the data needed to interpret these objects are contained in a countable localized subpresentation of \((\mathcal{S},\dot{J})\) over \((\mathcal{R}_\beta,\dot{I}_\beta)\). The construction chooses the \(<_{M_1}\)-least such support and restricts the corresponding presentation below the witnessing condition \(q\). The resulting presentation \[(\mathcal{S}^B,\dot{J}^B)\triangleright_{\alpha^\ast} (\mathcal{R}_\beta,\dot{I}_\beta)\] is still relative \(\alpha^\ast\)-allowable, because the derivative clauses are closed under passing to localized subpresentations and under restricting below a condition. Moreover its quotient forces \[(\dot{x}^{\uparrow\mathcal{S}^B}, \dot{y}^{\uparrow\mathcal{S}^B}) \notin A_{\dot{m}^{\uparrow\mathcal{S}^B}}.\] Thus the second uniformization case also preserves \(\alpha^\ast\)-allowability.

It remains to record the bookkeeping. Whenever the construction appends a countable presentation in the second uniformization case, we use the bookkeeping function witnessing that chosen presentation on the newly added coordinates. On the coordinates coming from the original stages we use the original bookkeeping function \(F\). Since \(\omega_2\) is regular, the concatenation of \(\omega_2\)-many countable presentations has length at most \(\omega_2\), and hence can be indexed by \(\omega_2\) in the order in which it is built. This gives a single \(M_1\)-bookkeeping function \(F^\ast\) for the final presentation.

The cofinality requirements are inherited from \(F\). The original bookkeeping function places ordinary Cohen tags cofinally often. Once a finite tuple of real names becomes meaningful as an admissibly based regularity stage, with witness \((A_{\mathrm{rb}},\dot{W}_{\mathrm{rb}},B^0_{\mathrm{rb}},\dot{B}_{\mathrm{rb}})\), \(F\) places the three corresponding finite-real-parameter tags cofinally often, using the Random, measure-amoeba, and category-amoeba forcings computed in the lifted base generated by that witness. Adding countably many coordinates at individual stages does not destroy cofinality in the final indexing of length \(\omega_2\). Therefore the final presentation has all the required cofinal regularity and Cohen stages, and every initial segment is \(\alpha^\ast\)-allowable relative to \(F^\ast\). Hence \((\mathcal{R}_{\omega_2},\dot{I}_{\omega_2})\) is \(\infty\)-allowable. ◻

Proof. Fix a real \(r\in W^\ast\) witnessing \(\Phi(w)\). Thus \(\Psi(r,w)\) holds in \(W^\ast\), where \(\Psi\) is the predicate used in the definition of \(\Phi\). By the local-support property of the hybrid presentations, the real \(w\), the witness \(r\), and the data needed to verify \(\Psi(r,w)\) are read in a countable localized subpresentation of the final construction over \(W\). Closing this support under the local data used by the relevant names gives a \(0\)-allowable local hybrid presentation \(\mathcal{R}_A\) over \(W\) and a generic filter \(G_A\) such that \[r,w\in W[G_A] \quad\text{and}\quad W[G_A]\models\Psi(r,w).\] Hence \[W[G_A]\models\Phi(w).\]

Apply Lemma 15 to this localized presentation. There is an explicit coding coordinate \(\eta\) of \(\mathcal{R}_A\) and a name \(\dot{u}_\eta\) such that \[w=(\dot{u}_\eta)^{G_A}.\] Thus every occurrence of \(\Phi(w)\) for a reserved tag is produced by an explicit coding coordinate of the actual local presentation which reads the witness.

It remains only to identify which coding coordinates may write reserved tags. The construction uses the tags \(\mathrm{UF}\) and \(\mathrm{WO}\) only for the reserved uniformization and well-order decisions. Direct coding clauses do not use reals whose outer tag is \(\mathrm{UF}\) or \(\mathrm{WO}\). The same convention is part of every countable localized presentation appended in the second uniformization case. Therefore an explicit coding coordinate which writes a real of the form \(\langle\mathrm{WO},z_0,z_1\rangle\) must be a well-order coding step, and an explicit coding coordinate which writes a real of the form \(\langle\mathrm{UF},x,y,m\rangle\) must be a uniformization coding step.

This proves the claimed exactness of the reserved tags. ◻

Proof. The two alternatives are mutually exclusive and exhaustive by their first displayed clauses. We prove the corresponding conclusions.

Assume first that \[X_{x,m}=\{(y,\xi)\mid \xi<\alpha^\ast\text{ and }(x,y,m,\xi)\in I^\ast\}\] is nonempty. Let \(\xi_0\) be the least ordinal such that \((y,\xi_0)\in X_{x,m}\) for some \(y\). Among all names whose interpretation gives such a tuple of rank \(\xi_0\), choose the one with \(<_{M_1}\)-least localized presentation. Let its value be \(y_0\), and let \(\beta_0<\omega_2\) be the first stage at which the corresponding tuple \[(x,y_0,m,\xi_0)\] is inserted into the auxiliary name. By Lemma 19, applied to the tail of the final \(\infty\)-allowable presentation after \(\beta_0\), \[W^\ast\models (x,y_0)\in A_m. \]

We show that \(\Phi(\langle\mathrm{UF},x,y_0,m\rangle)\) fails in \(W^\ast\). Suppose otherwise. By Lemma 21, there is an intentional uniformization coding stage \(\eta<\omega_2\) which codes \[w_0=\langle\mathrm{UF},x,y_0,m\rangle .\] Choose \(\eta\) least with this property.

First suppose that \(\eta\geq\beta_0\). At every stage \(\eta'\geq\beta_0\), the lift of the name for \(y_0\) is still a rank \(\xi_0\) tentative value, by Lemma 19. If the construction at \(\eta\) selected some value different from \(y_0\), then that value would have either smaller rank than \(\xi_0\), or rank \(\xi_0\) and a strictly earlier localized presentation. Its tuple would belong to \(I^\ast\), contradicting the choice of \((\xi_0,y_0)\). Hence \(y_0\) is the selected value at \(\eta\). The first uniformization clause never codes the selected value itself, so \(w_0\) is not coded at \(\eta\), a contradiction.

Now suppose that \(\eta<\beta_0\). If \(w_0\) is coded at \(\eta\) by the second uniformization case, then there are a relative \(\xi_0\)-allowable continuation \((\mathcal{S},\dot{J})\) over \((\mathcal{R}_\eta,\dot{I}_\eta)\), a quotient condition \(q\), and a name \(\dot{r}\), all contained in the countable localized subpresentation chosen at stage \(\eta\), such that, writing \(P_{\mathcal{S}}\) for the terminal post-branch forcing associated with \(\mathcal{S}\), \[q\Vdash_{P_{\mathcal{S}}/\dot{G}_\eta} \theta(\dot{r}, \dot{x}^{\uparrow\mathcal{S}}, \dot{y}_0^{\uparrow\mathcal{S}}, \check m),\] where \((u,v)\notin A_m\) is written as \(\exists r\,\theta(r,u,v,m)\) with \(\theta\in\Pi^1_3\). By Lemma 18 and Lemma 17, composing this continuation with the actual interval from \(\eta\) to \(\beta_0\) gives a relative \(\xi_0\)-allowable continuation over \((\mathcal{R}_{\beta_0},\dot{I}_{\beta_0})\) which forces the lift of \((\dot{x},\dot{y}_0)\) out of \(A_m\). This contradicts the fact that \(y_0\) is inserted at stage \(\beta_0\) as a rank \(\xi_0\) tentative value.

Thus stage \(\eta\) used the first uniformization case. It selected some value \(y_\eta\) and coded \(y_0\) as a different candidate. If a relative \(\xi_0\)-allowable continuation over \((\mathcal{R}_\eta,\dot{I}_\eta)\) forced the lift of \((\dot{x},\dot{y}_0)\) out of \(A_m\), then the same composition argument would contradict the insertion of \((x,y_0,m,\xi_0)\) at \(\beta_0\). Hence \(y_0\) was already eligible at \(\eta\) as a rank \(\xi_0\) tentative value. Since the construction chooses first the least rank and then the \(<_{M_1}\)-least localized presentation, the selected value \(y_\eta\) has rank below \(\xi_0\), or has rank \(\xi_0\) with an earlier localized presentation. Then the tuple for \(y_\eta\) belongs to \(I^\ast\), again contradicting the choice of \((\xi_0,y_0)\). Therefore \[W^\ast\models \neg\Phi(\langle\mathrm{UF},x,y_0,m\rangle). \]

Let now \(y\ne y_0\) and suppose that \(W^\ast\models (x,y)\in A_m\). Choose localized names \(\dot{x},\dot{y},\dot{y}_0\) and, by the usual mixing below a condition in \(G^\ast\), arrange that \[1\Vdash \dot{y}\ne\dot{y}_0, \qquad \dot{x}^{G^\ast}=x, \quad \dot{y}^{G^\ast}=y, \quad \dot{y}_0^{G^\ast}=y_0.\] By bookkeeping, there is a stage \(\gamma>\beta_0\) with \[F(\gamma)=(\mathrm{UF},\dot{x},\dot{y},\check m)\] after these names are available. At stage \(\gamma\), the lift of \(y_0\) is the selected tentative value by the preceding minimality argument. If \(\langle\mathrm{UF},x,y,m\rangle\) has not already been coded, the first uniformization case codes \[\langle\mathrm{UF},\dot{x},\dot{y},\check m\rangle,\] since \(1\Vdash\dot{y}\ne\dot{y}_0\). Hence, in all cases, \[W^\ast\models \Phi(\langle\mathrm{UF},x,y,m\rangle). \] Equations \((1)\)–\((3)\) prove the first alternative.

Assume now that \[X_{x,m}=\emptyset . \] Suppose toward a contradiction that \(W^\ast\models (x,y)\in A_m\). Choose localized names \(\dot{x},\dot{y}\) for \(x,y\), and choose a later stage \(\gamma<\omega_2\) such that \[F(\gamma)=(\mathrm{UF},\dot{x},\dot{y},\check m).\] The first uniformization case cannot occur at \(\gamma\), since it would add some tuple \((x,y',m,\xi)\) with \(\xi<\alpha^\ast\) to \(I^\ast\), contradicting \((4)\). Therefore the second uniformization case is used. Thus the construction appends a countable localized relative \(\alpha^\ast\)-allowable presentation, restricted below a witnessing quotient condition \(q\), and a name \(\dot{r}\) such that \[q\Vdash \theta(\dot{r}, \dot{x}^{\uparrow}, \dot{y}^{\uparrow}, \check m), \] where again \((u,v)\notin A_m\) is written as \(\exists r\,\theta(r,u,v,m)\) with \(\theta\in\Pi^1_3\).

The presentation added at \(\gamma\) is an initial segment of the final presentation, and the remaining quotient is an allowable local hybrid tail. By the \(T_2\)-absoluteness used for allowable tails, the \(\Pi^1_3\)-statement in \((5)\) remains true in the final extension for the same witness \(r=\dot{r}^{G^\ast}\). Hence \[W^\ast\models (x,y)\notin A_m,\] contradicting the choice of \(y\). Therefore \(A_{m,x}=\emptyset\) in \(W^\ast\), as required. ◻

Proof. Fix \(m<\omega\) and a real \(x\in W^\ast\). If the \(x\)-section of \(A_m\) is empty, then no real \(y\) satisfies \(U_m(x,y)\), by definition. Suppose therefore that \(A_{m,x}\neq\emptyset\). The second alternative of Lemma 22 is then impossible. Hence the first alternative holds, and the lemma gives a real \(y_0\) such that \[W^\ast\models (x,y_0)\in A_m \quad\text{and}\quad W^\ast\models \neg\Phi(\langle\mathrm{UF},x,y_0,m\rangle).\] Thus \(U_m(x,y_0)\) holds.

The same lemma also gives uniqueness. Namely, if \(y\neq y_0\) and \((x,y)\in A_m\), then \[W^\ast\models \Phi(\langle\mathrm{UF},x,y,m\rangle),\] so \(U_m(x,y)\) fails. If \((x,y)\notin A_m\), then \(U_m(x,y)\) fails already by its first conjunct. Therefore \(y_0\) is the unique value selected by \(U_m\) on the \(x\)-section of \(A_m\).

It remains to record the projective complexity. By the choice of the universal list, \((x,y)\in A_m\) is \(\Pi^1_4\). The local coding predicate \(\Phi(w)\) was defined in the coding section as a \(\Sigma^1_4\) predicate. Therefore \[\neg\Phi(\langle\mathrm{UF},x,y,m\rangle)\] is \(\Pi^1_4\). Since the class \(\Pi^1_4\) is closed under finite conjunctions, \(U_m(x,y)\) is \(\Pi^1_4\).

For the boldface conclusion, let \(A(x,y)\) be \(\Pi^1_4(a)\). Using the fixed recursive pairing of reals, regard this as a lightface \(\Pi^1_4\) relation in the pair \((a,x)\) and the value \(y\), say as a section of some member of the universal list. Applying the preceding lightface uniformization to the relation on \(((a,x),y)\) and then fixing the parameter \(a\) gives a \(\Pi^1_4(a)\) uniformizing relation for \(A\). ◻

Proof. We first describe the underlying order independently of the projective definition. If \(z\in W^\ast\) is a real, let \(\pi(z)\) be the \(<_{M_1}\)-least localized presentation, in the final hybrid presentation, of a name whose interpretation is \(z\). Such a presentation exists because every real in the final mixed-support hybrid iteration has a bounded local support. If \(z_0\ne z_1\), then \(\pi(z_0)\ne\pi(z_1)\), since the same localized name has only one interpretation in the fixed generic extension. Hence \[z_0\triangleleft z_1 \quad\Longleftrightarrow\quad z_0\ne z_1\text{ and }\pi(z_0)<_{M_1}\pi(z_1)\] defines a well-order of the reals in \(W^\ast\). It is the order induced by the fixed \(<_{M_1}\)-well-order of the canonical localized presentations.

We claim that, for distinct reals \(z_0,z_1\in W^\ast\), \[z_0\triangleleft z_1 \quad\Longleftrightarrow\quad W^\ast\models \Phi(\langle\mathrm{WO},z_0,z_1\rangle).\] Assume first that \(z_0\triangleleft z_1\). Choose localized names \(\dot{z}_0,\dot{z}_1\) whose final canonical localized presentations are \(\pi(z_0)\) and \(\pi(z_1)\). The supports of these presentations are bounded in \(\omega_2\), so there is an initial segment \(\mathbb{P}_\beta\) over which these names are already available. By the bookkeeping property of \(F\), there is a later stage \(\gamma>\beta\) at which \[F(\gamma)=(\mathrm{WO},\dot{z}_0,\dot{z}_1).\] At stage \(\gamma\) the well-order clause compares the same canonical localized presentations. The localization convention and the product/tail lemmas ensure that passing to the larger initial segment, or later appending a countable local tail, does not change the \(<_{M_1}\)-comparison of these presentations. Since \(\pi(z_0)<_{M_1}\pi(z_1)\), the stage explicitly codes \[\langle\mathrm{WO},\dot{z}_0,\dot{z}_1\rangle.\] After interpreting by \(G^\ast\), Lemma 12 yields \[W^\ast\models \Phi(\langle\mathrm{WO},z_0,z_1\rangle).\]

Conversely suppose that \(z_0\ne z_1\) and \[W^\ast\models \Phi(\langle\mathrm{WO},z_0,z_1\rangle).\] By Lemma 21, this code was introduced at an intentional well-order coding stage of the final presentation. Thus, at some stage, the construction decoded a well-order tag, compared the canonical localized presentations of two names whose interpretations are \(z_0\) and \(z_1\), and coded the ordered tag with the smaller presentation placed first. Again the localization and product/tail conventions imply that this comparison agrees with the comparison of the final canonical presentations \(\pi(z_0)\) and \(\pi(z_1)\). Therefore \(\pi(z_0)<_{M_1}\pi(z_1)\), and hence \(z_0\triangleleft z_1\). This proves the claim.

Now define, in \(W^\ast\), \[z_0<_{\Delta}z_1 \quad\Longleftrightarrow\quad z_0\ne z_1\;\land\; \Phi(\langle\mathrm{WO},z_0,z_1\rangle).\] By the claim, \(<_{\Delta}\) is exactly \(\triangleleft\), and hence is a well-order of the reals.

It remains to record the projective complexity. Since \(\Phi\) is the local \(\Sigma^1_4\)-coding predicate, the displayed definition of \(<_{\Delta}\) is \(\Sigma^1_4\). The claim also gives, for distinct reals \(z_0,z_1\), that exactly one of \[\Phi(\langle\mathrm{WO},z_0,z_1\rangle), \qquad \Phi(\langle\mathrm{WO},z_1,z_0\rangle)\] holds. Hence, in \(W^\ast\), the same relation is equivalently defined by \[z_0<_{\Delta}z_1 \quad\Longleftrightarrow\quad z_0\ne z_1\;\land\; \neg\Phi(\langle\mathrm{WO},z_1,z_0\rangle).\] This second definition is \(\Pi^1_4\). Thus \(<_{\Delta}\) is both \(\Sigma^1_4\) and \(\Pi^1_4\), and consequently is a \(\Delta^1_4\)-definable well-order of the reals. ◻

Proof. Fix \(a\in W^\ast\). By Lemma 13, choose a countable admissible support \(A\subseteq\omega_2\) and a \(\mathbb{P}_A\)-name \(\sigma\) such that \[\sigma^{G_A}=a,\] where \(G_A=G^\ast\cap\mathbb{P}_A\). Since \(\omega_2\) is regular, choose \(\beta<\omega_2\) with \(A\subseteq\beta\). Let \[\dot{a}=(\sigma)^{\uparrow\beta}\] and let \(\dot{N}\) be the \(\mathbb{P}_\beta\)-name for \(L[T_2,\dot{a}]\). Then the corresponding regularity tags for \(\dot{N}\) are admissibly based. Indeed, this is the one-parameter instance of Definition 14: take \[A_{\mathrm{rb}}=A, \qquad k=1, \qquad \dot{a}_0=\sigma, \qquad \dot{W}_{\mathrm{rb}}=L[T_2,\sigma].\] No further presentation data are needed. The set \(B^0_{\mathrm{rb}}\) is the countable union of the branch-product supports of the \(W\)-parameters occurring in the name \(\sigma\), and \(\dot{B}_{\mathrm{rb}}\) is the corresponding branch footprint generated by \(B^0_{\mathrm{rb}}\) and by the explicit coding coordinates in \(A\). Thus the bookkeeping for admissible bases applies to \(\dot{N}\), and it must eventually schedule the relative measure- and category-amoeba stages over this base.

By the final bookkeeping, at some stage \(\lambda_{\mathcal{N}}>\beta\) the tag \[(\mathrm{Am}_{\mathcal{N}},\dot{N}^{\uparrow\lambda_{\mathcal{N}}})\] is used. At this stage the forcing is \[\mathbb{A}_{\mathcal{N}}^{N_a},\] computed in the interpreted base \(N_a=L[T_2,a]\). Let \(Z_a^{\mathcal{N}}\) be the Borel null set added by this amoeba forcing. By the definition of amoeba forcing for the null ideal, \[B\subseteq Z_a^{\mathcal{N}}\] for every Borel null set \(B\) coded in \(N_a\). Later forcing preserves the Borel code for \(Z_a^{\mathcal{N}}\) and the statement that it is null. Hence the first displayed inclusion holds in \(W^\ast\).

The meager case is identical. The bookkeeping later uses the tag \[(\mathrm{Am}_{\mathcal{M}},\dot{N}^{\uparrow\lambda_{\mathcal{M}}})\] for some \(\lambda_{\mathcal{M}}>\beta\). The forcing \(\mathbb{A}_{\mathcal{M}}^{N_a}\) adds a Borel meager set \(Z_a^{\mathcal{M}}\) covering every Borel meager set coded in \(N_a\), and this covering relation remains true in the final extension.

Finally, a real is not Random-generic over \(N_a\) iff it belongs to some Borel null set coded in \(N_a\). Hence \[R_a\subseteq Z_a^{\mathcal{N}},\] so \(R_a\) is null. Similarly, a real is not Cohen-generic over \(N_a\) iff it belongs to some Borel meager set coded in \(N_a\). Hence \[C_a\subseteq Z_a^{\mathcal{M}},\] so \(C_a\) is meager. ◻

Proof. We give the argument in the form in which it is used in Hjorth’s proof of Corollary 2.4 of [14], with the use of Martin’s Axiom replaced by Lemma 24. Let \(a\in W^\ast\) be a real parameter and put \[N_a=L[T_2,a].\] Here \(T_2\) is the Martin–Solovay tree fixed in the preliminaries. By Lemma 24, almost every real in \(W^\ast\) is Random over \(N_a\), and comeagerly many reals in \(W^\ast\) are Cohen over \(N_a\).

Let \(A\subseteq\omega^\omega\) be \(\Sigma^1_3(a)\), say \[A=\{z: W^\ast\models\varphi(z,a)\},\] where \(\varphi(v,a)\) is a \(\Sigma^1_3(a)\) formula. We prove first that \(A\) is Lebesgue measurable. Work in \(N_a\) with the Random algebra \(\mathbb{B}_{\mathrm{rand}}^{N_a}\) and let \(\dot{r}\) be its canonical name for the Random real. The Boolean value \[\|\varphi(\dot{r},a)\|_{\mathbb{B}_{\mathrm{rand}}^{N_a}}\] is represented by a Borel set \(B\subseteq\omega^\omega\), coded in \(N_a\), modulo null sets. If \(z\) is Random over \(N_a\), then the forcing theorem for \(\mathbb{B}_{\mathrm{rand}}^{N_a}\) gives \[z\in B \quad\Longleftrightarrow\quad N_a[z]\models\varphi(z,a).\] The Martin–Solovay tree \(T_2\), together with its absolute complement from Corollary 2, gives the required \(\Sigma^1_3\) generic absoluteness through all forcing extensions used here. Hence, for every \(z\) Random over \(N_a\), \[N_a[z]\models\varphi(z,a) \quad\Longleftrightarrow\quad W^\ast\models\varphi(z,a).\] Thus \(A\) and \(B\) can differ only on \(R_a\), the set of reals which are not Random over \(N_a\). By Lemma 24, \(R_a\) is null. Therefore \(A\triangle B\) is null, and \(A\) is Lebesgue measurable.

The proof of the Baire property is the category analogue. Work in \(N_a\) with ordinary Cohen forcing \(\mathbb{C}^{N_a}\) and let \(\dot{c}\) be its canonical Cohen real. The Boolean value \[\|\varphi(\dot{c},a)\|_{\mathbb{C}^{N_a}}\] is represented, modulo meager sets, by a Borel set \(C\subseteq\omega^\omega\) coded in \(N_a\). If \(z\) is Cohen over \(N_a\), then the forcing theorem gives \[z\in C \quad\Longleftrightarrow\quad N_a[z]\models\varphi(z,a).\] The same \(T_2\)-absoluteness yields \[N_a[z]\models\varphi(z,a) \quad\Longleftrightarrow\quad W^\ast\models\varphi(z,a)\] for every such Cohen real \(z\). Hence \(A\triangle C\subseteq C_a\), where \(C_a\) is the meager set of reals which are not Cohen over \(N_a\). Therefore \(A\) differs from the Borel set \(C\) by a meager set, and \(A\) has the Baire property.

Since the parameter \(a\) was arbitrary, the conclusion holds for all boldface \(\boldsymbol{\Sigma}^1_3\) sets of reals in \(W^\ast\). ◻

Proof. Let \(N=M_1[G]\) be a small generic extension of \(M_1\). Work in \(N\), and let \(A\subseteq\mathbb{R}^2\) be a boldface \(\Sigma^1_3\) relation. The same argument also works for lightface \(\Sigma^1_3\)-relations. Fix a real parameter \(a\) and a \(\Pi^1_2\) formula \(\psi\) such that \[A(x,y)\quad\Longleftrightarrow\quad \exists z\,\psi(a,x,y,z).\] For each real \(x\), put \(s=a\oplus x\). Define \(A^*(x,y)\) to hold iff \[\operatorname{Least}_{\theta}(s,y),\] where \(\theta(s,y,z)\) is the \(\Pi^1_2\) formula obtained from \(\psi(a,x,y,z)\) after decoding \(s=a\oplus x\). By Fact 10(3), the relation \(A^*\) is \(\Sigma^1_3(a)\), hence boldface \(\Sigma^1_3\).

We verify that \(A^*\) uniformizes \(A\). If \(A^*(x,y)\) holds, then by definition there is some \(z\in M_1(a\oplus x)\) such that \[M_1(a\oplus x)\models \psi(a,x,y,z).\] By Fact 10(2), \(N\models\psi(a,x,y,z)\). Hence \(A(x,y)\) holds.

The relation \(A^*\) is single-valued because \(<^1_{a\oplus x}\) is a well-order and \(A^*(x,y)\) asserts that \(y\) is the \(<^1_{a\oplus x}\)-least real in \(M_1(a\oplus x)\) for which a suitable \(z\) exists.

Finally suppose that the \(x\)-section of \(A\) is nonempty in \(N\). Then \[N\models \exists y\exists z\,\psi(a,x,y,z).\] By Fact 10(1), there are witnesses \(y,z\in M_1(a\oplus x)\). Therefore the set of \(<^1_{a\oplus x}\)-candidates is nonempty, so it has a least element. For this least element \(y_0\), Fact 10(3) gives \(A^*(x,y_0)\).

Thus \(A^*\) is a boldface \(\Sigma^1_3\) uniformization of \(A\) in \(N\). The final model \(W^\ast\) is a small generic extension of \(M_1\) by the forcings fixed in the construction, so the final assertion follows. ◻

Proof. Let \(W^\ast=W[G^\ast]\) be the final model obtained from Definition 20. By Lemma 12 and Fact [fact:main-iteration-infty-allowable], the final forcing is a proper, \(\aleph_2\)-c.c. hybrid presentation of length \(\omega_2=\omega_2^{M_1}\) with iterands of size at most \(\aleph_1\). Since \(W\) satisfies \(\mathsf{CH}\), the final forcing has size at most \(\omega_2\). Hence \(W^\ast\models 2^{\aleph_0}\leq\aleph_2\). On the other hand, ordinary Cohen forcing occurs cofinally often in the final presentation, and each such nontrivial coordinate adds a new real. Therefore \(W^\ast\) has at least \(\omega_2\) many reals. Thus \(W^\ast\models 2^{\aleph_0}=\aleph_2\).

Theorem 11 gives the boldface \(\Sigma^1_3\)-uniformization property. Corollary 3 gives the boldface \(\Pi^1_4\)-uniformization property. Lemma 23 gives a \(\Delta^1_4\)-definable well-order of the reals. Finally, Lemma 25 gives Lebesgue measurability and the Baire property for all boldface \(\boldsymbol{\Sigma}^1_3\) sets of reals. These are exactly the asserted conclusions. ◻

Proof. The complexity calculation is the uniform version of the calculation for \(\Phi\) in the \(M_1\) case. A witness to \(\Phi_n(r)\) is a real coding a countable localized presentation together with the associated decoding data. The correctness of the lower-part mouse and of the localized \(M_n\)-initial segment is expressed using the \(\Pi_n\)-iterability analysis from Definition 5, Fact 4, and Lemma 6. Steel’s definability theorem places the relevant verification one projective level above the definition of the \(M_n\)-well-order, hence at level \(\Sigma^1_{n+3}\). The remaining clauses–that the displayed Suslin-tree pattern is present, that the reshaping is correct, and that the almost-disjoint code decodes the reshaped set–are arithmetic or projective of lower complexity relative to that mouse witness. Thus the whole predicate is \(\Sigma^1_{n+3}\).

The exactness assertion is the \(M_n\)-version of Lemma 21. The proof of no unwanted codes uses independence of the Suslin sequence, freshness of the \(M_n\)-Cohen coding areas, and branch omission for selected coordinates. The branch-footprint part is unchanged: the finitely many real names generating a regularity base are read on countable admissible supports, and hence generate only countably many coding areas; the footprint records the selected coordinates coming from those areas. Hence the proof of Lemma 15 applies after replacing \(M_1\) by \(M_n\). Since the two reserved tag forms are excluded from direct coding and are used only by the well-order and uniformization clauses, any final occurrence of \(\Phi_n\) on such a tag is intentional, and every intentional code is read by \(\Phi_n\). ◻

Proof. The first three assertions are formal consequences of the recursive definition, exactly as in Lemmas 16, 17, and 18. The proof uses only the fact that the class at a later derivative stage has more restrictions, that the hybrid presentation can be factored into an initial part and a relative tail, that relative regularity tags carry finitely many real parameters and branch footprints under products, and that the fresh coding areas for a product can be renamed to fresh coordinates. The countable-tail refinement in (2) is the same local-support argument used in the \(M_1\) construction: choose a name for the witness to the relevant \(\Sigma^1_{n+3}\) statement and restrict to the countable complete subpresentation generated by that name, the condition, and the parameters.

For (4), suppose a value has been declared tentative at a successor stage. By definition, every relevant future \(M_n\)-\(\rho\)-allowable tail preserves its membership in the relevant \(\Pi^1_{n+3}\) section. The only possible loss of membership would be witnessed by a \(\Sigma^1_{n+3}\) statement in a later extension. This statement is represented, relative to the real parameters already present, by the canonical tree \(T_{n+1}\) and its Martin–Solovay absolute complement. Lemma 9 therefore gives the same small-generic absoluteness used in the \(T_2\) argument. Hence the proof of Lemma 19 lifts with \(T_2\) replaced by \(T_{n+1}\). ◻

Proof. This is the same countable-tail argument as in Fact [fact:main-iteration-infty-allowable]. The bookkeeping function \(F_n\) supplies cofinally many ordinary Cohen coordinates, cofinally many relative Random and amoeba coordinates for every finite-real-parameter regularity stage once it becomes meaningful, and cofinally many names for the well-order and uniformization tasks. At a relative regularity stage the forcing is the one computed in the witnessed base \(L[T_{n+1},\vec{a}]\). The witness carries the support on which the finitely many real parameters \(\vec{a}\) are read, the countable branch-product support of the \(W_n\)-parameters occurring in those names, and the branch footprint through later tails and products. A second-case uniformization stage appends a countable relative \(M_n\)-\(\infty\)-allowable local hybrid tail rather than a single coordinate. Since \(\kappa_n\) is regular, inserting countable blocks at \(\kappa_n\) many stages still gives a presentation of length at most \(\kappa_n\), and the witnessing bookkeeping functions for the countable tails can be concatenated with the original bookkeeping into one global bookkeeping function. The \(M_n\)-allowability clauses are preserved by this countable-tail construction. ◻

Proof. The proof is the proof of Lemma 22, with the complexity shifted by \(n-1\). We indicate the points where something has to be checked.

Suppose first that a tentative value occurs. By Lemma 27(4), tentative values remain in their \(\Pi^1_{n+3}\) sections through later \(M_n\)-\(\infty\)-allowable tails. Let \(y_0\) be the least tentative value according to the fixed rank and \(M_n\)-localized-presentation order. The bookkeeping revisits every later candidate \(y\) in the same section. Whenever \(y\neq y_0\) is still a member of the \(x\)-section, the uniformization clause intentionally codes the tag \(\langle\mathrm{UF},n,x,y,m\rangle\). By Lemma 26, these intentional codes are exactly the final instances of \(\Phi_n\) on reserved \(\mathrm{UF}\)-tags. The selected value \(y_0\) is never coded with its own \(\mathrm{UF}\)-tag, again by the exactness lemma. This gives the first alternative.

Now suppose that no tentative value occurs. Let \(y\) be any real in the final model and choose a bounded localized name for \(y\). By the cofinality of the bookkeeping, some later uniformization stage considers the corresponding triple \((x,y,m)\). Since no tentative value is available, the construction uses the second case and appends a countable relative \(M_n\)-\(\infty\)-allowable local hybrid tail, restricted below a quotient condition forcing \[(x,y)\notin A^n_m.\] The complement of \(A^n_m\) is \(\Sigma^1_{n+3}\). The witness to this \(\Sigma^1_{n+3}\) statement is preserved through the remaining tail by the \(T_{n+1}\) absoluteness supplied by Lemma 9. Hence \((x,y)\notin A^n_m\) in \(W_n^\ast\). Since \(y\) was arbitrary, the section is empty. ◻

Proof. Since \(A^n_m\) is \(\Pi^1_{n+3}\) and \(\Phi_n\) is \(\Sigma^1_{n+3}\), the displayed relation is \(\Pi^1_{n+3}\). If the \(x\)-section of \(A^n_m\) is empty, then the \(x\)-section of \(U^n_m\) is empty. If the \(x\)-section of \(A^n_m\) is nonempty, Lemma 28 gives a unique value \(y_0\) in the section whose \(\mathrm{UF}\)-tag is not \(\Phi_n\)-coded. Hence \(U^n_m(x,y)\) holds exactly for \(y=y_0\). This is uniformization. The boldface version follows by the usual coding of real parameters into the universal family and by the fact that the bookkeeping ranges over names for those parameters. ◻

Proof. For a real \(z\in W_n^\ast\), let \(\pi_n(z)\) be the least canonical \(M_n\)-localized presentation of a name whose interpretation is \(z\), ordered by the fixed \(M_n\)-well-order of localized presentations. Every real has such a presentation because the final hybrid forcing has countable support and every real name has bounded local support. Distinct reals have distinct least presentations.

Define the underlying order by \[z_0\triangleleft_n z_1 \quad\Longleftrightarrow\quad z_0\neq z_1\;\text{ and }\;\pi_n(z_0)<_{M_n}\pi_n(z_1).\] This is a well-order of the reals. The well-order stages of Definition 24 intentionally code \[\langle\mathrm{WO},n,z_0,z_1\rangle\] exactly when \(z_0\triangleleft_n z_1\). By Lemma 26, for distinct reals \(z_0,z_1\), \[z_0\triangleleft_n z_1 \quad\Longleftrightarrow\quad \Phi_n(\langle\mathrm{WO},n,z_0,z_1\rangle).\] Thus \[z_0<_{\Delta,n}z_1 \quad\Longleftrightarrow\quad z_0\neq z_1\;\land\; \Phi_n(\langle\mathrm{WO},n,z_0,z_1\rangle)\] is a \(\Sigma^1_{n+3}\) definition of the well-order. Since exactly one of the two opposite well-order tags is intentionally coded, the same relation is equivalently given by \[z_0<_{\Delta,n}z_1 \quad\Longleftrightarrow\quad z_0\neq z_1\;\land\; \neg\Phi_n(\langle\mathrm{WO},n,z_1,z_0\rangle).\] This is a \(\Pi^1_{n+3}\) definition. Hence the well-order is \(\Delta^1_{n+3}\). ◻

Proof. Fix \(a\in W_n^\ast\). By the \(M_n\)-version of Lemma 13, choose a countable admissible support \(A\subseteq\kappa_n\) and a \(\mathbb{P}_A\)-name \(\sigma\) such that \[\sigma^{G_A}=a,\] where \(G_A=G^n_\infty\cap\mathbb{P}_A\). Choose \(\beta<\kappa_n\) with \(A\subseteq\beta\). Let \(\dot{a}=\sigma^{\uparrow\beta}\), and let \(\dot{N}\) be the \(\mathbb{P}_\beta\)-name for \(L[T_{n+1},\dot{a}]\). Then the corresponding regularity tags for \(\dot{N}\) are admissibly based. This is the higher-level version of Definition 14, with \[A_{\mathrm{rb}}=A, \qquad k=1, \qquad \dot{a}_0=\sigma, \qquad \dot{W}_{\mathrm{rb}}=L[T_{n+1},\sigma].\] The set \(B^0_{\mathrm{rb}}\) is the countable union of the branch-product supports of the \(W_n\)-parameters occurring in \(\sigma\), and \(\dot{B}_{\mathrm{rb}}\) is the corresponding branch footprint generated by \(B^0_{\mathrm{rb}}\) and by the explicit coding coordinates in \(A\).

By the final bookkeeping, at some stage \(\lambda_{\mathcal{N}}>\beta\) the tag \[(\mathrm{Am}_{\mathcal{N}},\dot{N}^{\uparrow\lambda_{\mathcal{N}}})\] is used. At this stage the forcing is \[\mathbb{A}_{\mathcal{N}}^{N^n_a},\] computed in the interpreted base \(N^n_a\). Let \(Z^{\mathcal{N}}_{n,a}\) be the Borel null set added by this amoeba forcing. By the definition of amoeba forcing for the null ideal, \[B\subseteq Z^{\mathcal{N}}_{n,a}\] for every Borel null set \(B\) coded in \(N^n_a\). Later forcing preserves the Borel code for \(Z^{\mathcal{N}}_{n,a}\) and the statement that it is null. Hence the first displayed inclusion holds in \(W_n^\ast\).

The meager case is the same. The bookkeeping later uses the tag \[(\mathrm{Am}_{\mathcal{M}},\dot{N}^{\uparrow\lambda_{\mathcal{M}}})\] for some \(\lambda_{\mathcal{M}}>\beta\). The forcing \(\mathbb{A}_{\mathcal{M}}^{N^n_a}\) adds a Borel meager set \(Z^{\mathcal{M}}_{n,a}\) covering every Borel meager set coded in \(N^n_a\), and this covering relation remains true in the final extension.

Finally, a real is not Random-generic over \(N^n_a\) iff it belongs to a Borel null set coded in \(N^n_a\). Hence the non-Random reals over \(N^n_a\) are contained in \(Z^{\mathcal{N}}_{n,a}\). Similarly, the non-Cohen reals over \(N^n_a\) are contained in \(Z^{\mathcal{M}}_{n,a}\). This proves the lemma. ◻

Proof. Let \(A\subseteq\omega^\omega\) be \(\Sigma^1_{n+2}(a)\), where \(a\in W_n^\ast\) is a real parameter, and put \(N^n_a=L[T_{n+1},a]\). By Lemma 30, almost every real is Random over \(N^n_a\) and comeagerly many reals are Cohen over \(N^n_a\).

For Lebesgue measurability, work in \(N^n_a\) with the Random algebra \(\mathbb{B}_{\mathrm{rand}}^{N^n_a}\) and let \(\dot{r}\) be the canonical Random real. The Boolean value of the statement “\(\dot{r}\in A\)” is represented, modulo null sets, by a Borel set \(B\) coded in \(N^n_a\). If \(z\) is Random over \(N^n_a\), the forcing theorem for \(\mathbb{B}_{\mathrm{rand}}^{N^n_a}\) gives \[z\in B \quad\Longleftrightarrow\quad N^n_a[z]\models z\in A.\] Since \(A\) is \(\Sigma^1_{n+2}(a)\) and \(T_{n+1}\) is the canonical weakly homogeneous tree representing the universal \(\Sigma^1_{n+2}\) set, Lemma 9 identifies this truth with the truth of \(z\in A\) in the final model. Therefore \(A\triangle B\) is contained in the null set of reals which are not Random over \(N^n_a\). Hence \(A\) is Lebesgue measurable.

For the Baire property, the same argument is carried out in \(N^n_a\) with Cohen forcing. The Boolean value of “\(\dot{c}\in A\)” for the canonical Cohen real is represented by a Borel set \(C\) coded in \(N^n_a\), and for every Cohen real \(z\) over \(N^n_a\) we have \[z\in C \quad\Longleftrightarrow\quad z\in A\] by the same \(T_{n+1}\) absoluteness. Thus \(A\triangle C\) is contained in the meager set of reals which are not Cohen-generic over \(N^n_a\). Hence \(A\) has the Baire property. ◻

Proof. This is the relativized Steel analysis of the canonical mice \(M_n(s)\), in the same form as Fact 10 for \(n=1\). We recall the ingredients in order to make clear that no new coding argument is being used here.

The projective description of the sound initial segments of \(M_n(s)\) is the relativized version of the \(\Pi_n\)-iterability analysis recalled in Section 2. In the codes, the relevant \(s\)-premice are described by a \(\Pi^1_{n+1}(s)\) condition: they are sound, project to \(\omega\), are \(n\)-small over the parameter \(s\), and have the required \(\Pi_n\)-iterability. Steel comparison linearly orders these premice by initial segment and identifies the correctly iterable ones with the initial segments of the canonical mouse \(M_n(s)\).

The usual comparison-and-capture argument then gives the first two clauses. If a small generic extension satisfies a \(\Sigma^1_{n+2}(s)\) assertion, write it in the form \(\exists u\exists v\,\theta(s,u,v)\) with \(\theta\) \(\Pi^1_{n+1}\). The tree or mouse witnessing this assertion is captured by a countable initial segment of \(M_n(s)\); otherwise comparison with the canonical construction would produce the same contradiction as in Steel’s proof of the projective correctness of \(M_n(s)\). Conversely, once the witnesses belong to \(M_n(s)\), \(\Pi^1_{n+1}\) correctness follows from the same comparison theorem and the preservation convention for the generic extensions considered here.

Finally, define \(<_{n,s}\) by first taking the least sound initial segment of \(M_n(s)\) containing the real in question, and then using the canonical well-order of that premouse. Since membership in the relevant initial segment class is \(\Pi^1_{n+1}(s)\) and comparison gives initial-segment linearity, initial segments of \(<_{n,s}\) are uniformly \(\Sigma^1_{n+2}(s)\). Therefore least-witness assertions for \(\Pi^1_{n+1}\) matrices are again \(\Sigma^1_{n+2}(s)\). ◻

Proof. Let \(N\) be a small generic extension of \(M_n\). Work in \(N\), and let \(A\subseteq\mathbb{R}^2\) be a boldface \(\Sigma^1_{n+2}\) relation. Choose a real parameter \(a\) and a \(\Pi^1_{n+1}\) formula \(\psi\) such that \[A(x,y) \quad\Longleftrightarrow\quad \exists z\,\psi(a,x,y,z).\] For each real \(x\), put \(s=a\oplus x\), and let \(\theta(s,y,z)\) be the \(\Pi^1_{n+1}\) formula obtained from \(\psi(a,x,y,z)\) after decoding \(s\) as \(a\oplus x\). Define \(U(x,y)\) to hold iff \[\operatorname{Least}^{n}_{\theta}(a\oplus x,y).\] By Proposition 14(3), \(U\) is \(\Sigma^1_{n+2}(a)\), hence boldface \(\Sigma^1_{n+2}\).

If \(U(x,y)\) holds, then for some \(z\in M_n(a\oplus x)\), \[M_n(a\oplus x)\models\psi(a,x,y,z).\] By Proposition 14(2), \(N\models\psi(a,x,y,z)\), and therefore \(A(x,y)\) holds. Thus \(U\subseteq A\).

The relation \(U\) is single-valued because \(<_{n,a\oplus x}\) is a well-order and \(U(x,y)\) asserts that \(y\) is the least real in \(M_n(a\oplus x)\) for which a suitable \(z\) exists.

Finally suppose that the \(x\)-section of \(A\) is nonempty in \(N\). Then \[N\models\exists y\exists z\,\psi(a,x,y,z).\] By Proposition 14(1), there are witnesses \(y,z\in M_n(a\oplus x)\). Hence the set of \(<_{n,a\oplus x}\)-candidates is nonempty, and it has a least element \(y_0\). By definition, \(U(x,y_0)\) holds. Thus \(U\) uniformizes \(A\). ◻

Proof. Let \(W_n^\ast\) be the final extension from Definition 24. The forcing has length \(\kappa_n=(\omega_2)^{M_n}\), preserves \(\omega_1\), has the \(\aleph_2\)-chain condition by the same size and \(\Delta\)-system argument used in Lemma 12, and every iterand has size at most \(\aleph_1\) in the relevant intermediate model. Since the preparatory model satisfies \(\mathsf{CH}\), the final forcing has size at most \(\kappa_n\), so \[W_n^\ast\models 2^{\aleph_0}\leq\aleph_2.\] Cofinally many ordinary Cohen coordinates add new reals, and hence \(W_n^\ast\) has at least \(\kappa_n\) many reals. Therefore \[W_n^\ast\models 2^{\aleph_0}=\aleph_2.\]

Theorem 15 gives \(\Sigma^1_{n+2}\)-uniformization. Corollary 4 gives \(\Pi^1_{n+3}\)-uniformization. Lemma 29 gives a \(\Delta^1_{n+3}\) well-order of the reals. Lemma 31 gives Lebesgue measurability and the Baire property for all boldface \(\boldsymbol{\Sigma}^1_{n+2}\) sets of reals. This proves the theorem. ◻