Does P/poly $\neq$ NP/poly have any interesting implications?

Question

$P/poly = NP/poly$ implies $NP \subseteq P/poly$, which in turn has interesting consequences like the collapse of the polynomial hierarchy.

Are there interesting implications for $P/poly \neq NP/poly$?

Answer 1

Emil Jeřábek' comment answers the question:

P/poly $=$ NP/poly is equivalent to NP $\subseteq$ P/poly

Note the corollary

P/poly $\neq$ NP/poly implies P $\neq$ NP.

Proof of corollary:

1. P/poly $=$ NP/poly is equivalent to NP $\subseteq$ P/poly $\ $ (Emil's comment)
2. NP $\subseteq$ P/poly implies P/poly $=$ NP/poly $\ $ (implied by 1.)
3. P/poly $\neq$ NP/poly implies NP $\not\subseteq$ P/poly $\ $ (equivalent to 2.)
4. NP $\not\subseteq$ P/poly implies P $\neq$ NP $\ $ (P $\subseteq$ P/poly)
5. P/poly $\neq$ NP/poly implies P $\neq$ NP $\ $ (implied by 3. and 4.)

Proof of Emil's comment: It is sufficient to show that NP $\subseteq$ P/poly implies P/poly $=$ NP/poly.

1. So let's assume NP $\subseteq$ P/poly.
2. Because SAT $\in$ NP there exists $p_{SAT}\geq k_{SAT}>0$ and a sequence of advice strings $s_n$ with $\left|s_n\right|\leq n^{k_{SAT}}$, a deterministic algorithm that can decide SAT instances of size $n$ in time $\leq n^{p_{SAT}}$, if it has access to $s_n$. WLOG, that algorithm can also decide SAT instances of size $\leq n$, because we can define a modified sequence $s'_n=s'_{n-1}s_n$ with $\left|s'_n\right|\leq n^{k_{SAT}+1}$, where all previous advice strings are included in $s'_n$.
3. Now let $L\in$ NP/poly be an arbitrary language, for which we need to show $L\in$ P/poly. There exists $p_L\geq k_L>0$ and a sequence of advice strings $l_n$ with $\left|l_n\right|\leq n^{k_L}$ and a nondeterministic algorithm that can decide $L$ instances of size $n$ in time $\leq n^{p_L}$, if it has access to $l_n$.
4. For each $w$ with $|w|=n$, a SAT instance of size $\leq c\cdot n^{p_L}$ can be computed (in time $O(n^{p_L})$) that is satisfiable exactly if $w\in L$.
5. So for the sequence of advice strings $t_n=l_ns_{c\cdot n^{p_L}}$ with $|t_n|\leq n^{k_L}+(c\cdot n^{p_L})^{k_{SAT}}$, the combination of the deterministic algorithms from 2. and 4. gives a deterministic algorithm that can decide $L$ instances of size $n$ in time $O((c\cdot n^{p_L})^{p_{SAT}})$, if it has access to $t_n$.
6. Because $L\in$ NP/poly was an arbitrary language, this shows NP/poly $\subseteq$ P/poly, under the assumption that NP $\subseteq$ P/poly.

---

All the above proofs relativize, because the existence of NP-complete problems is also true in relativized worlds. This suggests that it is fruitless to search for a proof that P/poly $\neq$ NP/poly. However let's summarize the removed motivation section from the question as "The advice string could be a formal axiomatic system (automatically guaranteed to be consistent, evil grin) whose strength is quickly increasing with input length, and NP is extermely good at exploiting this advice." If one is not very careful that "existence of a sequence of advice stings" only has "formal" meaning relative to a fixed formal system, that setup is likely to allow the construction of apparent paradoxes. But the construction of such paradoxes might be fun nevertheless, and perhaps they might even suggests ways how to construct independence proofs (for sufficiently weak formal systems).