@stevendaryl
I feel that there are number of subtelties. As your post is very new, I haven't thought about it very well. However, I can try to explain with one example the kind of issues that I feel arise here. I will assume below that we are talking about a theory ##T## with r.e. theorems (and also, the discussion is limited to theorems of ##T## rather than all the problems that are posed in ##T##).
Let's suppose we have 6 programs with indexes ##e_1##, ##e_2##, ##e_3##, ##e_4##, ##e_5##, ##e_6## respectively. Denoting the halting times of these programs as ##t_1##, ##t_2##, ##t_3##, ##t_4##, ##t_5##, ##t_6## respectively
[also suppose that the ##t_i## values are strictly increasing with ##t_{i+1}>>t_i##
]. Also suppose that ##t_i>> e_i## for each ##1 \leq i \leq 6##.
Now consider the problem of determining the truth of the following two equations
[each of the ##t_i## values expressed indirectly via halting times
]:
##t_1+t_2=t_3## ---- (E1)
##t_4+t_5=t_6## ---- (E2)
One "obvious" way (in both cases) is to simulate running of the programs and then determine the answer. Such a proof would have a very high length. Now suppose that there is a sophisticated alternative which leads to a very short proof of ##E2##.
However, assume that there is no such short and sophisticated alternative for ##E1##.
========================
Would you say that the ##E1## is easier than ##E2##?
In terms of smallest proof, ##E2## is easier than ##E1##. However, alternatively, if we informally think about the difficulty of ##E1##, ##E2## we could say that they are equally difficult
[since (in a very informal sense) both have the "easiest proof" with the "same method"
].
This kind of thing is also highlighted when, for some program enumerating the theorems, we try to think of "time of output" for a given proof to appear. If we think of a program that outputs theorems in a very basic way, it is entirely possible that it would output the "sophisticated shorter proof" of ##E2## too late, and hence it would classify ##E1## as easier than ##E2##. On the other hand, another more advanced program for enumerating proofs could recognize the "sophisticated shorter proof" of ##E2## much earlier and hence declare ##E2## to be easier than ##E1##.
========================
In short, it looks complicated to me.
P.S.
It occurred to me that the function ##f:S^2 \rightarrow \{0,1\}## in post#26 should have been ##f:S^2 \rightarrow \{0,1,2\}##.