We should be able to make the bounds smaller... Let a be small (in comparison to n), and let P be the proof of length n that "T can't prove a falsehood in f(n) symbols" is true.

Then define R as above, except it searches through all proofs beginning with P, of length n+a. Then T can completely simulate the execution of R in slightly over (n+a)exp(a) symbols. Then the same reasoning would establish that we only need to take f(n) >> (n+a)exp(a) in order for the reasoning to work.

Not sure how large a should be. It might be a constant, but more likely it grows logarithmically with n (as it probably has to include the definition of n itself). Which would mean f(n) >> n^2.

If this argument works, we might be able to get even better bounds restrictions - maybe we restrict R to look at proofs starting with P, which then include the definition of n somewhere after. Or maybe R just looks at a single proof - the actual proof that R printing anything is impossible? That would reduce to f(n) >> n.