We prove lower bounds for proofs of the bit pigeonhole principle (BPHP) and its generalizations in bounded-depth resolution over parities (Res$(\oplus)$). For weak BPHP$_n^m$ with $m = cn$ pigeons (for any constant $c > 1$) and $n$ holes, for all $\epsilon > 0$, we prove that any depth $N^{1.5 - \epsilon}$ proof in Res$(\oplus)$ must have size $\exp(\widetilde{\Omega}(N^{2\epsilon}))$, where $N = cn\log n$ is the number of variables.

Inspired by recent work in TFNP on multicollision-finding, we consider a generalization of the bit pigeonhole principle, denoted $t$-BPHP$_n^m$, asserting that there is a map from $[m]$ to $[n]$ ($m > (t-1)n$) such that each $i \in [n]$ has fewer than $t$ preimages. We prove that any depth $N^{2-1/t-\epsilon}$ proof in Res$(\oplus)$ of $t$-BPHP$_n^{ctn}$ (for any constant $c \geq 1$) must have size $\exp(\widetilde{\Omega}(N^{\epsilon t/(t-1)}))$.

For the usual bit pigeonhole principle, we show that any depth $N^{2-\epsilon}$ Res$(\oplus)$ proof of BPHP$_n^{n+1}$ must have size $\exp(\widetilde{\Omega}(N^{\epsilon}))$. As a byproduct of our proof, we obtain that any randomized parity decision tree for the collision-finding problem with $n+1$ pigeons and $n$ holes must have depth $\Omega(n)$, which matches the upper bound coming from a deterministic decision tree.

We also prove a lifting theorem for bounded-depth Res$(\oplus)$ with a constant size gadget which lifts from $(p, q)$-DT-hardness, recently defined by Bhattacharya and Chattopadhyay (2025). By combining our lifting theorem with the $(\Omega(n), \Omega(n))$-DT-hardness of the $n$-variate Tseitin contradiction over a suitable expander, proved by Bhattacharya and Chattopadhyay, we obtain an $N$-variate constant-width unsatisfiable CNF formula with $O(N)$ clauses for which any depth $N^{2-\epsilon}$ Res$(\oplus)$ proof requires size $\exp(\Omega(N^\epsilon))$. Previously no superpolynomial lower bounds were known for Res$(\oplus)$ proofs when the depth is superlinear in the size of the formula (instead of the number of variables).

Added some new results and a more detailed proof overview of the lower bound for weak BPHP.

We prove that for the bit pigeonhole principle with any number of pigeons and $n$ holes, any depth $D$ proof in resolution over parities must have size $\exp(\Omega(n^3/D^2))$. Our proof uses the random walk with restarts approach of Alekseev and Itsykson [STOC '25], along with ideas from recent simulation theorems for randomized parity decision trees.