Indeed, but I expect that that for any theorem, that for some level of proof quality which is attained, that all proofs that are at least that good, all have at

Indeed, but I expect that that for any theorem, that for some level of proof quality which is attained, that all proofs that are at least that good, all have at most a certain finite length. And, as there are only finitely many proofs of any finite length, then the supremum of proof quality over any proofs of that theorem, is attained. (whether there is usually unique proof which attains it, I don't care to guess.)