There is a class of forcing notions I've been playing around with recently. They have a couple nice properties, and all have the same theme, but I've found them difficult to analyze beyond the basics. Before I spend too much time with them, I'd like to ask whether they (or things like them) have been studied before.

*My interest in them is that they can be used to build interesting (hopefully) models in which the reverse-mathematical principle ADS (and related principles) fails; I've sketched this construction below the main question.*

The basic forcing I'm considering is the following:

A nonempty tree $T\subseteq[0, 1]^{<\omega}$ with no dead ends is

$\epsilon$-robust($\epsilon>0$) if the following hold: $(i)$ if $\sigma\in T$ and $m<n<\vert\sigma\vert$ then $\sigma(m)\not=\sigma(n)$ (this isn't essential, but it cleans things up) and $(ii)$ for every $\sigma\in T$ above the stem of $T$ and every open set $U\subseteq [0, 1]$ with $m(U)<\epsilon$, there is a path $f$ through $T$ extending $\sigma$ such that $f(k)\not\in U$ for all $k\ge\vert\sigma\vert$. $T$ isrobustif it is $\epsilon$-robust for some $\epsilon>0$.

Let $\mathbb{T}$ denote the poset of robust trees, ordered by inclusion. My question is:

Question. Is there already literature on $\mathbb{T}$, or related forcing notions?

Let me say a bit about what variations one might consider:

As an obvious first step, we can alter $\mathbb{T}$ by demanding that a condition $T$ be "nice" - e.g. for each $\sigma\in T$, the set of $r$ such that $\sigma^\smallfrown \langle r\rangle\in T$ is Borel, or (assuming large cardinals) that $T$ live in $L(\mathbb{R})$, or so on.

Another change would be to control the robustness, too: e.g. force with pairs $(T,\epsilon)$ where $T$ is $\epsilon$-robust and $(T,\epsilon)\le(S,\delta)$ iff $T\subseteq S$ and $\epsilon>\delta$

Finally, a more elaborate change we can make is to broaden the forcing notion by being more flexible about what "robust" means. Consider the following game $R(T, \epsilon)$ associated to a tree $T\subseteq[0, 1]^{<\omega}$ and an $\epsilon>0$:

Players $1$ and $2$ alternate moves, with player $1$ playing a strictly increasing sequence $\sigma_0\prec \sigma_1\prec\sigma_2\prec …$ of nodes of $T$ and player $2$ playing a strictly increasing sequence of open sets $U_0\subset U_1\subset U_2\subset …$.

On move $i+1$, player $1$ must not use any reals in the open set built by player $2$ so far: if $k\ge\vert \sigma_i\vert$ and $k<\vert\sigma_{i+1}\vert$, then $\sigma_{i+1}(k)\not\in U_i$.

For each $i$, the measure of $U_i$ is $<\epsilon$.

Player $1$ wins iff they always make a legal move.

Call a tree $T$ *playfully $\epsilon$-robust* if player $1$ has a winning strategy in $R(T,\epsilon)$; we can force with such trees instead of genuinely robust trees.

Alright, why do I care about these forcings? It turns out that we can use them to produce $\omega$-models of RCA$_0$ in which the reverse-mathematical principle ADS ("every infinite linear order has an infinite ascending or descending sequence") fails, and I'm interested in figuring out other properties of these models. So let me say a bit about how this works.

Forcing with $\mathbb{T}$ produces a generic sequence $G$ of elements of $[0, 1]$. We isolate a nice class of names for reals:

Let $\nu$ be a $\mathbb{T}$-name for a subset of $\omega$. We say $\nu$ is

stableif for all $T_0,T_1\in\mathbb{T}$ with the same stem and every $k\in\omega$, we have $T_0\Vdash k\in\nu\iff T_1\Vdash k\in \nu$ and $T_0\Vdash k\not\in\nu\iff T_1\Vdash k\not\in \nu$.

This then lets us build an $\omega$-model of RCA$_0$ as follows:

Fix $G$ $\mathbb{T}$-generic over $V$. We set $\mathcal{M}_G=\{\nu[G]:\nu$ is stable$\}$, and conflate this with the corresponding $\omega$-model of RCA$_0$.

(That this is indeed an $\omega$-model is easy to check.)

It turns out that the models we get in this way never satisfy the ADS. The relation "$G(x)\le G(y)$" has a stable name and defines a linear order on $\omega$ in $\mathcal{M}_G$. However, $\mathcal{M}_G$ can have no infinite ascending or descending sequence for this ordering (call it "$\trianglelefteq$"). To see this, suppose $\nu$ were a stable name for a (WLOG) infinite descending sequence through $\trianglelefteq$, and that this is forced by some condition $T$. Let $$r=\inf\{s\in[0,1]: \exists T'\le T, n\in\omega(stem(T')(n)=s\mbox{ and }T'\Vdash n\in\nu) \}.$$ Pick $s\in [0, 1]$, $T'\le T$, and $n\in\omega$ such that the following hold: $\vert s-r\vert<\epsilon$, $stem(T')(n)=s$, and $T'\Vdash n\in\nu$. Letting $T'$ be $\epsilon$-robust, pick some open set $U$ of measure $\delta<\epsilon$ containing the interval $[r, s]$, and let $$\hat{T}=\{\sigma\in T: \forall k\ge\vert stem(T')\vert \mbox{ we have }\sigma(k)\not\in U\}.$$ $\hat{T}$ is $(\epsilon-\delta$)-robust, hence $\hat{T}\le T'$, and $T'$ forces that $\nu$ is not a name for an infinite descending sequence in $\trianglelefteq$.

(The variations on $\mathbb{T}$ described above also allow this same argument to go through. There are also simpler versions of $\mathbb{T}$ with the same basic property, but they seem less interesting.)

I'm trying to figure out whether these models may actually be interesting from a reverse-mathematical point of view. For this to be the case, we would need some nontrivial principle to *hold* in $\mathcal{M}_G$, e.g. WKL$_0$; however, I haven't been able to prove that such a phenomenon occurs. (To me these models are interesting on their own, but I'm particularly interested in their reverse-mathematical potential.) Hence this question.