On small-depth Frege proofs for PHP

We study Frege proofs for the one-to-one graph Pigeon Hole Principle defined on the $n \times n$ grid where n is odd. We are interested in the case where each formula in the proof is a depth d formula in the basis given by $\wedge, \vee$, and $\neg$. We prove that in this situation the proof needs to be of size exponential in $n^{\Omega(1 / d)}$. If we restrict the size of each line in the proof to be of size M then the number of lines needed is exponential in $n /(\log M)^{O(d)}$. The main technical component of the proofs is to design a new family of random restrictions and to prove the appropriate switching lemmas.