Understanding the monoid of endofunctors of the stable homotopy category generated by localizations with respect to finite unions of Morava K-theories is relevant to transchromatic phenomena and the Chromatic Splitting Conjecture, but the combinatorial aspects are complex.

The authors work in an axiomatic framework applicable to both ordinary and equivariant stable homotopy theory, studying iterated chromatic localizations. The combinatorial parts of the work are formalized in the Lean proof assistant to ensure correctness of the intricate combinatorial arguments.

The results characterize the monoid structure of iterated chromatic localizations, providing tools for studying transchromatic phenomena including the Chromatic Splitting Conjecture. The Lean formalization covers the combinatorial components of the proofs.