NP-completeness separates membership and hardness

For every language $L\subseteq B^*$, the predicate called NPComplete, defined by $L\in NP\land\forall A\subseteq B^*,\ A\in NP\Rightarrow A\preceq L$, is equivalent to $L\in NP$ conjoined with the predicate called NPHard, which is itself defined by $\forall A\subseteq B^*,\ A\in NP\Rightarrow A\preceq L$. Both sides therefore assert membership in the checker-defined class and reductions from every language of that class. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length. The set $NP$ consists exactly of languages $L\subseteq B^*$ for which there exist $R:B^*\times B^*\to B$ and $k\in\mathbb N$ satisfying $C(R)$ and $\forall w\in B^*,\ w\in L\ \Longleftrightarrow\ \exists y\in B^*,\ |y|\le |w|^k\ \land\ R(w,y)=\mathrm{true}$. This includes $k=0$ and empty input: $0^0=1$, whereas $0^k=0$ for $k>0$. Write $C(R)$ for existence of such a machine and a polynomial $p\in\mathbb N[X]$ that, for all $w,y\in B^*$, compute $[R(w,y)]$ in at most $p(|w|+|y|)$ steps from the list obtained by tagging every bit of $w$ with the left injection into $B\sqcup B$, tagging every bit of $y$ with the right injection, and concatenating those two lists. For languages $A,B_0\subseteq B^*$, write $A\preceq B_0$ to mean that there exists $f:B^*\to B^*$ satisfying $F(f)$ and $\forall w\in B^*,\ w\in A\ \Longleftrightarrow\ f(w)\in B_0$. Write $F(f)$ for existence of such a machine and a polynomial $p\in\mathbb N[X]$ that, for every $w\in B^*$, compute output list $f(w)$ from input list $w$ in at most $p(|w|)$ steps. Different existential computation witnesses may use different machines and polynomials. A machine in these assertions is a Mathlib TM2 stack machine with finitely many stack indices, instruction labels, and control states, a finite input-stack alphabet, designated input and output stacks, a program, and initial label and control state; its other stack alphabets need not be finite. Input and output alphabet bijections transport the specified encoded lists to the corresponding stack alphabets. Computation starts with only the input stack populated, and reaches a halted configuration with the specified output on the output stack, all other stacks empty, and the control state reset to its initial value. Time counts executions of whole TM2 statements, each of which may contain several stack operations.