Hm, so let's see; you started off mocking the impossibility and infeasibility of AIXI and any computable version:

I am not persuaded that the harder Bayesians have any more concrete answer. Solmonoff induction is uncomputable and seems to unnaturally favour short hypotheses involving Busy-Beaver-sized numbers. And any computable approximation to it looks to me like brute-forcing an NP-hard problem.

Then you admitted that actually every working solution can be seen as a form of SI/AIXI:

There might well be a theorem formalising that statement. There might also be one formalising the statement that every remotely optimal form of induction or decision-making is uncomputable. If that's the way it is, well, that's the way it is... Since AIXI is, by construction, the best possible intelligent agent, all work on AGI can, in a rather useless sense, be described as an approximation to AIXI

And now you're down to arguing that it'll be "very useful, but not AGI".

Well, I guess I can settle for that.