Why there isn't a simpler proof of IKW

A question raised in class today was, Why can't we prove the IKW Lemma, $NEXP\subseteq P/poly\Rightarrow NEXP=EXP$, via techniques similar to Meyer's Lemma, $EXP\subseteq P/poly\Rightarrow EXP=PSPACE$?

(Recall, btw, that IKW actually get $NEXP=MA$ and Meyer actually gets $EXP={\Sigma }_2$.)

In discussing it with Or and Pranjal after class, it seems the answer is the following. In the Meyer Lemma, for a fixed $EXP$ machine, we considered the map taking the index of tableau window into the tableau window contents. That map is in $EXP$, hence in $P/poly$. So there exists a circuit $C$ of some size $n^k$ computing the map. Given x, we enumerate all circuits of that size, and accept iff one of them implicitly describes an accepting tableau; this is doable in $PSPACE$.

Why doesn't this work for $NEXP$? For $NEXP$ computations, there may be multiple accepting tableaus. Not a problem so far. Certainly the $PSPACE$ algorithm still makes sense: enumerate all circuits of some fixed poly-size, and if one of them implicitly describes an accepting tableau, accept. The question is, if $x$ is in the language, will there be a fixed poly-size circuit describing an accepting tableau?

One has to be careful. There is no longer a clear meaning for "the map that takes a tableau window index to the tableau window contents", since there are multiple valid tableaus. Perhaps that's okay; perhaps we can allow for "multivalued functions". But still, there isn't a clear meaning for "this map is computable in $NEXP$ and hence in $P/poly$". The reason is, the usual meaning of an NTM computing a function is that some branches reject, and the ones that accept output valid answers. Such a model indeed computes a multi-valued function. However since it's not a decision problem (a language), it's not clear how we can get anything out of the assumption $NEXP\subseteq P/\backslash poly$.

One way around this, as Or suggested, would be to make everything single-valued by looking at the lexicographically least accepting tableaus. Unfortunately, as we saw on Homework 2, this lexicographically least satisfying assignments characterize the lass $P^{NP}$, not $NP$. All is not lost, though; a paper of Bourke uses such ideas to show $EX{P}^{NP\left[t\right(n\left)\right]}\subseteq P/poly\Rightarrow EX{P}^{NP\left[t\right(n\left)\right]}=MA$ (where the notation indicates that the $EXP$ machine makes $t\left(n\right)$ queries to the oracle). This is related to Buhrman and Homer's old extension of Karp-Lipton: $EX{P}^{NP}\subseteq P/poly\Rightarrow EX{P}^{NP}={\Sigma }_2$.