@PhilipWelch Could you elaborate on the illfounded ordering of $L_{\omega_1^{ck}}$? I'm not sure where it comes from.

@Collapse I agree that what is written is your interpretation but it seems to me that this wasn't intended by the author. As I've suspected, this property is meant to capture well-foundedness of the ultrapower and the version I've proved suffices to conclude that. Maybe the stronger version is true as well, but I remain doubtful about that.

@Collapse I'm fairly certain that this is the general case. If you don't have $((a_n, x_n) \mid n < \omega) \in M$, I suspect there will be counterexamples. Also note that you want $\omega$-completeness (that's the name for the property we consider here) to show that $\mathrm{Ult}(M;E)$ is well-founded. The prove above suffices to conclude that.

In this answer I assume that $((a_n,x_n) \mid n < \omega) \in M$ but not that $E \in M$. I also get a slightly better result than required since $f \in M$. If we don't assume that the sequences $(a_n \mid n < \omega), (x_n \mid n < \omega)$ are in $M$, I don't even know where to begin...

As far as I can tell, we need an additional assumption here. May we assume that $E \in M$?

Can you elaborate on your after note? I'm not sure that I get what it's saying.

@David I have a candidate for that: $\mathrm{CH}$ holds if and only if the plane $\mathbb R^2$ can be covered by 3 clouds. (See here.) With a little more work you can actually squeeze out a characterization of $2^{\aleph_0} = \aleph_n$ for all $n < \omega$ -- a result we rediscovered over lunch during least year's Arctic Set Theory Conference.

Thank you, Victoria. That's precisely what I was looking for.

That's precisely what I've been doing so far. The motivation behind my question is that I was hoping there might be a -- for lack of a better phrase -- more uniform approach dealing with classes in forcing extensions that I just haven't heard of, yet. It's, of course, entirely possible that this approach is doomed to fail.

"Why are you trying to define $\mathbb P$-names for classes?" Because I'd like to use them, if possible. "The class-extension axiom requires an explicit formula which is not allowed to quantify over arbitrary classes." Fair enough. What about MK then? (And yes, there are still issues regarding the class of all class names... but it seems like we can deal with that like we do in ZFC with classes, since the relevant $2$-classes are definable.)

I find it very likely that someone else has asked this, or a very similar question, before. But in my (admittedly short) search for duplicates, the only related question I found was this.