This construction splits the space into 'small' models with a quadratic lookup cost and 'large' with sub-exponential cost. The small one is by enumerating all SAT problems with their answers, then looking up the answer. The large one is something in polynomials I don't understand. An answer from openai about where the cutoff is was:

    the constructed lookup machine has vastly more states than the estimated total number of physically distinguishable configurations of the observable universe.

I'm not inclined to consider "wrote down all the answers ahead of time, so that's free" as a quadratic time solution to SAT. Nor very convinced by the other half.

So on balance, if this is considered proof that the exponential time hypothesis is false, and openai model reading of the lean was vaguely on point, then I reject the axioms of this system. Not a proof, even if there is lean. I'm OK with being downvoted for that position.