Are there any proofs that BQP is not in P? In laymen's terms, I am asking if there is any formal proof separating the complexity class that quantum computers are presently assumed to solve efficiently from the complexity class that non-quantum computers are presently known to solve efficiently.
Obviously I'm not talking here about black box/oracle proofs that show they are nonequivalent if we have access to some theoretical oracle. Just talking about regular, normal equivalence.