I think you're right.

In Gödel's speed-up theorem, one may consider the statement $\sigma$, asserting that "there is no proof of $\sigma$ in PA of length less than a googolplex symbols." Now, if there were a short proof of $\sigma$, in less than a googolplex symbols, then we would be able to prove that the proof had that property, and thereby prove a contradiction in PA. So if PA is consistent, then $\sigma$ is true. Meanwhile, assuming again that PA is consistent, then we can also see that PA is actually provable in PA, by enumerating all the proofs. So we see that in fact PA proves $\sigma$, but only by a very long proof, whereas PA+Con(PA) provides a very quick proof of $\sigma$ by formalizing the argument we have just given.

Now, by the MRDP theorem, there is an integer polynomial $p(x,\vec x)$ such that $p(k,\vec k)=0$ for integers just in case $k$ codes a proof of $\sigma$ in PA. Although the coding of c.e. sets into diophantine equations is complicated, it is ultimately managable, and one can get an explicit polynomial $p$. I haven't worked out the polynomial explicitly — and I don't intend to do so — but I believe that the particular bounds that you mention are not unreasonable. It may be useful to compare with this polynomial, whose solutions are exactly the primes. The difficulty of the primeness representation seems basically comparable to yours, and this is why I think your bounds are reasonable.

So what we have is a comparatively small polynomial $p(x,\vec x)$, such that PA proves that $\exists k,\vec k\ p(k,\vec k)=0$ and furthermore proves that any such $k$ will be the code of a proof of $\sigma$ in PA. Thus, there can be no short proof of this. But meanwhile, PA+Con(PA) proves $\exists k,\vec k\ p(k,\vec k)=0$ by a very short proof, which simply formalizes our argument above. So we've got all your desired properties.

So I think (a) you're basically right; (b) yes, the $k$'s must be large, for otherwise we could have a short proof of $\sigma$ just by evaluating $p(k,\vec k)=0$, combined with the fact that PA proves (by a short proof) that any such $k$ must code a proof of $\sigma$. Regarding statement (c), however, I don't think it makes any sense, because every particular natural number is computable, by the algorithm that simply writes it down. If it was merely bounds on $k$ that you wanted, these are provided by the size of the proof of $\sigma$ in PA, which proceeds by enumerating all proofs of size less than a googolplex symbols, and noting that it is not a proof of $\sigma$.

I think you're right.

In Gödel's speed-up theorem, one may consider the statement $\sigma$, asserting that "there is no proof of $\sigma$ in PA of length less than a googolplex symbols." Now, if there were a short proof of $\sigma$, in less than a googolplex symbols, then we would be able to prove that the proof had that property, and thereby prove a contradiction in PA. So if PA is consistent, then $\sigma$ is true. Meanwhile, assuming again that PA is consistent, then we can also see that $\sigma$ is actually provable in PA, by enumerating all the proofs. So we see that in fact PA proves $\sigma$, but only by a very long proof, whereas PA+Con(PA) provides a very quick proof of $\sigma$ by formalizing the argument we have just given.

Now, by the MRDP theorem, there is an integer polynomial $p(x,\vec x)$ such that $p(k,\vec k)=0$ for integers just in case $k$ codes a proof of $\sigma$ in PA. Although the coding of c.e. sets into diophantine equations is complicated, it is ultimately managable, and one can get an explicit polynomial $p$. I haven't worked out the polynomial explicitly — and I don't intend to do so — but I believe that the particular bounds that you mention are not unreasonable. It may be useful to compare with this polynomial, whose solutions are exactly the primes. The difficulty of the primeness representation seems basically comparable to yours, and this is why I think your bounds are reasonable.

So what we have is a comparatively small polynomial $p(x,\vec x)$, such that PA proves that $\exists k,\vec k\ p(k,\vec k)=0$ and furthermore proves that any such $k$ will be the code of a proof of $\sigma$ in PA. Thus, there can be no short proof of this. But meanwhile, PA+Con(PA) proves $\exists k,\vec k\ p(k,\vec k)=0$ by a very short proof, which simply formalizes our argument above. So we've got all your desired properties.

So I think (a) you're basically right; (b) yes, the $k$'s must be large, for otherwise we could have a short proof of $\sigma$ just by evaluating $p(k,\vec k)=0$, combined with the fact that PA proves (by a short proof) that any such $k$ must code a proof of $\sigma$. Regarding statement (c), however, I don't think it makes any sense, because every particular natural number is computable, by the algorithm that simply writes it down. If it was merely bounds on $k$ that you wanted, these are provided by the size of the proof of $\sigma$ in PA, which proceeds by enumerating all proofs of size less than a googolplex symbols, and noting that it is not a proof of $\sigma$.