Finite-support symmetry and bounded-stage approximation

Suppose $p{⊩}_3\phi (\vec{\tau })$ but $p\upharpoonright e$ does not force it. By the negation clause there is $q\le p\upharpoonright e$ with $q{⊩}_3\mathrm{\neg }\phi (\vec{\tau })$. Because the trunk of $q$ lies in its upper tree and that tree projects into the upper tree of $p\upharpoonright e$, lift the trunk $q\upharpoonright e$ to a node of the upper tree of $p$ and pass to its cone. This gives $p^{\ast }\le p$ with $p^{\ast }\upharpoonright e=q\upharpoonright e$. Use finite support extension and legal successor steps to obtain $p_1\le p^{\ast }$ and $q_1\le q$ on the same finite closed coordinate domain, with equal corresponding section lengths and still $p_1\upharpoonright e=q_1\upharpoonright e$. For each coordinate outside $e$, the finite bijection sending $p_1(\alpha )(n)$ to $q_1(\alpha )(n)$ extends to a finite permutation ${\pi }_{\alpha }$ of $\alpha$; take the identity on $e$, obtaining $\pi \in H_e$. Shrink the upper tree $U_1$ of $p_1$ so that no value newly appearing outside $e$ lies in the finite range of $q_1$ at that coordinate, and shrink the upper tree $V_1$ of $q_1$ symmetrically away from the range of $p_1$. The coordinate filters are uniform and hence contain complements of finite sets, so these are direct refinements; by construction $(p_1,U_1^{\mathrm{\prime }})$ lies in the dense action domain $P^{\pi }$. Finally intersect $\pi U_1^{\mathrm{\prime }}$ with $V_1^{\mathrm{\prime }}$ above their common trunk $\pi p_1=q_1$. F3 makes this a condition $q^{\mathrm{\prime }}\le q_1$; its inverse image $p^{\mathrm{\prime }}={\pi }^{-1}{q}^{\mathrm{\prime }}$ refines $p_1$, and $\pi p^{\mathrm{\prime }}=q^{\mathrm{\prime }}$.

Since $H_e$ fixes every name in $\vec{\tau }$, F2 sends $p^{\mathrm{\prime }}{⊩}_3\phi (\vec{\tau })$ to $\pi p^{\mathrm{\prime }}{⊩}_3\phi (\vec{\tau })$. But $q^{\mathrm{\prime }}{⊩}_3\mathrm{\neg }\phi (\vec{\tau })$, and a common refinement of $\pi p^{\mathrm{\prime }}$ and $q^{\mathrm{\prime }}$ would force both alternatives. This contradiction proves the restriction implication. The empty support and identity permutation are allowed, and zero parameters cause no change.

Let $\dot{x}$ be supported by $e$ and suppose ${\dot{x}}_G\subseteq \gamma$ for a ground ordinal $\gamma$. By the truth lemma choose $p_0\in G$ with $p_0{⊩}_3\dot{x}\subseteq \check{\gamma }$. Define the set $P_e$-name ${\dot{x}}_e=\{(\check{\alpha },p\upharpoonright e):\alpha <\gamma ,p\le p_0,p{⊩}_3\check{\alpha }\in \dot{x}\}$. This is a set because $\gamma$ and the finite-coordinate forcing $P_e$ are sets. Step 2.1 says every displayed restriction forces the same membership. If $\alpha \in ({\dot{x}}_e{)}_{G\upharpoonright e}$, truth gives $\alpha \in {\dot{x}}_G$; conversely, if $\alpha \in {\dot{x}}_G$, truth below the chosen $p_0\in G$ gives $p\in G$ with $p\le p_0$ forcing membership, and $p\upharpoonright e\in G\upharpoonright e$ places $\alpha$ in $({\dot{x}}_e{)}_{G\upharpoonright e}$. Thus the two values agree.

Every $x\in N_G$ is the value of an HS name, which by definition has some finite support; closing it under ${\mathrm{cf}}^{\mathrm{\prime }}$ remains finite. F1 bounds the transitive closure of that set name in a regular $P_{\theta }$ and preserves hereditary symmetry there, giving $x\in N_{G_{\theta }}$. For a set of ordinals, choose $\gamma >\sup x$ and apply step 3.1 to obtain the sharper finite-restriction name. No converse from mere membership in $M[G\upharpoonright e]$ to symmetry is claimed.