Stronger versions of P != NP which better express actual convictions

Question

Does the conviction "L-uniform NC¹ != NP is incredibly hard to prove!" express the core of "P != NP is incredibly hard to prove!" in a similar spirit as the conviction "The polynomial hierarchy doesn't collapse!" expresses the core of "P is not equal to NP!" ? Let me try to elaborate:

The P vs NP problem implicitly invokes a number of related but distinct challenges and convictions. Focusing on the convictions, we have that NP != coNP is believed with nearly the same conviction as P != NP, and is part of the conviction that the polynomial hierarchy doesn't collapse. (Because the polynomial hierarchy is less familiar than NP, this conviction is weaker, but still strong enough to be used as a reasonable assumption in a proof.)

Similarly, "L != NP is incredibly hard to prove" is believed with nearly the same conviction as "P != NP is incredibly hard to prove". Now there may be weaker statements which we don't know how to prove either, like "$U_{E^*}$-uniform TC⁰ != PH", but they don't necessarily feel natural enough to be part of real convictions. So my question is whether "L-uniform NC¹ != NP is incredibly hard to prove" would qualify as a natural (and sufficiently strong) conviction. (I'm pretty certain that "NC¹" is appropriate here, but I'm less certain about "L-uniform" and "NP". Maybe something like "non-uniform NC¹ != PH/poly is incredibly hard to prove" would be much more natural and somehow imply all the other related natural convictions.)

Answer 1

Considering that the conviction "P != NP is incredibly hard to prove" is largely based on known barrier results, one promising approach (for answering this question) would be to look for a statement expressing a natural separation, and ask why it is hard to prove. Then one can check which of the known barrier results for P != NP can be extended to that statement.

The question "Why is it hard to prove ALogTime != PH?" should be most promising in this respect. This statement is weaker and more natural than "L-uniform NC¹ != NP", because $\subset$ PH and

ALogTime = DLogTime-uniform NC¹ = $U_{E^*}$-uniform NC¹ $\subset$ L-uniform NC¹.

For the relativization barrier, it would be enough to show ALogTime^A = PH^A for A := TQBF, where TQBF is the PSPACE-complete problem to decide true quantified Boolean formulas. No idea whether the natural proofs and the algebrizing proofs barrier should be expected to carry over, but at least checking whether they do should not be terribly difficult.

---

I also wonder whether the statement "ALogTime != PH" points to the right place where the difficulties for proving separation results start. Below ALogTime, we have the logarithmic time hierarchy LH, which probably doesn't collapse either, but the question is whether this has been proved (or whether this is relatively easy to prove, just in case nobody cared yet).

Edit: It turns out somebody actually cared to prove that the logarithmic time hierarchy is strict, and how it is related to the AC⁰ hierarchy. See Searching Constant Width Mazes Captures the AC⁰ Hierarchy by Barrington et al. I didn't check which results were already proved in one of the references, and which results have been proved for the first time in that paper.

This means that the statement "ALogTime != PH" is exactly the place where the difficulties for proving separation results start. It may be noted that this statement is actually equivalent to "ALogTime != NP", since "ALogTime = NP" would imply "P=NP=PH". Observe that (it seems that) coNLogTime verification can be used instead of PTime verification when characterising NP, so this is actually really equivalent to a statement where "polynomial time" no longer occurs, only some version of "read only polynomial length witness string".