This is a special post for quick takes by kman. Only they can create top-level comments. Comments here also appear on the Quick Takes page and All Posts page.
Something I didn't realize until now: P = NP would imply that finding the argmax of arbitrary polynomial time (P-time) functions could be done in P-time.
Proof sketch
Suppose you have some polynomial time function f: N -> Q. Since f is P-time, if we feed it an n-bit input x it will output a y with at most max_output_bits(n) bits as output, where max_output_bits(n) is at most polynomial in n. Denote y_max and y_min as the largest and smallest rational numbers encodable in max_output_bits(n) bits.
Now define check(x, y) := f(x) >= y, and argsat(y) := x such that check(x, y) else None. argsat(y) is in FNP, and thus runs in P-time if P = NP. Now we can find argmax(f(x)) by running a binary search over all values y in [y_min, y_max] on the function argsat(y). The binary search will call argsat(y) at most max_output_bits(n) times, and P x P = P.
I'd previously thought of argmax as necessarily exponential time, since something being an optimum is a global property of all evaluations of the function, rather than a local property of one evaluation.
This is a cool fact I hadn't been aware of. An alternative sketch (it might be nonsense, not being careful):
If P = NP then P = co-NP. The problem of "given x, say yes if x is the argmax of f" is co-NP, because you can polynomially verify "no" answers: a witness is y such that f(y) > f(x). So this is in P, i.e. we can polynomially answer "is this the argmax". Since we can polynomially verify this, the map from polytime TMs for some f, to argmax, is in FNP. (<- This step is the one I'm slightly unconfident about but seems right.) So this map is in P since FNP = P (presumably).
I think this is spiritually quite similar to your proof, except that the binary search thing isn't necessary?