Neighborhoods of Rudin initial-top slices contain tails

If $k<2$, there are no $n\in B$ with $n\le k$, so $F_k=X$ and $U=X$. The zero function belongs to the displayed product, and its tail in $X$ is contained in $U$. Suppose henceforth $k\ge 2$. Apply F1 and A1 with $U,X,B,P_B,t$ among the parameters. The resulting $M$ contains all these objects, and $x\in F_k$. For every finite $S\subseteq \{n\in B:n>k\}$ define $x^S$ by replacing $x(n)$ by ${\mathrm{\aleph }}_n$ on $S$ and leaving it unchanged elsewhere. This point remains in $F_k$: it still has the prescribed initial tops, all unchanged coordinates have cofinality at most ${\mathrm{\aleph }}_k$, and its finitely many new top cofinalities are the finite alephs ${\mathrm{\aleph }}_n$ for $n\in S$, by F3. A finite bound larger than $k$ and every member of $S$ bounds all these cofinalities strictly. Thus $x^S\in X$ and hence $x^S\in U$.

There are countably many finite $S$ as in step 1.1: the map $S\mapsto {\sum }_{n\in S}{2}^n$ takes them injectively to the natural numbers. For distinct sets, let $d$ be the greatest member of their symmetric difference. The contribution $2^d$ to the difference of their sums exceeds the sum of all possible smaller contributions, since ${\sum }_{i<d}{2}^i=2^d-1$ (the identity follows by induction from the zero empty sum). Thus the codes differ. By F2 and A1 choose, for every such $S$, a function $y^S<x^S$ with $(y^S,x^S{]}_X\subseteq U$. For $n\in B$ put

Let $u\in M\cap X$ satisfy $z<u$. Set $S=\{n\in B:n>k\text{ and }u(n)={\mathrm{\aleph }}_n\}$. The defining Rudin condition gives a finite $q$ with every coordinate cofinality of $u$ below ${\mathrm{\aleph }}_q$. If $n\in S$, F3 gives ${\mathrm{\aleph }}_n=\mathrm{cf}(u(n))<{\mathrm{\aleph }}_q$, so $n<q$. Hence $S$ is finite. For tail coordinates outside $S$, $u(n)<{\mathrm{\aleph }}_n$ and F1 yields $u(n)<x(n)=x^S(n)$. For coordinates in $S$, $u(n)=x^S(n)={\mathrm{\aleph }}_n$. At initial coordinates $u(n)\le {\mathrm{\aleph }}_n=x^S(n)$. Thus $u\le x^S$. If $n\mathrm{\notin }S$, step 2.1 gives $u(n)>z(n)>b(n)\ge y^S(n)$; if $n\in S$, $u(n)=x^S(n)>y^S(n)$. Therefore $u\in (y^S,x^S{]}_X\subseteq U$. This treats every internal Rudin point above $z$, including those attaining some tail tops.

Suppose there were an external $u\in X\setminus U$ with $z<u$. The assertion that such a $u$ exists is true in $V_{\theta }$: $X,U,z,B$ belong to it, every member of $X$ is in it by F5, and the conditions $u\in X$, $u\mathrm{\notin }U$ and $z(n)<u(n)$ for all $n\in B$ use only membership and bounded function-coordinate comparisons. Transitivity makes these conditions absolute, as bounded quantifiers range over all actual members of their bounds and function values are the actual entries. All their parameters belong to $M$, by steps 1.1–2.1. Elementarity F1 therefore gives a witness in $M$ with the same actual properties, contradicting step 3.1. There is no such witness, which proves the full pointwise tail inclusion. QED.