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?
Finding the input x such that f(x) == argmax(f(x)) is left as an exercise for the reader though.
Oh, indeed I was getting confused between those. So as a concrete example of your proof we could consider the following degenerate example case
def f(N: int) -> int:
if N == 0x855bdad365f9331421ab4b13737917cf97b5e8d26246a14c9af1adb060f9724a:
return 1
else:
return 0
def check(x: int, y: float) -> bool:
return f(x) >= y
def argsat(y: float, max_search: int = 2**64) -> int or None:
# We postulate that we have this function because P=NP
if y > 1:
return None
elif y <= 0:
return 0
else:
return 0x855bdad365f9331421ab4b13737917cf97b5e8d26246a14c9af1adb060f9724abut we could also replace our degenerate f with e.g. sha256.
Is that the gist of your proof sketch?
I'm looking for recommendations for frameworks/tools/setups that could facilitate machine checked math manipulations.
More details:
Finding the input
xsuch thatf(x) == argmax(f(x))is left as an exercise for the reader though.