We study Frege proofs for the functional and onto graph Pigeon Hole Principle defined on the n x 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 A, v, and We prove that in this situation the proof needs to be of size exponential in nΩ(1/𝑑). If we restrict each line in the proof to be of size Μ then the number of lines needed is exponential in nO(d). The main technical component of the proofs is to design a new family of random restrictions and to prove the appropriate switching lemmas.
QC 20260310