I am a PhD student in computer science at the University of Waterloo, supervised by Professor Ming Li and advised by Professor Marcus Hutter.
My current research is related to applications of algorithmic probability to sequential decision theory (universal artificial intelligence). Recently I have been trying to start a dialogue between the computational cognitive science and UAI communities (if this includes you, consider contacting me about the reading group). Sometimes I build robots, professionally or otherwise. Another hobby (and a personal favorite of my posts here) is the Sherlockian abduction master list, which is a crowdsourced project seeking to make "Sherlock Holmes" style inference feasible by compiling observational cues. Give it a read and see if you can contribute!
See my personal website colewyeth.com for an overview of my interests and work.
The definition you settled on in your paper (using rejection sampling) only works for estimable weights, so cannot be extended to the lower semicomputable weights usually used for Solomonoff induction (e.g. 2^{-K(<T>)}). The alternative construction in "A formal solution to the grain of truth problem," when properly formalized, works with lower semicomputable weights.
This is a nitpick, but technically to apply the closed graph property instead of upper semicontinuity in Kakutani's fixed point theorem, I believe you need to know that your LCTVS is metrizable. It is sufficient to show it has a countable local base by Theorem 9 of Rudin's functional analysis, which is true because you've taken a countable power of R, but would not necessarily hold for any power of R (?).
I don't find these intuitive arguments reliable. In particular, I doubt it is meaningful to say that reflective oracle AIXI takes the complexity of its own counterfactual actions into account when weighing decisions. This is not how its prior works or interacts with its action choice. I don't fully understand your intuition, and perhaps you're discussing how it reasons about other agents in the environment, but this is much more complicated than you imply, and probably depends on the choice of reflective oracle. (I am doing a PhD related to this).
What would you have to see proven about Solomonoff induction to conclude it does not have convergence/calibration problems? My friend Aram Ebtekar has worked on showing it converges to 50% on adversarial sequences.