# Does Laver Forcing add an infinitely often equal real?

Given a model $V$ of set theory and an inner model $W \subseteq V$, a real $x \in V \cap \omega^\omega$ is infinitely often equal over $W$ if for each real $y \in \omega^\omega$ there are infinitely $n$ with $x(n) = y(n)$. Cohen reals have this property and it was an open question for a while as to whether every forcing adding an infinitely often equal real also adds a Cohen real. In fact this is false.

What I want to know is whether it is ever the case that Laver forcing adds a real which is infinitely often equal over the ground model. I expect the answer to be no given the aforementioned question about finding infinitely often equal reals that are not Cohen. However, I'm struggling to prove it.

For reference, recall that Laver forcing, $\mathbb L$, is defined to be the set of trees on $\omega$ with a distinguished stem and infinitely branching at every node above the stem. A Laver real is defined in the generic extension to be the union of the stems of the trees in the generic. It's not hard to see that such a real is always dominating over the ground model. Moreover it is well known (and proved in Jech) that $\mathbb L$ never adds Cohen reals over the ground model, even when iterated.

• If $x$ is infinitely equal to all reals from the ground model, then $x':=\min(x,id)$ is infinitely equal to all ground model reals bounded by $id$, and $x'$ is now bounded. – Goldstern Dec 7 '17 at 22:37