This is useful information, thank you for sharing this theorem! I am still skeptical about the soundness of the verifier's challenge generating mechanism. Assuming P!=NP and the challenge is drawn uniformly from the full space, I am still not convinced that the prover does not have access to a backdoor which makes the challenge "easier" on average than the challenger realizes.
Even if challenge instances are superpolynomial in the worst case, empirically, we know from SAT solving competitions that a very small fraction of randomly sampled k-SAT instances are truly hard and most are in P. It is nontrivial to design a challenge whose average case is superpolynomial, and there are many open questions in the field of average-case complexity [1].
I would be very skeptical that the challenge generator is not somehow poisoned. Even if the prover did not collude with the protocol designer to poison it directly, if she can infer any information about the internal state of the verifier from the instances he proposes, she may be able to solve future challenges much more easily than would be possible by random chance.
[1]: https://arxiv.org/pdf/cs/0606037.pdf