Restriction, amalgamation, and the set-sized Prikry property

Put $U\upharpoonright a=\{q\upharpoonright a:q\in U\}$. For a Gitik condition $(p,U)$, clauses 1–4 and 7–9 of F1 plainly survive restriction to a closed support. For the small-coordinate successor clause, lift a projected trunk $r$ and use clause 7 to replace its lift by one agreeing with $p$ off $a$; the old measure-one successor set is contained in the projected one. For union/tree monotonicity, use the lifts $p\cup r_i$ and clause 6 before projecting. For predecessors, choose a lift with the least finite number of added triples; clause 10's last triple must then lie in the projection. Thus $(p\upharpoonright a,U\upharpoonright a)$ is a condition.

If $s\in U$, the cone $U_s=\{t\in U:s\subseteq t\}$ satisfies all ten clauses: clauses 5–7 follow by first adjoining the small part of $s$ with clauses 6–7, and the remaining clauses are inherited. If $b\supseteq {\mathrm{dom}}_1(p)$ is finite and closed under ${\mathrm{cf}}^{\mathrm{\prime }}$, extending every trunk coherently to $b$ gives a condition by the same clause-by-clause induction. Two upper trees with a common trunk may be intersected because every relevant coordinate filter is closed under finite intersections. Combining these operations aligns compatible trunks on the union of two finite closed supports and then intersects their upper trees, proving the asserted amalgamation.

Let $A\subseteq P_{\theta }$ be a maximal antichain and $c=(p,U)\in P_3$. The restriction $c\upharpoonright \theta$ is compatible with some $r\in A$; take a common refinement $d=(q,V)\in P_{\theta }$ and first directly lengthen its finitely many trunk sections to a common finite length. Choose $t\in U$ whose restriction to the old coordinates below $\theta$ is the corresponding part of $q$, and pass to the cone above $t$. The union $t\cup q$ is a coherent trunk: on the overlap the two functions agree, while outside it their coordinate domains are disjoint. Support extension and intersection of the two lifted upper trees, as in step 2.1, produce a condition refining both $c$ and $d$, hence both $c$ and $r$. Thus every maximal antichain of $P_{\theta }$ remains maximal in $P_3$, which is the complete-subforcing assertion. If $G\subseteq P_3$ is generic for the ground-definable dense classes, $G_{\theta }=G\cap P_{\theta }$ consequently meets every ground dense subset of $P_{\theta }$. Finally, the transitive closure of a set name is a set; the union of the finite coordinate supports of all conditions occurring in it is therefore a set of ordinals and is bounded by a regular $\theta$. Induction on name rank makes the name a $P_{\theta }$-name. Evaluating it uses only $G_{\theta }$, proving the displayed union of extensions.

Work below a fixed condition on $a$. For every type-2 tail coordinate $\alpha \in a\setminus \kappa$ whose ${\mathrm{cf}}^{\mathrm{\prime }}(\alpha )$ coordinate lies below $\kappa$, choose the least index ${\lambda }_{\alpha }$ for which ${\kappa }_{{\lambda }_{\alpha }}^{\alpha }\ge \kappa$. Prune the lower-coordinate successor sets so that every later value used as an index is at least the maximum of the finitely many relevant ${\lambda }_{\alpha }$. This is dense by the uniformity of those successor filters. Call the resulting dense set $J$. On $J$, split every trunk as $r=r_0\cup r_1$ below and above $\kappa$. Map $(r,R)$ to its lower restriction $(r_0,R_0)$ together with the lower-forcing name whose pairs are the tail projections $r^{\mathrm{\prime }}\upharpoonright (a\setminus \kappa )$, placed under the lower trunk condition $R_0\uparrow (r^{\mathrm{\prime }}\upharpoonright (a\cap \kappa ))$. Clauses 8–10 in F1 say exactly that this name evaluates to a tail condition with $\kappa$-complete successor filters. Conversely, strengthen a proposed pair in $E\ast \dot{Q}$ to decide its tail trunk, follow its lower tree below $\kappa$, and recursively admit a successor $\xi$ above $\kappa$ precisely when some lower refinement forces that tail successor into the named tree. The forced measure-one clauses supply a ground measure-one subset at every node, so the reconstructed combined tree is a condition in $J$. The two constructions preserve restriction and tree inclusion and the second refines every proposed iteration condition; hence this is a dense embedding.

The lower forcing $E$ has size $\mu <\kappa$: it uses finitely many coordinates below the inaccessible $\kappa$; F3 bounds the finite products of possible triples, and the strong-limit part of F2 bounds the power sets coding their upper trees. Let $H$ be $E$-generic and let $U$ be any ground $\kappa$-complete tail ultrafilter. In the extension define $U^{\ast }=\{X:(\mathrm{\exists }Y\in U)Y\subseteq X\}$. To decide a new $X\subseteq I$ below any lower condition, choose for every $i\in I$ a stronger condition deciding $i\in \dot{X}$ and partition $I$ by the deciding condition and truth value. There are fewer than $\kappa$ cells, so $\kappa$-completeness and ultrafilterhood put one cell in $U$; the corresponding condition forces that cell into $X$ or its complement. These conditions are dense, so $U^{\ast }$ is an ultrafilter. For a sequence of $\delta <\kappa$ members of $U^{\ast }$, maximal antichains of size at most $\mu$ list ground witnesses for each member. Intersecting all fewer than $\kappa$ listed witnesses gives one ground $U$-set contained in their intersection. Thus $U^{\ast }$ is $\kappa$-complete in $M[H]$.

A descending sequence of fewer than $\kappa$ fixed-trunk tail conditions has a lower bound obtained by intersecting their trees. At every surviving node the successor set is the intersection of fewer than $\kappa$ members of the relevant $U^{\ast }$ and is therefore measure one by step 4.1; predecessor and coherence clauses survive intersection. This is precisely $\kappa$-closure in F6. The empty tail is the trivial forcing and satisfies the same conclusion.

Fix $(s,S)\in Q$ and a sentence $\phi$. Cycle from left to right through the finitely many tail coordinates, thereby enumerating the unfilled slots and levels above $s$. At a level $j$, colour a trunk $r$ by $0$, $1$, or $2$ according as some upper subtree with trunk $r$ forces $\phi$, forces $\mathrm{\neg }\phi$, or neither; same-trunk intersection makes the first two alternatives exclusive. Define the colour at earlier levels backwards: at a node $r$, take the unique colour whose successor set is in the ultrafilter at $r$. Countable completeness permits simultaneous intersection over all later levels, and AC chooses these prunings at every node, producing one tree $W\subseteq S$. If two extensions of $(s,W)$ forced opposite alternatives, extend the shorter trunk through finitely many measure-one intersections until both trunks have the same level. Backward homogeneity then assigns them the same colour, a contradiction. By decision density, some extension decides $\phi$; since the opposite alternative occurs nowhere below $(s,W)$, its chosen alternative is dense there, and F4 makes $(s,W)$ itself decide it without changing $s$.

Let $\gamma <\kappa$ and suppose a tail condition forces $\dot{x}\subseteq \gamma$. Recursively apply step 6.1 to decide each statement ``$\xi \in \dot{x}$'' by a fixed-trunk refinement. At limit stages below $\gamma$, and once more at the end, use the direct $\kappa$-closure from step 5.1. The final condition decides all memberships; Separation in the lower extension forms the corresponding set $x\subseteq \gamma$, and F4 gives that the condition forces $\dot{x}=\check{x}$. This includes $\gamma =0$ (the original condition and the empty set) and proves that $Q$ adds no bounded subsets below its completeness bound.