I am reading Jörg Brendle's Bogota note, and the author claimed that Sacks forcing with countable support product does not satisfy a product lemma. Especially, he mentioned that if $\mathbb{S}_I$, $|I|$-many countable support product of Sacks forcing $\mathbb{S}$, adds $|I|$ Sacks reals $\langle s_i\mid i\in I\rangle$ and $i\neq j$, then $s_j$ is not $\mathbb{S}$-generic over $V[s_i]$.
Let me take $I=2$ for simplicity. One subtle point of the claim is that $\mathbb{S}$ need not be absolute between $V$ and $V[s_0]$. In fact, the product lemma for general forcing shows that $s_1$ would be $\mathbb{S}^V$-generic over $V[s_0]$. Hence I think the author intends to claim that $s_1$ is not $\mathbb{S}^{V[s_0]}$-generic over $V[s_0]$.
However, $\mathbb{S}^V\neq\mathbb{S}^{V[s_0]}$ does not automatically mean $s_1$ is not $\mathbb{S}^{V[s_0]}$-generic over $V[s_0]$. My question is:
How to prove $s_1$ is not $\mathbb{S}^{V[s_0]}$-generic over $V[s_0]$?
I am new at Sacks forcing, so I have no idea how to start. I would appreciate your help!
The point is that in the two-step iteration $s_1$ codes $s_0$ over the ground model in the sense that there is a Borel function $f \colon 2^\omega \to 2^\omega$ in $V$ so that $f(s_1) = s_0$. This can't happen in the product (for example $s_1$ is not a minimal real over $V$).
I don't know if there is a simple way to see this but I will sketch how I would prove it (if you want me to add details I can do that).
Lemma 1. Sacks forcing has the continuous reading of names, i.e. whenever $\dot y$ is an $\mathbb{S}$-name for an element of an arbitrary Polish space $X$ and $p \in \mathbb{S}$, then there is $q \leq p$ and a continuous function $g \colon [q] \to X$ so that $q \Vdash g(\dot s_0) = \dot y$.
This is usually formulated with $X = \omega^\omega$ but it doesn't make a difference since every Polish space is the continuous image of $\omega^\omega$. Also $[q]$ is the set of branches through $q$ and $\dot s_0$ is a name for the Sacks real that is added by $\mathbb{S}$.
Now a condition in the two-step iteration is a pair $(p,\dot q)$ where $p$ is a perfect tree and $\dot q$ is a $\mathbb{S}$-name for a perfect tree. Thus $\dot q$ is a name for an element of the Polish space $X$ of perfect trees and we find $p' \leq p$, $g \colon [p'] \to X$ interpreting $\dot q$, in the sense that $p' \Vdash g(\dot s_0) = \dot q$.
Now consider the following lemma.
Lemma 2. There is a continuous function $g' \colon [p'] \to X$ so that for every $x \in [p']$, $$g'(x) \subseteq g(x)$$ and for every $x\neq y \in [p']$, $$[g'(x)] \cap [g'(y)] = \emptyset.$$
Now we can define a name $\dot q'$ so that $p' \Vdash \dot q' = g'(\dot s_0)$. The point is that now we can read off $s_0$ from $s_1$. Define $f(x) = y$ if $y \in [p']$ and $x \in [g'(y)]$, and else $f(x) = 0$. Then $f$ is a Borel function in $V$ and $f(s_1) = s_0$.