Spent most of today wrestling with trying to understand Rowan's latest iteration on this family of modal logics him and Frank and me have been talking about over the last month or two. I am really skeptical of whether it cut-eliminates properly. This comes mostly just from an experience-fueled intuition that almost every sufficiently complicated logic you try to invent that is not definitely proven to cut-eliminate, in fact does not. Also there are some specific red flags, like the 0L rule having some funny side conditions that don't sit well with me.
Still, I haven't found any actual way to break it, even after making good progress drilling down into where I think the counterexample should lie, if anywhere: in the 0L commutative case of the cut theorem for cutting possibility judgments. I have it down to a relatively small lemma that I nonetheless can't see how to prove or refute.
Fun times anyhow!