Does there exist any unrelativized separation between a quantum complexity class and a classical one?

I'm familiar with results of relativized separation for BPP-BQP, BQP-PH and NPC-BQP. I'm also aware that while e.g. Factoring is not believed to be in BPP, it hasn't been proven and so we're not quite near proving BQP!=BPP.

My question is, do we have any certain, theoretical, unrelativized proof that quantum computers are "superior" to classical one on any specific problem - Where here, I define superior to include any sort of runtime complexity superiority, so e.g. a quadratic improvement would qualify in this regard.

I'd expect Grover's algorithm to qualify for this criterion - But despite being supposedly "obvious", I'm not sure if it's been proven that classical computers can't solve it in sqrt(n) time as well, in a non-black-box model (i.e. unrelativized).

Separations are known for constant-depth circuits. One recent result in this area is due to Bravyi, Gosset, and Koenig (see also the journal version in Science). Recent independent works by Bene Watts, Kothari, Schaeffer, and Tal, Coudron, Stark and Vidick, and Le Gall strengthened the hardness result for classical circuits from worst-case hardness to average-case hardness.

StackExchange Computer Science Q#115791, answer score: 2