Hereditarily symmetric names have bounded layer support

Let $\dot{x}$ be hereditarily symmetric. Its stabilizer belongs to $\mathcal{F}$. By the definition of the upward closure in F1, some $H_m$ is contained in $\mathrm{sym}(\dot{x})$. Thus every $\pi \in H_m$ fixes $\dot{x}$. Notice that this selects one natural number for one given name; it does not choose supports simultaneously for a family.

Now let $x\subseteq \omega$ belong to $N$, and choose one hereditarily symmetric name $\dot{x}$ with value $x$ in the supplied generic. By step 1.1 fix $m$ such that $H_m$ fixes $\dot{x}$. In the complete Boolean algebra $B$ from F2 put $b_k=\parallel \check{k}\in \dot{x}{\parallel }_B$ for $k<\omega$ and form the Boolean name $\dot{y}=\{⟨\check{k},b_k⟩:k<\omega \}$. By F4, the supplied Boolean generic contains $b_k$ exactly when $k\in {\dot{x}}_G=x$. Hence ${\dot{y}}_G=\{k:b_k\in G\}=x$. This proves equality of the two values in the fixed generic; it does not assert that an arbitrary name which happens to evaluate to a real is forced to be a real in every generic.

Make the Boolean action explicit. In the regular-open presentation from F2, $\widehat{\pi }(U)=\pi \mathrm{‘}\mathrm{‘}U$ preserves arbitrary unions followed by regularization, intersections, and complements, and so is a complete Boolean automorphism extending $p\mapsto \pi p$. The truth value $b_k$ is the regular open generated by conditions forcing $\check{k}\in \dot{x}$. If $\pi \in H_m$, then $\pi \check{k}=\check{k}$ and $\pi \dot{x}=\dot{x}$; F3 therefore maps that generating set to itself, whence $\widehat{\pi }(b_k)=b_k$. Hence $H_m$ fixes the displayed Boolean name $\dot{y}$ and fixes each of its Boolean coefficients. Its only subnames are the canonical natural-number names, so $\dot{y}$ is hereditarily symmetric. This is the asserted common bounded layer support.