What happens with large singular cardinals on the far side of the HOD dichotomy? Woodin's HOD Dichotomy Theorem says that if an extendible cardinal exists, then either $V$ and $HOD$ are rather close or rather far apart.  My question is whether the "far" case can be strengthened in analogy to Jensen's Covering Lemma to say something more about large singulars.  Suppose $\delta$ is extendible and every regular $\kappa \geq \delta$ is measurable in $HOD$.  Does there exist a singular $\lambda > \delta$ which is singular in $HOD$?
EDIT: The comment by Gabe Goldberg gives an easy "yes" answer.  Here's a harder version of the question.  Suppose $\delta$ is extendible and $\lambda$ is the least cardinal above $\delta$ such that $V_\lambda \models ZFC$.  Are all singular cardinals in the interval $(\delta,\lambda]$ singular in $HOD$?
 A: This is independent relative to the failure of the HOD hypothesis in the presence of large cardinals. 
We first give a positive answer under GCH. (Note that if it is consistent for the HOD Hypothesis to fail in the presence of an extendible, then this is consistent with GCH.) More generally, we show that under GCH, for any singular cardinal $\lambda$ that is regular in $\text{HOD}$, $V_\lambda\vDash \text{ZFC}$. Suppose towards a contradiction that $V_\lambda$ does not satisfy ZFC. Then there is a singularization of $\lambda$ definable over $V_\lambda$ from a parameter $a\in V_\lambda$. We may code $a$ by a set of ordinals $A\subseteq \alpha$ for some $\alpha < \lambda$. Thus $\lambda$ is singular in $\text{HOD}_A$. But $\text{HOD}_A$ is a generic extension of $\text{HOD}$ for a forcing of size less than $\lambda$ in $\text{HOD}$. (This bound falls out of Vopenka's theorem given GCH: recall that the Vopenka algebra is in bijection with the OD powerset of $P(\alpha)$.) One cannot destroy the $\text{HOD}$-inaccessible cardinal $\lambda$ by small forcing over $\text{HOD}$, so we have reached a contradiction.
On the other hand, the GCH assumption is necessary, which is proved easily by forcing. Start with a model $M$ of the failure of the HOD Hypothesis and an extendible cardinal $\delta$. Let $\lambda$ be the least singular cardinal of $M$ above $\delta$ that is regular in $\text{HOD}$. Force preserving cardinals, preserving the extendibility of $\delta$, and without increasing HOD to blow up $2^\delta$ above $\lambda$. This gives us a generic extension $N$. In $N$, the least $\lambda' > \delta$ such that $V_{\lambda'}$ is a model of ZFC is such that $\lambda' > 2^\delta > \lambda$. But $\lambda$ is still a singular of $N$ that is regular in $\text{HOD}$.
