Depth-stabilizing inverse limit of game coverings (source code)

= Depth-stabilizing inverse limit of game coverings

In a sequence of <game coverings> whose unchanged initial depths tend to infinity, each finite game-tree level eventually stabilizes. These stable levels form a limit game. Compositions of prefix projections and depth-local strategy maps give limit projections and strategy maps. Lift a compatible play coherently through successive coverings. If no premature loss occurs, stabilization of its finite prefixes supplies a compatible limit play. If a premature loss occurs, subsequent lift lengths cannot increase and eventually stabilize, supplying a losing terminal limit play. This proves the lifting condition for the limit covering. It makes countably many pulled-back payoffs <clopen> simultaneously in the covering proof of <Borel determinacy theorem>.