Quantum complexity of TQBF with an untrusted oracle This is a follow up to Quantum complexity of TQBF, trying to model the situation where we have good heuristics.
Let $L$ be the language of true, fully alternating totally quantified boolean formulas with some number $n$ of variables and circuit size $s = \operatorname{poly}(n)$.  The classical complexity of $L$ is $\tilde{O}\left(2^{0.793n}\right)$, and the quantum complexity is $\tilde{O}\left(2^{n/2}\right)$.
Now we assume we have access to an untrusted oracle for all subnodes of a particular formula $F \in L$.  That is, if the oracle is honest it will give the correct value of $F$ where any prefix of quantified variables is replaced by a chosen assignment of $\{0,1\}$ values.  We seek an algorithm which is correct for all oracles, untrustworthy or not, and ask for its worst-case complexity conditional on the oracle being honest.
In the classical case, I believe alpha-beta pruning is the optimal algorithm, and achieves complexity roughly $\tilde{O}\left(2^{n/2}\right)$.  (I'm not certain of this, so confirmation would be appreciated.)  Note that this matches the quantum complexity if we don't have an oracle.
Question: What is the quantum complexity of $L$ given an untrusted oracle, where complexity is measured conditional on the oracle being honest?
Motivation: The goal here is to model the situation where we have some particular TQBF, such as arising from chess or go, where there is enough structure that efficient, accurate heuristics are available but not enough structure to turn those heuristics into a rigorous proof of the game value.  In practice the heuristics would not be perfect (as in the honest oracle case), so this question is trying to get at a lower bound for the practical situation.
This question is more complicated to state than its predecessor Quantum complexity of TBQF, but in hindsight it is also way easier to answer.
Theorem: The complexity is $\tilde{O}\left(2^{n/4}\right)$, using a single call to Grover's algorithm to check if there is a path falsifying the oracle.  Moreover, this is optimal in the black box case.
Consider a TBQF query $F = \exists x_0 \forall y_0 \exists x_1 \forall y_1 \cdots f(x, y)$.  Assume w.l.o.g. that the oracle says $F$ is true.  The oracle is telling the truth about $F$ if, when we use the oracle to choose how to play each $x_k$ move, there is no choice of $y$'s that falsifies the oracle.  But this is just a single call to Grover to search through the space of such $y$'s.  There are $2^{n/2}$ $y$'s, so the complexity is $\tilde{O}\left(\sqrt{2^{n/2}}\right) = \tilde{O}\left(2^{n/4}\right)$.
For the black box lower bound, given a black box boolean function $f(y)$ defined on $n/2$ bits $y$, we can construct a degenerate TBQF formula $F = \exists x_0 \forall y_0 \exists x_1 \forall y_1 \cdots f(y)$ which simply ignores $x$.
(Thanks to Paul Christiano for discussion.)