In this work, we prove upper and lower bounds over fields of positive characteristics for several fragments of the Ideal Proof System (IPS), an algebraic proof system introduced by Grochow and Pitassi (J. ACM 2018). Our results extend the works of Forbes, Shpilka, Tzameret, and Wigderson (Theory of Computing 2021) and also of Govindasamy, Hakoniemi, and Tzameret (FOCS 2022). These works primarily focused on proof systems over fields of characteristic $0$, and we are able to extend these results to positive characteristic.

The question of proving general IPS lower bounds over positive characteristic is motivated by the important question of proving $AC^{0}[p]$-Frege lower bounds. This connection was observed by Grochow and Pitassi (J. ACM 2018). Additional motivation comes from recent developments in algebraic complexity theory due to Forbes (CCC 2024) who showed how to extend previous lower bounds over characteristic $0$ to positive characteristic.

In our work, we adapt the functional lower bound method of Forbes et al. (Theory of Computing 2021) to prove exponential-size lower bounds for various subsystems of IPS. In order to establish these size lower bounds, we first prove a tight degree lower bound for a variant of \emph{Subset Sum} over positive characteristic. This forms the core of all our lower bounds.

Additionally, we derive upper bounds for the instances presented above. We show that they have efficient constant-depth IPS refutations. This demonstrates that constant-depth IPS refutations are stronger than the proof systems considered above even in positive characteristic. We also show that constant-depth IPS can efficiently refute a general class of instances, namely all symmetric instances, thereby further uncovering the strength of these algebraic proofs in positive characteristic.

Notably, our lower bounds hold for fields of arbitrary characteristic but require the field size to be $n^{\omega(1)}$. In a concurrent work, Elbaz, Govindasamy, Lu, and Tzameret have shown lower bounds against restricted classes of IPS over finite fields of any size by considering different hard instances.