Basic arithmetic operations +, -, *, / belong to the complexity class TC^0, and it is a natural question what can be proved about them in the corresponding theory of arithmetic VTC^0. It has been known that the theory VTC^0 + IMUL including an axiom expressing the totality of iterated multiplication \prod_{i=0}^n X_i proves quite a lot: it can formalize root finding for constant-degree polynomials, and as a consequence, it proves the RSUV-translation of IOpen, and more generally, of induction and minimization for sharply bounded formulas in Buss's language.
This left open the problem whether IMUL is itself provable in VTC^0, which effectively calls for the formalization of the TC^0 iterated multiplication algorithm due to Hesse, Allender, and Barrington.
Even though the analysis of the HAB algorithm is in principle fairly elementary, it has some peculiar features that make its formalization quite challenging: in particular, it suffers from serious "chicken or egg"-type problems (the analysis heavily uses various iterated products and divisions, whose existence in VTC^0 a priori requires the very IMUL axiom we'd like to prove).
In this talk, we will show that IMUL is, after all, provable in VTC^0. We will outline the main challenges and ways how to get around them. As a byproduct, we will obtain a well-behaved \Delta_0 definition of modular exponentiation in the theory I\Delta_0 + WPHP(\Delta_0).
