Nondeterministic NC1 computation

We define the counting classes NC¹, GapNC¹ PNC¹ and C₌NC¹. We prove that Boolean circuits, algebraic circuits, programs over nondeterministic finite automata, and programs over constant integer matrices yield equivalent definitions of the latter three classes. We investigate closure properties. We observe that NC¹⊆L and that C₌NC¹⊆L. Then we exploit our finite automaton model and extend the padding techniques used to investigate leaf languages. Finally, we draw some consequences from the resulting body of leaf language characterizations of complexity classes, including the unconditional separation of ACC⁰ from MOD-PH as well as that of TC⁰ from the counting hierarchy. Moreover we obtain that dlogtime-uniformity and logspace-uniformity for AC⁰ coincide if and only if the polynomial time hierarchy equals PSPACE