A closed Easton tail adds no short sequences across its chain-condition head

Choose a $P\times Q$-name $\dot{f}\in M$ with $f={\mathrm{val}}_{G\times H}(\dot{f})$, and put $\rho ={\mathrm{rk}}_{P\times Q}(\dot{f})$. By [F4], $\mathrm{rank}(f)\le \rho$. Every value $f(\alpha )$ belongs to $M$ and has rank below $\rho +1$; transitivity of $M$ therefore puts it in the ground set $A:=V_{\rho +1}^M$. The product extension satisfies ZFC by [F4], so the truth lemma supplies $r=(p_r,q_r)\in G\times H$ forcing that $\dot{f}$ is a function from $\check{\lambda }$ into $\check{A}$. We will only use forcing below $r$.

Form the cones $P_r=\{p\in P:p\le p_r\}$ and $Q_r=\{q\in Q:q\le q_r\}$ in $M$. They are nonempty. Every descending sequence in $P_r$ of length below ${\lambda }^{+}$ has a lower bound still in $P_r$ (include $p_r$ when the sequence is empty); every pairwise-incompatible subset of $Q_r$ is one of $Q$, so $Q_r$ is ${\lambda }^{+}$-cc. Here a maximal antichain of $Q_r$ means a pairwise-incompatible subset $W$ such that every member of $Q_r$ is compatible with some member of $W$. This agrees with maximality by inclusion: a condition incompatible with all of $W$ could be added, and conversely.

For each $\alpha <\lambda$ let $D_{\alpha }\subseteq P_r$ be the set of $p$ for which there are a maximal antichain $W\subseteq Q_r$ and $a:W\to A$ such that $(p,q)⊩\dot{f}(\check{\alpha })=\check{a(q)}$ for every $q\in W$. The coordinate notation abbreviates the fixed first-order formula saying that $\dot{f}$ has value $\check{a(q)}$ at $\check{\alpha }$; no function-value term is added to the forcing language. This forcing relation is definable in $M$, and $W$ and $a$ range over ground sets, so Separation gives $D_{\alpha }\in M$. Monotonicity makes $D_{\alpha }$ downward closed in $P_r$.

Fix $p_0\in P_r$. Recursively, for $\gamma <{\lambda }^{+}$, suppose $⟨(p_{\xi },q_{\xi },a_{\xi }):\xi <\gamma ⟩$ has been chosen with the $p_{\xi }$ descending and the $q_{\xi }$ pairwise incompatible. If $W_{\gamma }=\{q_{\xi }:\xi <\gamma \}$ is maximal in $Q_r$, stop. Otherwise choose $q^{\mathrm{\prime }}\in Q_r$ incompatible with every member of $W_{\gamma }$. Closure gives $\bar{p}\in P_r$ below $p_0$ and every preceding $p_{\xi }$, since their number is below ${\lambda }^{+}$. Because $(\bar{p},q^{\mathrm{\prime }})\le r$ forces that the value of $\dot{f}$ at $\check{\alpha }$ lies in $\check{A}$, the existential-name clause first gives, densely below $(\bar{p},q^{\mathrm{\prime }})$, a name $\sigma$ forced to be that value and to belong to $\check{A}$. The atomic membership clause for $\check{A}$ then gives a further pair $(p_{\gamma },q_{\gamma })\le (\bar{p},q^{\mathrm{\prime }})$ and $a_{\gamma }\in A$ forcing $\sigma =\check{a_{\gamma }}$, hence $\dot{f}(\check{\alpha })=\check{a_{\gamma }}$. In particular $q_{\gamma }$ remains incompatible with all earlier $q_{\xi }$. The selected triples lie in the ground set $P_r\times Q_r\times A$; Choice in $M$ well-orders this set and makes the recursion deterministic. No choice from the proper class of all names is needed.

The recursion stops at some $\beta <{\lambda }^{+}$: otherwise the distinct $q_{\gamma }$, $\gamma <{\lambda }^{+}$, form a pairwise-incompatible subset of $Q_r$ of size ${\lambda }^{+}$. At the stopping stage $W_{\beta }$ is maximal. Closure supplies $p^{†}\in P_r$ below $p_0$ and every $p_{\xi }$ for $\xi <\beta$. Monotonicity then gives $(p^{†},q_{\xi })⊩\dot{f}(\check{\alpha })=\check{a_{\xi }}$ for all $\xi <\beta$, so $W_{\beta }$ and $a(q_{\xi })=a_{\xi }$ witness $p^{†}\in D_{\alpha }$. Thus every $D_{\alpha }$ is dense open in $P_r$.

The intersection $D={\bigcap }_{\alpha <\lambda }{D}_{\alpha }$ belongs to $M$ and is dense open in $P_r$. Indeed, starting below any $p\in P_r$, use [F5] to meet $D_{\alpha }$ successively for $\alpha <\lambda$, taking lower bounds at limits and at the end. All these sequences have length at most $\lambda <{\lambda }^{+}$; downward closure keeps the final condition in every $D_{\alpha }$.

The projection $G$ is $M$-generic for $P$: if $E\in M$ is dense in $P$, then $E\times Q$ is dense in $P\times Q$ and the product generic meets it. To meet the cone-dense set $D$, use the global dense set $E_D=D\cup \{p\in P:p\perp p_r\}$: if $p$ is compatible with $p_r$, first strengthen into $P_r$ and then into $D$. Since $p_r\in G$ and a filter cannot contain incompatible conditions, $G\cap E_D\subseteq D$. Fix $p^{\ast }\in G\cap D$. Choice in $M$ selects, for all $\alpha <\lambda$, witnesses $(W_{\alpha },a_{\alpha })$ to $p^{\ast }\in D_{\alpha }$; their full sequence belongs to $M$.

Similarly $H$ is $M$-generic for $Q$. For each $\alpha$, the downward closure of $W_{\alpha }$ is dense in $Q_r$: compatibility with a member of the maximal antichain yields a common stronger condition. Lifting this cone-dense set to $Q$ by adjoining conditions incompatible with $q_r$ shows that $H$ meets it. Upward closure then gives some $w_{\alpha }\in H\cap W_{\alpha }$, and downward directedness makes $w_{\alpha }$ unique because distinct members of $W_{\alpha }$ are incompatible.

For each $\alpha <\lambda$, $(p^{\ast },w_{\alpha })\in G\times H$ forces $\dot{f}(\check{\alpha })=\check{a_{\alpha }(w_{\alpha })}$, so the truth lemma gives $f(\alpha )=a_{\alpha }(w_{\alpha })$. The ground sequence $⟨(W_{\alpha },a_{\alpha }):\alpha <\lambda ⟩$ and $H$ belong to $M[H]$, which satisfies ZFC by [F4]. Its Separation and Replacement therefore construct $\alpha \mapsto a_{\alpha }(w_{\alpha })$ there. This function is $f$, hence $f\in M[H]$. Characteristic functions and cofinal maps are special cases of such sequences, proving the stated relative conclusions. ∎