[cvoss]

I'm not sure this really addresses GP's question, which I share.

You claimed in GGP that deciding whether a function is total is a TFNP problem. In particular, that would make it decidable. But the counter-claim is that deciding whether a function is total is actually an undecidable problem.

I've also examined a definition of TFNP and I don't see how it is related to the problem of deciding if a function is total. Rather, the definition seems to require that the function in question be total.