Uniform, integral and efficient proofs for the determinant identities

We give a uniform and integral version of the short propositional proofs for the determinant identities demonstrated over GF(2) in Hrubeš-Tzameret [9]. Specifically, we show that the multiplicativity of the determinant function over the integers is provable in the bounded arithmetic theory VNC2, which is a first-order theory corresponding to the complexity class NC2. This also establishes the existence of uniform polynomial-size and O(log2n)-depth Circuit-Frege (equivalently, Extended Frege) proofs over the integers, of the basic determinant identities (previous proofs hold only over GF(2)). In doing so, we give uniform NC2-algorithms for homogenizing algebraic circuits, balancing algebraic circuits (given as input an upper bound on the syntactic-degree of the circuit), and converting circuits with divisions into circuits with a single division gate—all (Σ1B-) definable in VNC2. This also implies an NC2-algorithm for evaluating algebraic circuits of any depth.