An exponential lower bound for the bit pigeonhole principle in resolution over parities

Claimed: for every $l >= 32$, any dag-like $\mathrm{Res}(\oplus)$ refutation of the bit pigeonhole principle with $2^l + 1$ pigeons and $n = 2^l$ holes has more than $exp(n/(32768 l^2)) = 2^{\Omega(n/log^2 n)}$ nodes; exponential in the number of holes up to a $log^2$ factor, for a proof system with no regularity or depth restriction. The whitepaper's route is a transfer to degree-$O(log n)$ polynomial calculus. Candidate: kernel-checked, read by no specialist.

Claimed: for every $l >= 32$, any dag-like $\mathrm{Res}(\oplus)$ refutation of the bit pigeonhole principle with $2^l + 1$ pigeons and $n = 2^l$ holes has more than $exp(n/(32768 l^2)) = 2^{\Omega(n/log^2 n)}$ nodes; exponential in the number of holes up to a $log^2$ factor, for a proof system with no regularity or depth restriction. The whitepaper's route is a transfer to degree-$O(log n)$ polynomial calculus. Candidate: kernel-checked, read by no specialist.