The (extended) Binary Value Principle (eBVP, the equation $\sum x_i 2^{i-1} = -k$ for $k > 0$
and in the presence of $x_i^2=x_i$) has received a lot of attention recently, several lower
bounds have been proved for it [Alekseev et al 20, Alekseev 21, Part and Tzameret 21].
Also it has been shown [Alekseev et al 20] that the
probabilistically verifiable Ideal Proof System (IPS) [Grochow and Pitassi 18] together with eBVP
polynomially simulates a similar semialgebraic proof system. In this paper we consider
Polynomial Calculus with the algebraic version of Tseitin’s extension rule (Ext-PC). Contrary
to IPS, this is a Cook--Reckhow proof system. We show that in this context eBVP still allows
to simulate similar semialgebraic systems. We also prove that it allows to simulate the
Square Root Rule [Grigoriev and Hirsch 03], which is in sharp contrast with the result of [Alekseev 21] that shows
an exponential lower bound on the size of Ext-PC derivations of the Binary Value Principle
from its square. On the other hand, we demonstrate that eBVP probably does not help in
proving exponential lower bounds for Boolean formulas: we show that an Ext-PC (even with
the Square Root Rule) derivation of any unsatisfiable Boolean formula in CNF from eBVP
must be of exponential size.