simrob gradually revealed that I've been mistaken about something in the Ill-Fated resource semantics paper for basically the last three years. It's a thing I like about math sometimes that when you're wrong, you're just flat out wrong and there's no quibbling about it. It ideally provides a nice boot in the butt to get you moving on to something else, although I have to admit it I still was on a bit of an emotional rollercoaster during thesis times as material alternately did and did not appear to work.Anyway, the latest version, with some proof sketches, is:
http://jcreed.org/math/modal-encoding/equational.html
The real scales-fall-from-eyes observation is that Nuel Belnap's "display property" seems to actually be really, really importantly involved in focusing working out right. I went back and looked at that silly little queue logic that I made up as a counterexample to make a point, and it turns out it focuses really badly! If you do it naively, the sequent p, ↓↑q |- p * q (where p and q are positive atoms) is not provable while p, q |- p * q plainly is. The only way I know how to recover is to bake shifts into some of the connectives: fuse must be of the form P * N, and blurs on its N argument, and right-arrow must be of the form N =>> N, and blurs on its left argument.
Relatedly, all the weird stuff in the shifty modalities like square, diamond, and circle is similarly "undisplayable", and so that's in a sense arguably why those connectives act like shifts.