Absoluteness of constructible levels ($L_{\alpha }^M=L_{\alpha }$)

For a transitive model $M$ of ZFC and $\alpha \in M\cap \mathrm{Ord}$, the internally computed constructible hierarchy agrees with the ambient level: $L_{\alpha }^M=L_{\alpha }$. Satisfaction for a fixed set structure is computed from the same finite formulas and the same domain in both universes. Transfinite recursion then proves agreement at successors and limits. If $\theta =M\cap \mathrm{Ord}$, it follows that $L_{\theta }\subseteq M$.

If $M$ is a transitive model of ZF, its internally computed $L_{\alpha }$ is the actual $L_{\alpha }$ for each ordinal $\alpha \in M$. At a successor stage use absoluteness of satisfaction for the same set structure, formula codes and parameters; at a limit stage take the union of the already identical earlier stages. Choice is not required.