Is there any known $NP$-complete problem which hardness proof is non-constructive.
A constructive $NP$-completeness proof is a proof that $L_1\leq_p L_2$ by a reduction $r$ and from the argument therein, one can extract two polynomial-time algorithms $f$ and $g$ such that:
For every instance $x\in L_1$, given a certificate $w_1$ for $x$, we must have that $w_2=f(w_1)$ is a certificate for $r(x)\in L_2$
For every instance $x\in L_1$, given a certificate $w_2$ for $r(x)\in L_2$, we must have that $w_1=g(w_2)$ is a certificate for $x\in L_1$.
In $NP$-completeness result, that does not describe $f$ and $g$, we can say that it is a non-constructive proof. Given a certificate for an instance of $L_1$, one does not know how to construct a certificate for the corresponding instance of $L_2$ and vice versa.
In a sense, the proof only establishes the existence of corresponding certificates.
More specifically, do we have an existence-only proof for some $NP$-complete problem?