Solution (source code)

= Solution

Use the transitive-model convention for “standard” in this assertion: the domain is a <transitive set> and membership is actual membership. A <standard membership model of set theory> without transitivity is a weaker notion and would not justify the asserted absoluteness. Ordinalhood is bounded-formula absolute, so the internal <ordinals> are precisely $A\cap\operatorname{Ord}$. <Satisfaction for a set structure> is absolute between transitive <ZF> models containing that structure: the domain, finite parameter tuples, formula codes and the recursive truth clauses are the same. Equivalently one may use the $\Delta_1$ absoluteness of the predicate defining $L_\alpha$.

Transfinite induction now gives $L_\alpha^{\mathbb A}=L_\alpha$ for each <ordinal> $\alpha\in A$. At successors both computations use the same definable <subsets> of the same <set> structure; at limits they take the same union over all smaller <ordinals>, which belong to $A$ by transitivity. Thus
$$
\boxed{L^{\mathbb A}=\bigcup_{\alpha\in A\cap\operatorname{Ord}}L_\alpha.}
$$
For a set-sized model of <ordinal> height $\theta$, this is $L_\theta$. The restriction to actual <ordinals> makes the printed union precise. Mere well-foundedness of a nontransitive membership substructure would not justify these absoluteness steps; transitivity is the intended standard-model convention.