I apologize for all the edits driving this up to the front page, but it seems I asked a question which was half-baked. Initially I thought E2 proved a much stronger lower bound, but working out the heuristics, I realized that it doesn't. E3 generates all coprimes is the right question, as this is really what I was surprised by when doing calculations.

@Dror:1. Done. 2. There are much more serious problems with this heuristic, it is not quite self-consistent. I "feel" it is asymptotically right, but it is not even convincing at the heuristic level.

I still am having some trouble with the full computational interpretation of Jech/Woodin. The simpler consequences are easy enough to interpret as standard type I arguments, but there is one theorem which is completely different: there is no descending infinite sequence of models of set theory. I had a similar proof for the well-foundedness of the collection of theories stronger than PA under the ordering A is stronger than B when A proves the consistency of B. But this theorem has a more involved proof than type I arguments. I'll try to finish Jech Woodin today.

Of course you are right. The way I think of silly changes is by the complexity of the proof required to prove statement II given statement I and vice versa. For the example you gave, I would be happy thinking of them as (slightly)different proofs because to get from one to the other is not much simpler than proving either. There is a measure of closeness defined by how long/complex (axiom strength wise) the equivalence between the constructions is.