The latest thing that occurred to me is to do the thing I love to do and represent ^P as q * P and vN as q -o N, and subsequently to that say that [P]N ("if P is true right now then you can focus on N on the left") is something like
q -o ((P -o 0) + N)
This resembles vN, except you've wedged in the additional requirement that you have to be able to prove P, while of course being able to sneak whatever resources you like into the garbage collector that is 0.
But, critically, you've spent the token q, which means it's not available during the proof of P, so you can't execute on transition rules that represent "real" changes in the state, which will by default all participate in the token discipline of slurping up and spitting back out q's. Also while decomposing N, you've already spent the token, but this is normally how focusing on something negative on the left works -- by the time you drill down to some ^P = q * P, you'll get the token back in that branch.
Now if you want to have some rules that derive a datalog-style IDB from an EDB, then you can maybe make them at a different mode-of-truth that have different shifts that don't require token-slinging, and they will still be available during the proof of P.