Given two symbolic matrices $X$ and $Y$ of dimensions $m\times n$ and $n\times m$, respectively, the *rank principle* states that when $m = n+1$ and $A$ is a scalar matrix of rank $n+1$, the equation $XY = A$ is unsatisfiable. When $m$ is arbitrarily larger than $n$ and $A$ has rank exceeding $n$, we obtain the *weak rank principle*. We study this principle as an algebraic generalisation of the weak pigeonhole principle (WPHP), asserting that $m$ pigeons cannot be injected into $n$ holes. As a strengthening of WPHP, it admits proof complexity lower bounds in settings where none are known for WPHP, while still supporting analogous applications. Using new generalised random restrictions applied to the weak rank principle, which may be of independent interest, we resolve several open problems in proof complexity: we construct proof complexity generators for Polynomial Calculus Resolution over the two-element field (PCR$_{\mathbb{F}_2}$), new generators for Sherali--Adams (SA), and hardness results for circuit lower bound statements against PCR$_{\mathbb{F}_2}$.
GENERATORS FOR PCR$_{\mathbb{F}_2}$: We prove exponential size lower bounds for several encodings---both algebraic and CNF---of the weak rank principle in PCR over ${\mathbb{F}_2}$, where no such bounds are known for the WPHP in the regime with arbitrarily many pigeons. In particular, we obtain $2^{\Omega(n)}$ size lower bounds for both algebraic and standard CNF encodings, including the *bamboo-tree encoding*, which is the most relevant for applications and corresponds to a circuit encoding, as considered by Alekhnovich, Ben-Sasson, Razborov, and Wigderson (SIAM J. Comput., 2004) and Razborov (Ann. Math., 2015). Our bounds hold for every matrix $A$ in $XY = A$, implying that the rank principle forms a proof complexity generator with nearly quadratic stretch. Using a standard iteration technique we amplify the stretch to $2^{n^{\Omega(1)}}$, thereby obtaining a function generator. This resolves the open problem posed by Alekhnovich et al. (SIAM J. Comput., 2004) and Razborov (Ann. Math., 2015) concerning the construction of proof complexity generators with good stretch for PCR$_{\mathbb{F}_2}$.
GENERATORS FOR SHERALI-ADAMS: Since in SA even the strong pigeonhole principle is easy, we develop a new size lower-bound technique showing that the weak rank principle, encoded as a bamboo-tree CNF, serves as a proof complexity generator for SA. Our method introduces a new relaxed notion of degree and a corresponding pseudoexpectation tailored specifically to the rank principle (and incompatible with the pigeonhole principle).
CIRCUIT LOWER BOUND FORMULAS: We show that PCR$_{\mathbb{F}_2}$ does not admit short proofs of lower-bound statements against Boolean circuits, nor against weak models of algebraic circuits. This settles the open problem raised by Razborov (Ann. Math., 2015) concerning the provability of such lower bounds in PCR$_{\mathbb{F}_2}$.
STRENGTH OF THE WEAK RANK PRINCIPLE: Finally, we show that the weak rank principle is *necessary* for proving NC$^2$ circuit lower bounds and, for odd primes $p$, *sufficient* within the theory corresponding to AC$^{0}[p]$ for deriving AC$^{0}[p]$ lower bounds.
