Full normalization for mouse pairs

TL;DR

This paper develops the theory of meta-iteration trees and proves a comparison theorem, showing that mouse pairs have a strong hull condensation property leading to simplified iteration strategies.

Contribution

It introduces the concept of meta-iteration trees, proves a comparison theorem for strategies, and demonstrates that mouse pairs have a unique, simplified iteration process.

Findings

Meta-iteration trees theory established.

Comparison theorem for meta-iteration strategies proved.

Every iterate of a mouse pair is via a single normal iteration tree.

Abstract

We develop the theory of meta-iteration trees, that is, iteration trees whose base "model" is itself an ordinary iteration tree. We prove a comparison theorem for meta-iteration strategies parallel to the one for ordinary iteration strategies, and use it to show that the iteration strategy component of a mouse pair condenses to itself under weak tree embeddings. These constitute a class of embeddings between iteration trees that is significantly larger than the class of embeddings mentioned in the definition of mouse pair. We then use this very strong hull condensation property of mouse pairs to show that every iterate of a mouse pair is an iterate via a single $\lambda$-tight, normal iteration tree, and that the associated tail strategies are independent of how the iterate was reached.