= Stage histories appear below every limit constructible level
{title2=$f_\xi\in L_\alpha(X)\quad(\xi<\alpha,\ \alpha\text{ a nonzero limit})$}
For a <transitive set> $X$, let $f_\xi$ be the history function $\eta\mapsto L_\eta(X)$ on $\xi+1$ in the <relative constructible hierarchy>. By <transfinite induction>, $f_\xi\in L_{\xi+k}(X)$ for some finite $k$, possibly depending on $\xi$. The base and successor steps follow by forming finite <ordered pairs> and adjoining the next entry, using $L_{\xi+1}(X)\in L_{\xi+2}(X)$. These operations require finitely many subsequent <definable power sets>.
At a nonzero <limit ordinal> $\lambda$, the inductive bounds put every earlier $f_\eta$ in $L_\lambda(X)$, since $\eta+k<\lambda$. This level satisfies <finite relation closure for set-theoretic coding>, independently of the availability of history functions. Consequently its <coded relative constructible stage> predicate computes the endpoints correctly. Finite pairing closure and the earlier histories show that
$$
h=\{\langle\eta,B\rangle\in L_\lambda(X):(L_\lambda(X),\in)\models S_X(\eta,B)\}
$$
contains exactly the pairs $\langle\eta,L_\eta(X)\rangle$ for $\eta<\lambda$. There are no extra indices: if $\eta\geq\lambda$ and $B=L_\eta(X)\in L_\lambda(X)$, increasing levels would give $B\in B$, contradicting <Axiom of foundation>. Thus $h=f_\lambda\!\upharpoonright\lambda$ is a definable <subset> of $L_\lambda(X)$ and belongs to $L_{\lambda+1}(X)$. Extracting its domain $\lambda$ and adjoining $\langle\lambda,L_\lambda(X)\rangle$ uses finitely many further operations, proving the induction step. Every nonzero limit $\alpha$ therefore contains all $f_\xi$ with $\xi<\alpha$, as required by <relative constructible level recognition>.
Back to article page
