Often, large cardinals imply that many definable inner models and transitive sets have theories which are absolute under forcing. For example, assuming a proper class of Woodin cardinals, the theory of $L(\mathbb{R})$ is absolute under forcing in the following sense: if $V[G]$ is a set-generic extension of $V$, then $H(\omega_1)^V\preccurlyeq H(\omega_1)^{V[G]}$. See this paper of Bagaria for more facts about forcing absoluteness.

I'm curious about a possible absoluteness principle for a much larger model. The *Chang model*, $C$, is the smallest model of set theory containing all the ordinals, and closed under countable sequences. My question is:

What is the large cardinal strength of the statement, "The lightface theory of the Chang model is forcing absolute?"

That is, for every sentence $\varphi$ in the language of set theory without parameters and every set-generic extension $V[G]$, we have $C^V\models\varphi\iff C^{V[G]}\models\varphi$.

It is not at all obvious to me that this is consistent - in fact, right now I suspect it isn't - but I don't see how to get a contradiction from it.

(We can also ask the same question involving *some* parameters - say, *real* parameters - of sufficiently low complexity that the obvious way of building a contradiction doesn't work. However, I don't want to get greedy - for now I'm interested in specifically the purely lightface version.)