Semi-Algebraic Proofs, IPS Lower Bounds and the $\tau$-Conjecture: Can a Natural Number be Negative?

TL;DR

This paper introduces the binary value principle to connect proof complexity with algebraic and semi-algebraic systems, providing conditional lower bounds and insights into the strength of IPS and related proof systems.

Contribution

It establishes conditional superpolynomial lower bounds for IPS refutations of the binary value principle based on a hypothesis about factorials, and shows how short IPS refutations relate algebraic and semi-algebraic proof systems.

Findings

Conditional superpolynomial lower bounds on IPS refutations based on factorial hardness hypothesis

Short IPS refutations connect algebraic and semi-algebraic proof systems

The binary value principle captures the advantage of semi-algebraic over algebraic reasoning

Abstract

We introduce the binary value principle which is a simple subset-sum instance expressing that a natural number written in binary cannot be negative, relating it to central problems in proof and algebraic complexity. We prove conditional superpolynomial lower bounds on the Ideal Proof System (IPS) refutation size of this instance, based on a well-known hypothesis by Shub and Smale about the hardness of computing factorials, where IPS is the strong algebraic proof system introduced by Grochow and Pitassi (2018). Conversely, we show that short IPS refutations of this instance bridge the gap between sufficiently strong algebraic and semi-algebraic proof systems. Our results extend to full-fledged IPS the paradigm introduced in Forbes et al. (2016), whereby lower bounds against subsystems of IPS were obtained using restricted algebraic circuit lower bounds, and demonstrate that the binary value principle captures the advantage of semi-algebraic over algebraic reasoning, for sufficiently strong systems. Specifically, we show the following: (abstract continues in document.)