Weak bounded arithmetic, the Diffie-Hellman problem and Constable´s Class K

The bounded arithmetic theory C₂⁰, which is closely related to the complexity class DLogTime-uniform TC⁰, is extended by a function symbol and axioms for integer division, which is not known to be in DLogTime-uniform TC⁰. About this extended theory C₂⁰[div], two main results are proved: (1). The Z₁^b-definable functions of C₂⁰[div] are exactly Constable´s class K, a function algebra whose precise complexity-theoretic nature is yet to be determined. This also yields the new upper bound K⊆uniform NC² . (2). The Δ₁^b-theorems C₂ ⁰[div] do not have Craig-interpolants of polynomial circuit size, unless the Diffie-Hellman key exchange protocol is insecure