The Shrinkage Exponent of de Morgan Formulas is 2

We prove that if we hit a de Morgan formula of size L with a random restriction from R p , then the expected remaining size is at most O(p²(log 1/p)3/2L+p√ L). As a corollary we obtain an Ω(n³⁻ᵒ⁽¹⁾)-formula-size lower bound for an explicit function in P. This is the strongest known lower bound for any explicit function in NP.