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 [J. ACM, 65(6):37:1–55, 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 unrestricted IPS the paradigm introduced in Forbes, Shpilka, Tzameret and Wigderson [Theory Comput., 17:1–88, 2021] 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:

Conditional IPS lower bounds: The Shub–Smale hypothesis [Duke Math. J., 81:47-54, 1995] implies a superpolynomial lower bound on the size of IPS refutations of the binary value principle over the rationals defined as the unsatisfiable linear equation ∑n i=1 2i−1xi = −1, for Boolean xi’s. Further, the related and more widely known τ -conjecture [Duke Math. J., 81:47-54, 1995] implies
a superpolynomial lower bound on the size of IPS refutations of a variant of the binary value principle over the ring of rational functions. No prior conditional lower bounds were known for IPS or apparently weaker propositional proof systems such as Frege systems (though our
lower bounds do not translate to Frege lower bounds since the hard instances are not Boolean formulas).