What if an $\mathsf L$-complete problem has $\mathsf{NC}^1$ circuits? More generally, what evidence is there against $\mathsf{NC}^1=\mathsf{L}$?

Edit: let me reformulate the question in a more specific way (and change the title accordingly). A slightly edited version of the original question follows.

Is there a result comparable to the Karp-Lipton theorem starting from the assumption $L\in\mathsf{NC}^1/\mathsf{poly}$ with $L$ an $\mathsf L$-complete language (under, say, $\mathsf{AC}^0$ reductions)? By "comparable" I mean that it derives non-trivial consequences (perhaps considered unlikely) from the assumption.

I am having trouble finding in the literature (or online) a discussion of the relationship between $\mathsf{NC}^1$ and logarithmic space going beyond "the former is included in the latter and it is open whether the inclusion is strict". More specifically, I could find only two three pieces of evidence against equality of the two classes:

• Barrington's theorem and the characterization of non-uniform deterministic logspace in terms of branching programs gives us $\mathsf{NC}^1/\mathsf{poly}=\mathsf{L}/\mathsf{poly}$ iff bounded-width polysize branching programs are as expressive as arbitrary polysize branching programs, which I guess would be highly surprising (especially considering how surprising Barrington's theorem itself is).
• Markus Holzer [Hol02] proved that $\mathsf{NC}^1/\mathsf{poly}=\mathsf{L}/\mathsf{poly}$ iff one-head two-way non-uniform deterministic finite automata have the same expressive power whether they are oblivious or not ("oblivious" means that the movement of the head during the computation depends only on the length of the input, not on the input itself). Oblivious polytime Turing machines do have the same power as non-oblivious ones, but I guess it is hard to see how that simulation may be done in the much more restricted framework of finite automata.
• Edit: there is a paper by Allender et al. [ABCDR09] in which a number of reachability problems for certain classes of graphs are shown to be hard for $\mathsf{NC}^1$ under $\mathsf{AC}^0$ reductions, whereas the same problems are not known to be hard for $\mathsf{L}$. As stated by the authors, "this gives a cluster of natural problems that are candidates for having complexity intermediate between $\mathsf{NC}^1$ and $\mathsf{L}$".

Besides the above points and the usual empirical evidence ($\mathsf{L}$-complete problems do not seem to have logarithmic-depth bounded fan-in circuits), is there any other evidence against $\mathsf{NC}^1=\mathsf{L}$?

[Hol02] Markus Holzer. Multi-head finite automata: data-independent versus data-dependent computations. Theor. Comput. Sci. 286(1):97-116 (2002).

[ABCDR09] Eric Allender, David A. Mix Barrington, Tanmoy Chakraborty, Samir Datta and Sambuddha Roy. Planar and Grid Graph Reachability Problems. Theory Comput. Syst. 45(4):675--723 (2009).

• AP = PSPACE is no more evidence for ALOGTIME = L than PSPACE = NPSPACE is evidence for L = NL. That is, it is not evidence at all. The simulation of deterministic space by alternating time squares the bound, so the proper analogue of the “polynomial and higher cases” is APOLYLOGTIME = POLYLOGSPACE. – Emil Jeřábek Oct 9 '14 at 10:58
• @EmilJeřábek: yes, that's what I meant by "this is hardly evidence". I guess you're saying that it's pointless to even mention it. I will edit the question. – Damiano Mazza Oct 9 '14 at 14:05
• Ah, all right. I’m not saying it is pointless to mention it, but it wasn’t clear what you meant by the remark. – Emil Jeřábek Oct 10 '14 at 13:54
• FYI, the algebraic analogue is the formula size of det, for which the best known upper bound is currently quasi-poly. (Ben-Or & Cleve showed poly-size width 3 ABPs are equivalent to poly-size formulas; it is well-known that arbitrary poly-size ABPs are equivalent to poly-size projections of the determinant.) Det having poly-size formulas is not just surprising, but would likely also have consequences in proof complexity as well (e.g. whether the Hard Matrix Identities are provable in Frege, rather than $\mathsf{NC}^2$-Frege). Of course, none of this is "evidence" analogous to Karp-Lipton... – Joshua Grochow Dec 30 '17 at 3:49
• Thank you for your comment! It makes me realize how much I don't know about algebraic complexity... – Damiano Mazza Dec 31 '17 at 16:05