Interesting. I'm not convinced that that's required (e.g. for the 5 and 10 problem). If you read Ingredients of TDT with an eye towards that, I think there's a strong case that using causal surgery rather than logical implication solves the problem.

As far as I know, TDT was mostly abandoned in favor of UDT. In particular I don't think there is a well defined recipe how to describe a given process as a causal diagram with pure-computation nodes. But I might be missing something.

Fair enough - I meant that if you prove R-+(s,1), then for a consistent set of axioms, I think you violate the consistency condition set by Löb's theorem if say "If Pmin(s)=1, then s."

I'm not sure what you're saying here. The usual notion of consistency doesn't apply to my system since it works fine for inconsistent theories. I believe that for consistent theories the energy minimum is always 0 which provides a sort of analogue to consistency in usual logics.