Intuitively, at any given time the Gödel machine should
execute some self-modification algorithm only if it is
the `best' of all possible self-modifications,
given the optimality criterion, which typically
depends on available resources, such as storage size and
remaining lifetime.
At first glance, however, target theorem (2)
seems to implicitly talk about just
one single modification algorithm, namely, switchprog
as set by the systematic proof searcher at time 
.
Isn't this type of local search greedy? Couldn't
it lead to a local optimum instead of a global one?
No, it cannot, since the target theorem implicitly also talks about all the other switchprogs that the proof searcher could produce in the future. To see this, consider the two alternatives of the binary decision: (1) either execute the current switchprog, or (2) keep searching for proofs and switchprogs until the systematic searcher comes up with an even better switchprog. Obviously the second alternative concerns all (possibly infinitely many) potential switchprogs to be considered later. That is, if the current switchprog were not the `best', then the proof searcher would not be able to prove that setting switchbit and executing switchprog will cause higher expected reward than discarding switchprog, assuming consistency of the underlying formal system. Only if it is provable that the current proof searcher cannot be expected to find sufficiently quickly an even better switchprog, will it also be provable that the current switchprog should be executed.
So the trick is to let the formalized improvement criterion take into account the (expected) performance of the original search method, which automatically enforces globally optimal self-changes, relative to the provability restrictions.