Conditional SAT characterization

Assume four hypotheses: $P\subseteq NP$; $SAT\in NP$; $\forall L\subseteq B^*,\ L\in NP\Rightarrow L\preceq SAT$; and $\forall A,B_0\subseteq B^*,\ A\preceq B_0\Rightarrow B_0\in P\Rightarrow A\in P$. Under these supplied hypotheses, $P=NP$ if and only if $SAT\in P$. In particular the inclusion, the checker description of $SAT$, its incoming reductions, and closure of $P$ under the specified reductions are premises of this theorem rather than claims established by its statement. 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 $P$ consists exactly of languages $L\subseteq B^*$ for which there is a Boolean function $\chi:B^*\to B$ satisfying $D(\chi)$ and $\forall w\in B^*,\ w\in L\ \Longleftrightarrow\ \chi(w)=\mathrm{true}$. 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 $D(\chi)$ for existence of such a machine and a polynomial $p\in\mathbb N[X]$ that, for every $w\in B^*$, compute the singleton output $[\chi(w)]$ from input $w$ in at most $p(|w|)$ steps. 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. The language $SAT$ consists of exactly those $w\in B^*$ for which there are a formula $F$ and an assignment $\tau:\mathbb N\to B$ such that $E(F)=w$ and every clause of $F$ is true under $\tau$; strings without such an encoding are excluded. Write $E(F)$ for this Boolean-list encoding of a formula $F$: for each literal $(b,j)$, take $[b]$ followed by the little-endian canonical binary digits of $j$ (the digits of $0$ form the empty list), replace each bit $d$ by $[\mathrm{false},d]$, and append $[\mathrm{true},\mathrm{false}]$; concatenate these literal encodings within each clause and append $[\mathrm{true},\mathrm{true}]$; then concatenate the clause encodings in formula order. In particular $E([])=[]$. A formula is a finite list of clauses, each clause a finite list of literals $(b,j)\in B\times\mathbb N$. Under an assignment $\tau:\mathbb N\to B$, the literal $(b,j)$ is true exactly when $\tau(j)=b$, a clause is true exactly when some literal in it is true, and a formula is true exactly when every clause is true. Thus an empty clause is false and an empty formula is true.