What complexity class is Bitcoin's proof-of-work (hashcash) in?
There's a reason cryptographic hash functions, like the double SHA256 used for proof-of-work in Bitcoin, are not usually described using these complexity classes that classify asymptotic behavior. In fact, there are several.


A technical reason is that hash functions often do not scale. For example, it is not defined how one would extend the proof-of-work to operate on 512 bits. A natural choice would be to use SHA512 then, but going from SHA256 to SHA512 takes alot of essentially arbitrary choices, like changing the number of rounds from 64 to 80, which are standardized but not in a naturally scaling way and not for arbitrarily large hash sizes.
It is not relevant for the cryptographer. Even a NP-complete hash function, which would be the strongest amongst the complexity cases you listed for building a strong hash, does not guarantee all what we want from either a cryptographic hash or a proof-of-work function. To qualify for NP-completeness is merely a strong heuristic that the problem cannot be solved by an algorithm that is, asymptotically, less than exponential. But for a good hash function we want it to be, at the very limited bitcount we choose to use it at, maximally exponential in the sense that solving it is really as hard as trying every possibility in a hash function. For its corresponding proof-of-work function with such a difficulty that only a fraction x of the output range is acceptable, this would mean that we should expect to require a number of attempts of x/2 times the size of full output range to find a proof-of-work. Anything better than that would prompt an academic to call the associated hash function broken, even if it merely reduces the number of tries in half, which would still put it in an exponential complexity class and would easily be possible even with a NP-complete function.

An impressive (but only superficially related) example of how picking something seemingly NP-complete is insufficient to get something cryptographically hard is knapsack cryptography. Of course, there the problem was that by picking special cases the complexity of the problem was reduced. The point is that even a NP-complete problem can be less difficult than indeed having to try every solution, despite it sometimes being described that way! For cryptography-grade quality, having to try every input is meant literally; for the complexity analysis, it is good enough if the asymptotic scaling remains exponential in the number of bits. So if you could reduce the problem to another NP-complete function taking only every 1000th bit as input, that would be good enough for classifying the problem as NP (and even NP-complete if a similar mapping worked in reverse), but not for being of interest for cryptographic applications.
It's difficult! And I think this difficulty has already let you astray: Even your arguments for placing this problem in TFNP are, whilst really close to the truth, not true in the mathematical sense. For example, if I specify x=0, no y can produce hash(y) &lt; x, contradicting your assertion. If all other x are fine or if there is a required minimum value for x probably depends on how you define the "strings" y you want hashcash to operate on. For Bitcoin with a limited number of bits entering the double-SHA256, I wouldn't be surprised if x=1 also does not have a solution, i.e. if no block hash can become exactly zero. Of course we'll probably never know. In practice, it is desirable that a hash function should produce total proof-of-work functions in the way you describe, but I don't think it is a proven quality. Disclaimer: I honestly don't know. You really should ask a cryptographer.

What remains to be done to answer your question, after finding how the hash function scales and verifying that it remains polynomial for arbitrary large sizes, is just this proof that the corresponding proof-of-work function is total. If this proof can be done using the pigeon hole principle, you have shown that it is in PPP, etc.

So where is the difficulty? For example, if y has at least as many bits as x, and if we change your hashcash to have a less-than-or-equal rather just less-than, and if we are willing to multilate it further to the point that either finding a proof-of-work or the existence of a hash collision is good enough to make "hashcash" true, then the pigeon-hole principle as explained in the wikipedia article you linked to would obviously apply.

But anything less than that, as best as I can see, would not suffice to apply the pigeon-hole principle and hence would not answer the question if hashcash is in PPP or not. To again refer to your linked wikipedia article: Only for very few problems the answer is know, even for PPP. For the special cases of PPP, PPA and PPAD, it obviously gets even harder. If you find a solution, post it to an academic journal, not just here!