Finite support for constructibility absoluteness

Expand the proof used in F1 into the fixed first-order formulas named in the Given. Its induction says simultaneously that, for every internal ordinal $\alpha$, the internally constructed history through $\alpha$ is the actual history and hence $(L_{\alpha }{)}^M=L_{\alpha }$. At a successor, finite satisfaction over the transitive set $L_{\beta }$ is absolute, so the two definable-subset operations agree. At a limit, transitivity gives exactly the actual earlier indices and union gives exactly their union. The proof uses only finitely many instances of Separation, Replacement and Foundation, together with finitely many of the remaining ZF axioms. By F2, let $K_0$ be the exact finite set of ZF axiom sentences occurring in this expanded derivation. Thus the comparison holds for every transitive $K_0$-model; no occurrence of the hypothesis "model of ZF" remains unexpanded.

Add to $K_0$ the finitely many axiom occurrences in the fixed proofs that Infinity supplies an internal nonzero limit ordinal, that the ordinals of a nonempty transitive set form an ordinal with no largest member, and that the fixed formula $x\in L$ is equivalent internally to membership in some level of its hierarchy. Call the resulting finite fragment $K_L$. If $M$ is a transitive $K_L$-model and ${\delta }_M=\mathrm{Ord}\cap M$, these fixed proofs make ${\delta }_M$ a nonzero limit ordinal and give $L^M={\bigcup }_{\alpha <{\delta }_M}(L_{\alpha }{)}^M$. By step 1.1 every summand is the actual $L_{\alpha }$. Each such level is an element of $M$, and transitivity puts all of its elements in $M$. Therefore $L^M=L_{{\delta }_M}\subseteq M$.

Suppose $M\subseteq N$ are transitive $K_L$-models with the same ordinals. Then ${\delta }_M={\delta }_N$, so step 2.1 gives $L^M=L_{{\delta }_M}=L_{{\delta }_N}=L^N\subseteq M$.

If $x\in N\setminus M$, step 3.1 gives $x\mathrm{\notin }{L}^N$. Since $x$ is an element of the universe of $N$ but is not internally constructible there, $N\models V\mathrm{\ne }L$. This last implication uses the fixed internal formula for $x\in L$ and does not compare $L^N$ with constructible levels above the common ordinal height.