I think that's slightly incorrect. The proof M is looking for is of the following statement: "P is an algorithm that solves the problem and T is an algorithm th

I think that's slightly incorrect. The proof M is looking for is of the following statement: "P is an algorithm that solves the problem and T is an algorithm that is guaranteed to output, for any input, an upper bound on the running time of P for that input." There's no requirement that P should be proved to be faster than some other program. Anyhow, your criticism of the result's limited applicability still stands. I can't resist offering another nitpick: it's curious that the author neglected to mentioned that the proof system must be sound.