My question is:
Let $\mathbb{P}$ be a forcing and $\tau \in V^\mathbb{P}$ is a name. Suppose that $$1_{\mathbb{P} \times \mathbb{P}} \Vdash_{\mathbb{P} \times \mathbb{P}} \tau_\text{left} = \tau_\text{right}$$
where $\tau_\text{left}$ and $\tau_\text{right}$ are the usual $\mathbb{P} \times \mathbb{P}$ names that gives the evaluation of $\tau$ according to the left and right generic. Then is it true that there exists a set $x \in V$ such that $$1_\mathbb{P} \Vdash_\mathbb{P} \check x = \tau$$
Some remarks:
Note that this is true for names forced to be set of ordinals: If there is an ordinal $\lambda$ such that $1_\mathbb{P} \Vdash \tau \subset \check \lambda$, then the above question is answered positively.
Essentially this follows by asking for each $\alpha < \lambda$, whether $1_\mathbb{P} \Vdash \check \alpha \in \tau$.
If $1_{\mathbb{P}} \Vdash \tau \subseteq \check y$ for some $y \in V$, then the question should also be answered positively.
Also it is known that one can code arbitrary sets as sets of ordinals. One can attempt to do this in the forcing extension. However, to reduce this back to the subset of the ordinal case, one would need to have the encoding bijection be forced to be the same in any product generic, which I am not sure is possible. However, if $\tau$ is forced to be a subset of a ground model set, then one can choose an encoding bijection to be in the ground model.
Another thing to try may be a rank argument on the names used to make $\tau$. Using this method, I start to run into forcing statement like $``\sigma \notin \check V"$. Then to work with products, I would like to apply that statement over a forcing extension $V[G]$. I am some what uncomfortable using this name for the ground model. I am aware that the ground model is definable in $V[G]$ using parameters from $V$. However, if in $V$, $1_\mathbb{P}$ forces some statement using $\check V$ and $G \times H$ are product generic, I am not sure if $V[H]$ satisfy the same thing with $V[G]$ in place of the ground model. I am not sure if the usual behavior of forcing statements in products work for forcing statement that use the name for the ground model.
Intuitively, it feels that if a name is interpreted the same way in all generics extension then it should be a ground model element. Thanks for any insights that can be provided.
This is a nice question and the answer is yes. The key is the following result of Solovay: if $G,H$ are mutually generic for $\mathbb{P}$ (meaning that $G\times H$ is generic for $\mathbb{P}\times\mathbb{P}$) then $V[G]\cap V[H]=V$. You can find a proof in this MO answer (your own argument was basically going in this direction).
So let $\tau$ be a name which is interpreted to be the same by any pair of mutually generic filters. Fix such a pair of filters $G,H$. Since then $x=\tau^G=\tau^H$ is in both $V[G]$ and $V[H]$, Solovay's result implies that $\tau$ is forced to be a ground model set. We are almost done; we still need to deal with the possibility that the ground model set depends on the choice of the generic. However, we are in luck. Suppose there is a condition $p$ forcing that $\tau\neq \check{x}$. We can then let $H'$ be $\mathbb{P}$-generic over $V[G]$ with $p\in H'$. By assumption $x=\tau^G=\tau^{H'}$, but, since $p\in H'$, also $x\neq \tau^{H'}$, contradiction. We thus conclude that it is forced that $\tau=\check{x}$.