Assume P≠NP.
Say there's an NP-complete decision problem:
Does $P$ have a $Q$ ?
And we have a proposition $F$ computable in polynomial time, where $F(P)$ implies the existence of a solution in the original problem.
My question is:
Is there a "natural" case such that finding $Q$ is non-polynomial (maybe NP-hard?) even if $F(P)$ is given?
Insight:
Many theorems concerning the existence of a solution of a NP-complete problem is just a polynomial-time algorithm, e.g. Chvatal-Erdos theorem, Ore's condition, Kőnig's theorem on edge-coloring bipartite graphs. I wonder whether all such theorems should be of this kind.
Of course there are counterexamples.
Let $P$ be a bunch of statements, and the decision problem is "Does $P$ have a true statement ?", and $F$ searches for statements with the form $A$ and $¬A$. Surely, $F(P)$ implies the existence of a true statement, but picking out the statement is definitely hard. However, it seems too unnatural.
This paper provides an example about finding Hamilton cycles:$|d − λ_i | ≤ c \frac{(log log n)^2}{log n(log log log n)}d$ implies Hamiltonicity, and they provide an algorithm of $n^{ clnn}$ time. I'm not sure whether there is a polynomial-time algorithm or not. If there's no such algorithm, finding Hamiltonian cycles in those graphs constitutes a case.
