How does this proof work / can someone provide a link to a paper? This is exercise 6.7 of Computational Complexity a Modern Approach. I know the following:

(1) P = NP -> EXP = NEXP (by padding) (2) exists f: {0,1}^n -> {0,1} that takes at least O(2^n/n) , by pigeon hole (3) any f:{0,1}^n -> {0,1} can be done in O(2^n/n), by Shannon's clever result from 49 (4) Looks like I'm supposed t use NEXP to "guess" a circuit of some sort.

I've also googled around, and there's references to some famous work by Razabov's work, I can't figure out which paper.

Question: What step am I missing in proving this classical, well known result?

Thanks!