Smooth categories and global \(\square\) (Q1964146)

The authors axiomatically define the concept of a smooth category. Smooth categories allow the fine structural aspects of the construction of \(\square\)-sequences to be separated from the combinatorial aspects. They construct a smooth category of mice and embeddings in the core model for measures of order 0. The construction is based on a ``condensation'' lemma that guarantees that certain condensation arguments preserve sufficient soundness downwards. As a consequence of the construction, the global \(\square\) principle holds in \textbf{K}. The authors prove a stronger result, namely, that a condensation-coherent version of global \(\square\) holds in \textbf{K}.