The Good-Tree-Watson symmetric model is closed under omega-sequences from the full extension

Choose in $M$ a name $\dot{g}$ for $g$. By the truth lemma choose $p\in H$ forcing that $\dot{g}$ is a function on $\check{\beta }$. For each $\xi <\beta$, define in $M$ the downward-closed set $D_{\xi }=\{q\le p:\text{ for some }\tau \in {\mathrm{H}\mathrm{S}}^M,q⊩\dot{g}(\check{\xi })=\tau \}\mathrm{.}$ These are sets by Separation: HS is a definable ground class and forcing is definable for this fixed formula. They are downward closed by [F5]. Each $H\cap D_{\xi }$ is nonempty: $g(\xi )\in N$ has an HS name, the truth lemma gives a member of $H$ forcing the equality, and directedness combines it with $p$. This does not yet choose a simultaneous sequence of names or conditions.

Put $E_{\xi }=D_{\xi }\cup \{q\le p:\text{ no }r\le q\text{ belongs to }{D}_{\xi }\}\mathrm{.}$ Each $E_{\xi }$ is downward closed and dense below $p$: either a stronger member of $D_{\xi }$ exists or the condition is already in the second part. Their intersection is dense below $p$. Indeed, from any $r\le p$ run a recursion of length $\beta$: at stage $\xi$ choose the least extension in $E_{\xi }$ in a fixed ground well-order of $P$; at limit stages take the union of the preceding partial functions. The final union at $\beta$ is a condition by [F1], is stronger than $r$, and remains in every earlier $E_{\xi }$ by downward closure. For $\beta =0$ retain $r$. This is one ground recursion licensed by [F4]; it spends ground AC in the well-order of $P$.

By genericity [F5], fix $q\in H\cap {\bigcap }_{\xi <\beta }{E}_{\xi }$ with $q\le p$. In fact $q\in D_{\xi }$ for every $\xi$: step 1.1 supplies some $r_{\xi }\in H\cap D_{\xi }$, and directedness gives a common stronger member of $H$ below $q,r_{\xi }$, lying in $D_{\xi }$. Thus $q$ cannot be in the part of $E_{\xi }$ that forbids all stronger $D_{\xi }$ conditions. All coordinates can now be represented below the same actual generic condition $q$.

Work in $M$ with this condition $q$. For each $\xi <\beta$ choose a pair $({\tau }_{\xi },e_{\xi })$ such that ${\tau }_{\xi }$ is HS, $\mathrm{\mid }{e}_{\xi }{\mathrm{\mid }}^M<\lambda$, $e_{\xi }$ supports ${\tau }_{\xi }$, and $q⊩\dot{g}(\check{\xi })={\tau }_{\xi }$. Such witnesses exist by step 3.1 and [F3]. This is set-sized choice: Collection first bounds witnesses for the set of indices in one ground set, and ground AC chooses from its nonempty witness subsets. Hence the sequences of names and supports belong to $M$ without selecting from a proper class. Put $e={\bigcup }_{\xi <\beta }{e}_{\xi }$. Ground regularity of $\lambda$ and ground AC imply $\mathrm{\mid }e{\mathrm{\mid }}^M<\lambda$.

Use [F6] to form in $M$ the graph name $\dot{k}$ from the names $\check{\xi },{\tau }_{\xi }$. Each automorphism in $\mathrm{fix}(e)$ fixes every ${\tau }_{\xi }$ and check name, and therefore fixes $\dot{k}$. The pair and set-name constructions use only HS constituent names, all of $P$ and finite set operations; their subnames are HS recursively. Thus $\dot{k}$ is hereditarily symmetric, not just supported. The empty graph is covered by the same construction.

Since $q\in H$, every forced equality of step 4.1 holds after evaluation. Consequently $(\dot{k}{)}_H=\{⟨\xi ,g(\xi )⟩:\xi <\beta \}=g$. By step 5.1 and [F3], $g\in N$. This proves the assertion for all ground ordinals $\beta <\lambda$, including $\omega$ when $\lambda ={\omega }_1^M$. Forcing does not add ordinals, so these are exactly the ordinals below the fixed ordinal $\lambda$ in the extension; no assumption that an extension sequence of ground names is already available was needed.