Game coverings, k-coverings and unraveling

Let $T,S$ be trees with terminal taboos in the sense of Game trees with terminal taboos. A covering of $T$ is a triple $(S,\pi ,\varphi )$ with the following data and requirements, formulated in ZF.

The position map $\pi :S\to T$ preserves lengths and prefixes. It reflects target taboos: if $\pi (s)$ is taboo for $P$ in $T$, then $s$ is taboo for $P$ in $S$. For $y\in [S]$, define $\pi (y)={\bigcup }_n\pi (y\upharpoonright n)$. Prefix and length preservation make this a branch of $T$ with those specified restrictions. For a finite maximal play use the position map.

The strategy map $\varphi$ sends every total strategy on $S$ to a total strategy for the same player on $T$. Regard strategies as tagged by their player, even if the underlying functions happen to coincide. Finite-depth locality means: if two input strategies for the same player agree at all positions of length $<n$, their images agree at all target positions of length $<n$.

Lifting requirement. For each strategy $\sigma$ for player $P$ on $S$ and each maximal play $x$ on $T$ consistent with $\varphi (\sigma )$, there exists a maximal play $y$ on $S$ consistent with $\sigma$ such that $\pi (y)\subseteq x$ and either $\pi (y)=x$ or $y$ is taboo for $P$. Thus a lift may end early only as a loss for its strategy's player. No specified lift function is part of the data, and independent existential lifts are not asserted to be coherent.

For $k\in \mathbb{N}$, this is a $k$-covering if $S,T$ have identical nodes and taboo labels at lengths $\le k$, $\pi$ is the identity on those nodes, and $\varphi (\sigma )$ equals $\sigma$ at positions of length $<k$. In particular a zero-covering identifies the roots and their taboo labels; its strategy-identity condition is vacuous.

A covering unravels $A\subseteq [T]$ if ${\pi }^{-1}(A)$ is clopen in $[S]$. This preimage uses infinite branches only. The branch map is continuous: for a cylinder $[T{]}_p$ its preimage is $\bigcup \{[S{]}_s:\mathrm{\mid }s\mathrm{\mid }=\mathrm{\mid }p\mathrm{\mid },\pi (s)=p\}$. A finite maximal lifted play can project to a nonterminal target position; taboo reflection is not being reversed in that situation.