Pointwise definable models of determinacy Suppose that the Axiom of Determinacy (AD) holds in $L(ℝ)$, and for some statement φ, $α$ is minimal such that $L_α(ℝ)⊨φ$.  Do definable (in $L_α(ℝ)$) elements of $L_α(ℝ)$ form an elementary substructure $L_α(ℝ)$?
Extension:  Assume ZF+AD (or if needed $\text{AD}^+$), and let $W_α$ consist of all sets of reals of Wadge rank $<α$.  Suppose that for some statement $φ$, $(α,β)$ is lexicographically minimal such that $L_β(W_α)⊨φ$.  Do definable (in $L_β(W_α)$) elements of $L_β(W_α)$ form an elementary substructure $L_β(W_α)$?
Notes:
* To handle $α=0$, we assume that all hereditarily finite sets are included.  The nonextended version holds for $α=0$ because of lightface projective uniformization.
* A positive answer would likely extend to existence of lightface definable scales (or if we added a real number $r$ that could be referenced by $φ$, to scales to definable from $r$).
* A weakening of AD that might suffice is determinacy for $L_{β+1}(W_α)$.
* Under large cardinal axioms, the extension extends far beyond $L(ℝ)$ — and beyond Wadge ranks and definability in the minimal inner model of $\text{AD}_ℝ$ + "$Θ$ is Mahlo" containing all the reals.
* The extension is reducible to the use of $W_α$ (with different $α$) in place of $L_β(W_α)$ if we can show that under the conditions, $L_{β+1}(W_α)$ has a set of real numbers that codes $L_β(W_α)$, and such that quantification over the corresponding $W_{α'}$ allows effective use of that set.
Motivation
The axiom of choice, while very natural and very useful, leads to 'paradoxical' sets that are apparently not definable.  To a mathematician objecting to such sets, we can try to reply that if you insist that all sets be definable, you will end up with a model of the axiom of choice.  And indeed, a theory extending ZF (without adding new predicates) has a pointwise definable model iff the theory is consistent with V=HOD.
However, ZF is not finitely axiomatizable.  And a positive answer to the question would imply that if we lower our requirement to a single statement (which can still have $Σ_{100}$ replacement), then canonical pointwise definable models abound.  Or if we insist on the full replacement schema (not in this question), we can (perhaps canonically) add infinitely many predicates $R_1,R_2,...$ to the language and replacement in the extended language, and still have pointwise definable models of ZF (or ZFC) with $R_{i+1}$ permitting definition of some sets not in $\text{HOD}_{R_1,...,R_i}$.
 A: The least ordinal $\kappa$ such that $L_\kappa(\mathbb R)$ satisfies KP is a counterexample. This essentially reduces to Theorem 1.3 of Tony Martin's "The Largest Countable This, That, and the Other." Of course, we are assuming some determinacy; $\text{AD}^{L(\mathbb R)}$ is more than enough, and Martin used the optimal hypothesis.
Here goes. Since KP is finitely axiomatizable, $L_\kappa(\mathbb R)$ is the least level of $L(\mathbb R)$ satisfying some sentence, as you have required. The sets that are (lightface) $\Sigma_1$-definable over $L_\kappa(\mathbb R)$ are precisely the inductive sets. There is a largest countable inductive set, which is just the set of reals $x$ such that for some $\alpha < \kappa$, $x$ is definable in $L_\alpha(\mathbb R)$. But Martin's theorem states that this set in fact contains every real definable in $L_\kappa(\mathbb R)$. (We are translating Martin's theorem from the notation of his paper, where the collection of reals definable in $L_\kappa(\mathbb R)$ is denoted by $\bigcup \Sigma^*_n$.) The complement $A$ of the largest countable inductive set is of course coinductive, or in other words $\Pi_1$-definable over $L_\kappa(\mathbb R)$. Yet $A$ contains no reals that are definable in $L_\kappa(\mathbb R)$: by Martin's theorem it is equal to the set of all reals that are not definable in $L_\kappa(\mathbb R)$. It follows that the definable elements of $L_\kappa(\mathbb R)$ do not form an elementary substructure of $L_\kappa(\mathbb R)$, since any elementary substructure of $L_\kappa(\mathbb R)$ would contain an element of the nonempty definable set $A$.
