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$.