This is the precisely the point I am trying to make :

A candidate solution function can take a very small finite space : much smaller than the number of gamestates. And we can invalidate a candidate solution by finding a single counter example.

Current chess engine can't be invalidated quickly : they are not trying to solve chess. They are not falsifiable. They are not attempting to precisely define the frontier which is what I think where remaining efforts should be made.

We are just trying to encode the frontier like we would with a mandelbrot fractal.

Proving that a solution is valid is harder than finding a solution. Here I am suggesting we find the solution first.

Proving can also be done without exploring all legal chess positions. For example you can use branch and bound to cull vast amount of state space once you have your function. You just have to partition the state space and prove on each partition that the function is constant, for example when one side has 8 queen and the other has only a king with freedom of movement the position is winnable and you don't have to check every gamestate.

I am stating that there is a good chance that by searching for a function we will stumble upon one which has no counter example, because precisely the complexity of chess is not infinite (unproven conjecture (no-turing completeness of adversarial chess) ). We should be looking for it.