I think this factoring hides the computational content of Löb’s theorem (or at least doesn’t make it obvious). Namely, that if you have , then Löb’s theorem is just the fixpoint of this function.

Here’s a one-line proof of Löb’s theorem, which is basically the same as the construction of the Y combinator (h/t Neel Krishnaswami’s blogpost from 2016):

where is applying internal necessitation to , and .fwd (.bak) is the forward (reps. backwards) direction of the point-surjection .

This seems like a match for cross-entropy, c.f. Nate’s recent post K-complexity is silly; use cross-entropy instead