Stabilizing systems of game coverings have inverse limits

Choose increasing stabilization indices $i_n$, enlarging each least qualifying index by the preceding ones. The depth-$\le n$ nodes and taboo labels of $T_{i_n}$ agree with those of every later stage. These finite-depth restrictions agree on overlaps: compare both with any stage beyond both indices. Their union defines $T_{\mathrm{\infty }}$ on the union of the stage alphabets, which is a set. Prefix closure follows at a common depth. If a node is not taboo, look at the stabilized next depth: at that stage it is nonterminal and has a child, which belongs to the union. If it is taboo, no stage after stabilization has a child. Thus these labels partition exactly the terminal nodes of the union tree.

For a limit node $s$ of length $n$, take $j\ge i_n,i$ and define ${\pi }_{\mathrm{\infty },i}(s)={\pi }_{j,i}(s)$. Coherence and identity of later maps through depth $n$ make this independent of $j$. Prefix, length and taboo reflection follow by computing at one sufficiently late common stage. For a limit strategy $\sigma$, to define its image below depth $n$, take $j\ge i_{n+1},i$, extend its common finite-depth restriction to a total strategy ${\sigma }^j$ on $T_j$ using A1, and use ${\varphi }_{j,i}({\sigma }^j)$ below $n$. F1 makes this independent of the extension. Comparing at a further stage and using coherence proves independence of $j$ and agreement as $n$ grows. Thus it defines a total strategy ${\sigma }_i$; legality is inherited at that finite depth.

The same finite-depth calculation proves locality, ${\varphi }_{\mathrm{\infty },i}={\varphi }_{j,i}\circ {\varphi }_{\mathrm{\infty },j}$ and the analogous position identity. Since all stage maps are $k$-coverings, the common nodes/labels through $k$, position identities there and strategy identities below $k$ are inherited by each limit map. It remains only to prove lifting.

Fix a maximal ${\sigma }_i$-consistent play $x_i$ at stage $i$. For every stage $j\ge i$, ${\sigma }_j={\varphi }_{j+1,j}({\sigma }_{j+1})$ by step 3.1. Therefore F1 gives a nonempty set of maximal ${\sigma }_{j+1}$-consistent lifts of any maximal ${\sigma }_j$-consistent play. All candidates lie in the set union of the stage maximal-play spaces. A1 supplies a selector on these nonempty lift sets; F3 recursively gives $x_{j+1}$ lifting $x_j$. These are successive lifts, so ${\pi }_{j+1,j}(x_{j+1})\subseteq x_j$, with each proper lift taboo for the player $P$ of $\sigma$.

If every $x_j$ is infinite, every adjacent projection equality holds. For each $n$ and $j\ge i_n,i$, identity through depth $n$ gives $x_{j+1}\upharpoonright n=x_j\upharpoonright n$. The eventual prefixes are compatible, so their union is an infinite limit branch $y$, consistent with $\sigma$ by the finite-depth definition of ${\sigma }_j$. Computing its projection to $i$ at a sufficiently late stage gives ${\pi }_{\mathrm{\infty },i}(y)\upharpoonright n=x_i\upharpoonright n$ for every $n$, hence equality.

Otherwise, once a finite $x_j$ occurs, subsequent lengths are nonincreasing natural numbers by length preservation and the prefix requirement; they eventually equal some $l$. Choose a stage after this stabilization and after $i_{l+1}$. The ensuing plays have equal length and are literally the same depth-$l$ node by stabilization. This node $y$ is terminal in $T_{\mathrm{\infty }}$ with their common label, and its finite prefixes obey $\sigma$ by step 2.1. Its projection to stage $i$ is a prefix of $x_i$ by the successive projection identities. If that prefix is proper, at least one adjacent lift was proper (otherwise composition would give equality); that lift has label taboo for $P$. Each later proper lift has the same label, and each later exact lift inherits it by taboo reflection. Thus $y$ is taboo for $P$. If there was no proper lift, the projection equals $x_i$. Both alternatives satisfy F1. This completes the missing lifting condition and the theorem. QED.