Globally Optimal Self-Changes, Given $u$ and $\cal A$ Encoded in $p$

Theorem 4.1   Given any formalizable utility function $u$ (Item 1f), and assuming consistency of the underlying formal system $\cal A$, any self-change of $p$ obtained through execution of some program switchprog identified through the proof of a target theorem (2) is globally optimal in the following sense: the utility of starting the execution of the present switchprog is higher than the utility of waiting for the proof searcher to produce an alternative switchprog later.

Proof. Target theorem (2) implicitly 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 (set switchbit $=1$), or (2) keep searching for proofs and switchprogs (set switchbit $=0$) 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 $\cal A$. Q.E.D.

The initial proof searcher of Section 5 already generates all possible proofs and switchprogs in $O()$-optimal fashion. Nevertheless, since it is part of $p(1)$, its proofs can speak about the proof searcher itself, possibly triggering proof searcher rewrites resulting in better than merely $O()$-optimal performance.