A coordinate swap defeats an atom-free sock choice

Suppose $p$ forces that a supported name $c$ is a choice function. Let $E$ support both $p$ and $c$. Pick $n$ outside the finitely many pair indices occurring in $E$, and strengthen to $q\le p$ deciding, after relabelling the two mates if necessary, $q⊩c(P_n)=R_{n,0}\mathrm{.}$ This is a single forcing decision, not a sequence of choices.

Because $q$ has finite domain, choose a natural-number coordinate cutoff beyond all coordinates of $q$ in the $n$th blocks. Define an automorphism $\pi$ which swaps the two $n$-blocks while translating the finitely used internal coordinates to unused coordinates, and fixes $E$. Then $q$ and $\pi q$ agree wherever both are defined, hence $q\cup \pi q$ is a condition.

The support of $c$ is fixed, so $\pi c=c$, while $\pi R_{n,0}=R_{n,1}$ and $\pi P_n=P_n$. By F2, equivariance transforms the decision in step 1.1 into $\pi q⊩c(P_n)=R_{n,1}\mathrm{.}$ Their common extension forces $R_{n,0}=R_{n,1}$, contradicting F3. Thus the fresh coordinate swap defeats the proposed choice.