Smooth categories and global □ Original Research Article

We shall construct a smooth category of mice and embeddings in the core model for measures of order 0. The existence of such a category implies that the global principle □ holds in View the MathML source. We then prove a much stronger, the so-called condensation-coherent version of global □. The key tool of the whole construction is a new criterion on preserving soundness under condensation.