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