Return to Answer

So in terms of the 4-tuples defining $<_L$, the $<_L$-least Cohen generic $c$ has tuple $(\alpha,1,\{\alpha\},k)$ for some $k<\omega$.

Assuming that $<_L\upharpoonright M$ is $M$-compatible (meaning that $(M,{<_L\upharpoonright M})$ is a model of ZFC, in the expanded language with the predicate $<_L\upharpoonright M$), we want to deduce that $M$ can understand enough about $\pi$ for a contradiction. That is, for $\beta\in\alpha\backslash\omega$ let $c_\beta=c\cup\{\beta\}$. Then note that $c_\beta$ has tuple $(\alpha,1,\{\alpha\},k_\beta)$ for some $k_\beta<\omega$ (using here the surjection $\pi:\omega\to L_\alpha$ mentioned above). But the class $C=\{c_\beta\bigm|\beta\in[\omega,\alpha)\}\subseteq M$ is definable over $M$, so if $<_L\upharpoonright M$ is $M$-compatible, then $<_L\upharpoonright C$ is too. But this is an ordering of $\mathrm{OR}^M\backslash\omega$ in ordertype $\omega$, which is impossible.

So in terms of the 4-tuples defining $<_L$, the $<_L$-least Cohen generic $c$ has tuple $(\alpha+1,1,\{\alpha\},k)$ for some $k<\omega$.

Assuming that $<_L\upharpoonright M$ is $M$-compatible (meaning that $(M,{<_L\upharpoonright M})$ is a model of ZFC, in the expanded language with the predicate $<_L\upharpoonright M$), we want to deduce that $M$ can understand enough about $\pi$ for a contradiction. That is, for $\beta\in\alpha\backslash\omega$ let $c_\beta=c\cup\{\beta\}$. Then note that $c_\beta$ has tuple $(\alpha+1,1,\{\alpha\},k_\beta)$ for some $k_\beta<\omega$ (using here the surjection $\pi:\omega\to L_\alpha$ mentioned above). But the class $C=\{c_\beta\bigm|\beta\in[\omega,\alpha)\}\subseteq M$ is definable over $M$, so if $<_L\upharpoonright M$ is $M$-compatible, then $<_L\upharpoonright C$ is too. But this is an ordering of $\mathrm{OR}^M\backslash\omega$ in ordertype $\omega$, which is impossible.

Now it seems one would like to generalize this to show that there is no such transitive $M$ at all. But we used some particular fine structural facts which don't easily (seem to) generalize. In particular, the use of the standard $\Sigma_n$ hierarchy becomes inconvenient when $n>1$. This is modified in fine structure theory, and replaced with a slightly different definability hierarchy. One also uses the $\mathcal{J}$-hierarchy $\mathcal{J}_\alpha$, and definability over $\mathcal{J}_\alpha$, instead of the $L$-hierarchy $L_\alpha$ (though I think the more crucial thing is the definability hierarchy). If one defines $<_L$ in a natural way using these things, also incorporating the fine structural standard parameters in a natural way, then there can be no such transitive $M$ for which $<_L\upharpoonright M$ is $M$-compatible.

Now it seems one would like to generalize this to show that there is no such transitive $M$ at all. But we used some particular fine structural facts which don't easily (seem to) generalize. In particular, the use of the standard $\Sigma_n$ hierarchy becomes inconvenient when $n>1$. This is modified in fine structure theory, and replaced with a slightly different definability hierarchy (e.g. $\mathrm{r}\Sigma_n$ instead of $\Sigma_n$). One also uses the $\mathcal{J}$-hierarchy $\mathcal{J}_\alpha$, and definability over $\mathcal{J}_\alpha$, instead of the $L$-hierarchy $L_\alpha$ (though I think the more crucial thing is the definability hierarchy). If one defines $<_L$ in a natural way using these things, also incorporating the fine structural standard parameters in a natural way, then there can be no such transitive $M$ for which $<_L\upharpoonright M$ is $M$-compatible.

Now $L_\alpha$ is pointwise definable, and this yields a surjection $\pi:\omega\to L_\alpha$ which is $\Sigma_1$-definable over $L_{\alpha+1}$ from the parameter $\alpha$. Therefore there is a Cohen generic over $L_\alpha$ in $L_{\alpha+2}$, and in fact one that is $\Sigma_1$-definable over $L_{\alpha+1}$ from the parameter set $\alpha$. This is optimal for such a Cohen generic: Because $L_\alpha\models\mathrm{ZFC}$, we have $c\notin L_{\alpha+1}$ and there is no $\Sigma_0$ definition of $c$ over $L_{\alpha+1}$ from parameters. It also implies that $L_\alpha\preceq_{\Sigma_1} L_{\alpha+1}$, and hence there is no $\Sigma_1$ definition of $c$ over $L_{\alpha+1}$ from any $s\in[\mathrm{OR}]^{<\omega}$ with $s<_{\mathrm{lex}}\{\alpha\}$.

Now $L_\alpha$ is pointwise definable, and this yields a surjection $\pi:\omega\to L_\alpha$ which is $\Sigma_1$-definable over $L_{\alpha+1}$ from the parameter $\alpha$. Therefore there is a Cohen generic over $L_\alpha$ in $L_{\alpha+2}$, and in fact one that is $\Sigma_1$-definable over $L_{\alpha+1}$ from the parameter $\alpha$. This is optimal for such a Cohen generic: Because $L_\alpha\models\mathrm{ZFC}$, we have $c\notin L_{\alpha+1}$ and there is no $\Sigma_0$ definition of $c$ over $L_{\alpha+1}$ from parameters. It also implies that $L_\alpha\preceq_{\Sigma_1} L_{\alpha+1}$, and hence there is no $\Sigma_1$ definition of $c$ over $L_{\alpha+1}$ from any $s\in[\mathrm{OR}]^{<\omega}$ with $s<_{\mathrm{lex}}\{\alpha\}$.