Composition with universal-meagre forcing preserves sweetness

Enumerate, with repetitions allowed, all old equivalence classes as $\{A_m:m<\omega \}$. For $p\in D$ define $k_m(p)$ to be the least $k$ such that every $p^{\mathrm{\prime }}<msubsup><mi>E</mi><mi>k</mi><mi>P</mi></msubsup>p$ has the following property: $A_m\cap (P\downarrow p)\mathrm{\ne }\mathrm{\varnothing }⟹A_m\cap (P\downarrow p^{\mathrm{\prime }})\mathrm{\ne }\mathrm{\varnothing }\mathrm{.}$ If the left side is empty this is vacuous. Otherwise, writing $A_m$ as an old equivalence class, the transfer clause gives such a $k$. This is the source's clause $(\epsilon )$ modulus.

Shelah's source works with local conditions $(p,(t,\dot{T}))$ satisfying only $p⊩(t,\dot{T})\in \mathrm{U}\mathrm{M}$. Strengthen any iteration condition to decide the finite record $t$, make the second coordinate nontrivial, and put the first coordinate in $D$. By [A1] and the normalization theorem in Two-step forcing iterations, replace the resulting local second-coordinate name by a name in its set $R$ that is forced equal below $p$. Do this after every later conditional union as well, always below the constructed first coordinate. Substitution for forced equality shows that these normalized representatives have exactly the local order comparisons used in the source, so they form a dense presentation $D^{\ast }$ of the restricted iteration. In particular, no name is required to be a UM condition under $1_P$. For $x_j=(p_j,(t_j,{\dot{T}}_j))$, $j=1,2$, define $x_1{E}_n^{\ast }{x}_2$ by the following five clauses from the source composition result [F5]:

The five clauses define refining equivalence relations with countably many classes. At a fixed $n$ they record an old $E_n^P$-class, one finite tree, finitely many cone-meeting bits, finitely many nonmembership bits on $2^n$, and finitely many natural-number moduli and old classes. Transitivity of $(\delta )$ uses $(\gamma )$ to ensure that the same active $A_m$ is being compared; transitivity of $(\epsilon )$ uses directedness of $A_m$ together with the definition of $k_m$. For refinement, exclusion of a length-$n$ word from a pruned binary tree is equivalent to exclusion of both its children. If separate members of an active directed $A_m$ force the two exclusions, a common strengthening inside $A_m$ forces both. Thus equality of the length-$(n+1)$ exclusion traces implies equality at length $n$; all other recorded data restrict directly.

The stability subclaim recorded in [F5] is the fixed-model strengthening interface used repeatedly below. Put $K=\max (\{n\}\cup \{k_m(p):m<n\})$. If $p^{\mathrm{\prime }}<msubsup><mi>E</mi><mi>K</mi><mi>P</mi></msubsup>p$ and $p^{\mathrm{\prime }}\le p$, then for every canonical UM condition $(p,(t,\dot{T}))\in D^{\ast }$ one has $(p^{\mathrm{\prime }},(t,\dot{T}))\in D^{\ast }$ and $(p^{\mathrm{\prime }},(t,\dot{T}))E_n^{\ast }(p,(t,\dot{T}))$; moreover the cone below $p^{\mathrm{\prime }}$ meets $A_m$ iff the cone below $p$ meets $A_m$ for every $m<n$. The forward direction is immediate from $p^{\mathrm{\prime }}\le p$, and the reverse direction is exactly the defining property of $k_m(p)$.

Downward directedness now has a legitimate common condition. For two $E_n^{\ast }$-equivalent members, use the old directed class at the maximum of $n$ and their finitely many common $k_m$ values to obtain $p^{\ast }\le p_1,p_2$. The stability subclaim [F5] preserves all active $A_m$ traces. Clause $(\beta )$ gives one recorded tree $t$, while $(\delta )$ ensures that the two witness-tree names have compatible finite membership requirements. Their union below $p^{\ast }$ is a perfect nowhere-dense witness tree with recorded part $t$, by the exact UM compatibility calculation in [F2]. Normalize this local union name below $p^{\ast }$ as in step 1.2; the resulting member of $D^{\ast }$ is a common lower bound in the same $E_n^{\ast }$-class.

For the sequential clause, suppose $x_i{E}_i^{\ast }{x}_{\omega }$ for every $i<\omega$ and fix a tail $i\ge n$. Put $K=\max (\{n\}\cup \{k_m(p_{\omega }):m<n\})$. All first coordinates in the tail lie in the $E_K^P$-class of $p_{\omega }$ by the five clauses. The old sequential clause supplies a bound of the tail from index $K$ in that class; class directedness combines it with the finitely many first coordinates with $n\le i<K$. This gives $p^{\ast }\in D$ below all first coordinates in the tail and in the required old class. All recorded trees equal one finite $t$. Define the source's local conditional name ${\dot{T}}^{\ast }=\{\begin{array}{ll}{\bigcup }_{n\le i\le \omega }{\dot{T}}_i,& p^{\ast }\in {\dot{G}}_P,\\ {\dot{T}}_{\omega },& p^{\ast }\mathrm{\notin }{\dot{G}}_P\mathrm{.}\end{array}$ The finite initial-tree and perfectness clauses are immediate. Nowhere density is not inferred from the finite data. Given a ground node $\eta$ and a condition below $p^{\ast }$, first strengthen it to force some extension $\nu \supseteq \eta$ out of ${\dot{T}}_{\omega }$. For each sufficiently large $i$, choose the largest old equivalence level $\mathrm{\ell }(i)<i$ represented by a class $A_{m(i)}$ with $m(i)<i$ through that strengthening. The sequence $\mathrm{\ell }(i)$ is nondecreasing and unbounded. Clauses $(\gamma )$ and $(\delta )$ transfer the exclusion of all finitely many length-$i$ extensions of $\nu$ to a condition in $A_{m(i)}$ below $p_i$. On each finite block where $\mathrm{\ell }(i)$ is constant, directedness gives one condition in the corresponding old class; the old sequential clause diagonalises those block conditions to one lower bound. Finally finitely many early indices are handled successively using the nowhere density of their individual tree names. The resulting condition forces one extension of $\eta$ outside every ${\dot{T}}_i$, hence outside ${\dot{T}}^{\ast }$. This is the full source diagonal recorded in [F5], and it proves that $(p^{\ast },(t,{\dot{T}}^{\ast }))$ is a local UM condition below the whole tail. Normalize it below $p^{\ast }$ by step 1.2. Repeating the finite trace argument verifies clauses $(\gamma )$ and $(\delta )$ against $x_{\omega }$, so the normalized bound lies in its $E_n^{\ast }$-class.

For transfer, take $(q,(s,\dot{S}))\le (p,(t,\dot{T}))$ and a target level $n$. The source proof [F5] first chooses the old transfer modulus for $p,q$ after incorporating the finitely many $k_m(q)$, then enlarges it past the index of the old class containing $q$ and past the height of $s$. For an $E_k^{\ast }$-perturbation $(p^{\mathrm{\prime }},(t,{\dot{T}}^{\mathrm{\prime }}))$, the old transfer clause produces $p^{\ast }$ in the required old class below $p^{\mathrm{\prime }}$ and $q$. The source uses the local conditional name ${\dot{S}}^{\ast }=\{\begin{array}{ll}\dot{S}\cup {\dot{T}}^{\mathrm{\prime }},& p^{\ast }\in {\dot{G}}_P,\\ \dot{S},& p^{\ast }\mathrm{\notin }{\dot{G}}_P\mathrm{.}\end{array}$ The extra height qualification ensures that every node outside the recorded tree $s$ is tested by the level-$k$ $(\delta )$ trace. Together with $(\gamma )$, directedness of the active $A_m$, and the stability subclaim [F5], this proves that $(p^{\ast },(s,{\dot{S}}^{\ast }))$ is a local UM condition, lies below both inputs, and is $E_n^{\ast }$-equivalent to $(q,(s,\dot{S}))$. Normalize it below $p^{\ast }$ by step 1.2 to obtain the required restricted-iteration condition. This is the source transfer argument; the qualification cannot be replaced by agreement of initial trees alone.

Steps 2.1--3.3 prove that $(P\ast \dot{\mathrm{U}\mathrm{M}},D^{\ast },(E_n^{\ast }))$ is sweet. They do not yet prove that this presentation extends the fixed old model. The fixed-model result recorded in [F5] supplies that separate step: replace $D^{\ast }$ by a dense-open presentation disjoint from the canonical old dense set, adjoin the old $D$, and use $E_n^{\ast }$ on the new piece and $E_n^P$ on the old piece, with no cross-piece equivalences. The only mixed transfer case is settled using the stability subclaim [F5] and the comparable transfer clause of [F1]. The fixed-model result then checks all five extension conditions, including that a new class meeting $D$ is contained in $P$ and that a member of the new dense set lying above an old condition was already old. Thus the resulting sweetness model extends the given one.

If the second forcing is presented under a specified $P$-forced order isomorphism with canonical UM, pull the concrete conditions, nonmembership traces, and the five clauses back along that isomorphism. No inference from bare forcing equivalence to sweetness is made. Steps 3.1--4.1 establish the two conclusions of the Statement.