Indications that strengthen the conjecture: NEXP ⊊ EXP^NP

Question

I am trying to find indications that strengthen the conjecture of NEXP ⊊ EXP^NP.

Clearly NEXP ⊆ EXP^NP, and there are some hints that this inclusion is proper.

Some Examples: 1. A paper by Shuichi Hirahara: “Identifying an honest EXP^NP oracle among many”, which states that “No instance checker for EXP^NP -complete languages exists unless EXP^NP = NEXP” https://arxiv.org/abs/1502.07258

2. A paper by Laszlo Babai, Lance Fortnow and Carsten Lund: “NON-DETERMINISTIC EXPONENTIAL TIME HAS TWO-PROVER INTERACTIVE PROTOCOLS” which states that we do not know whether NEXP provers are sufficient to prove any NEXP language to a verifier, but the best upper bound we know on the power of the provers for NEXP is EXP^NP http://people.cs.uchicago.edu/~fortnow/papers/mip2.pdf

Are there any additional known results on the conjecture of NEXP ⊊ EXP^NP? What are its implications on the separation of other classes?

Thanks

Answer 1

Being pulled down by the gravitational force from $\mathrm{BPP}$, hardly any convincing evidence can be lurking on the surface of $\mathrm{EXP}^{\mathrm{NP}}$ for you to see.

Only after proving $\mathrm{BPP}\subseteq \mathrm{P}^\mathrm{NP}$, this class would give up on $\mathrm{EXP}^\mathrm{NP}$. But then, $\mathrm{EXP}$ and $\mathrm{NEXP}$ would have their chances to thrive (on their own).