@AndresCaicedo If you wish to get a bounty for this question, now is your last chance, because bounty is ending.

@AndresCaicedo I feel dumb for not doing this myself before, but I have just now checked that Kanamori's book indeed has the proof I was thinking about. Feel free to post this as the answer, and I'll award you the bounty.

@AndresCaicedo Can you confirm that Kanamori's book has the proof I am talking about? Note that I am looking for a specific proof of the fact.

@EmilJeřábek How would things change if we actually added an axiom "ZFC is consistent" to PA?

I have never seen upper asymptotic density (not the symmetric one) being used for $\Bbb Z$, because it completely ignores half of the set. May I ask where have you seen it being used?

This is perfect, thank you. I guess the same argument will work for Koepke's OTMs (which iirc sit in $\Delta^1_2$ as well).

+1 for the general principle.

That seems to work now. You might want to incorporate it into your answer.

What if the highest order term appears more than once in $\beta$? I don't think it really works then.

Could you elaborate on why you think your first claim is true? I guess that you mean to always choose the least $p_i$ such that adding $p_i^{1/e_i}$ factor will make the product not exceed $r$, but I don't see how it guaranteed the product actually converges to $r$ and not something smaller.

I am amazed by the simplicity of this argument.

@EmilJeřábek Thanks for this link, I think the question can now be marked as a duplicate.