(This question is pure curiosity. Feel free to close it if you feel it is not appropriate for mathoverflow.)
In 2013 Zhang showed that there are infinitely many pairs of primes which are less that 70,000,000 apart. Since then, this result has been significantly improved. (See here for the state-of-the-art.) Let $z_n$ denote the $n$th "Zhang prime", that is the $n$th prime $p$ such that the next prime is not more than $p + 70,000,000$. My question is as follows.
Does Zhang's proof or any of its improvements establish a primitive recursive upper bound on the $n$th Zhang prime, that is a primitive recursive function $f(n)$ such that $z_n \leq f(n)$?
A few (trivial) comments for those who don't regularly think about primitive recursive functions:
Zhang's result (regardless of the proof) gives a recursive (a.k.a. computable) upper bound, since one just needs to search for the $n$th Zhang prime until it is found. Zhang's result says this search will eventually terminate!
By well-known facts of primitive recursive functions, if such a primitive recursive upper bound $f(n)$ exists, then the function $n \mapsto z_n$ is itself primitive recursive.
The function $p(n)$, which returns the $n$th prime, is primitive recursive since Euclid's proof shows that there is a prime somewhere between $p(n) + 1$ and $p(n)! + 1$.