text:
\section{Introduction}
An essential question regarding the theory of inner models is the
analysis of the class of all hereditarily ordinal definable sets
$\ensuremath{\operatorname{HOD}} $ inside various inner models $M$ of the set theoretic universe
$V$ under appropriate determinacy hypotheses. Examples for such inner
models $M$ are $L(\mathbb{R})$, $L[x]$, and the canonical proper class
$x$-mouse with $n$ Woodin cardinals $M_n(x)$, but nowadays also larger
models of determinacy $M$ are considered.

One motivation for analyzing the internal structure of these models
$\ensuremath{\operatorname{HOD}} ^M$ is given by Woodin's results in \cite{KW10} that under
determinacy hypotheses these models contain large cardinals. He showed
in \cite{KW10} for example that assuming $\Delta^1_2$ determinacy
there is a Turing cone of reals $x$ such that $\omega_2^{L[x]}$ is a
Woodin cardinal in the model $\ensuremath{\operatorname{HOD}} ^{L[x]}$. This result generalizes to
higher levels in the projective hierarchy. That means for $n \geq 1$
assuming $\boldsymbol\Pi^1_{n+1}$ determinacy and $\Pi^1_{n+2}$ determinacy there
is a cone of reals $x$ such that $\omega_2^{M_{n}(x)}$ is a Woodin
cardinal in the model $\ensuremath{\operatorname{HOD}} ^{M_{n}(x) | \delta_x}$, where $M_{n}(x)$
denotes the canonical proper class $x$-mouse with $n$ Woodin cardinals
and $\delta_x$ is the least Woodin cardinal in $M_{n}(x)$. Moreover,
Woodin showed a similar result for $\ensuremath{\operatorname{HOD}} ^{L(\mathbb{R})}$. If we let
$\Theta$ denote the supremum of all ordinals $\alpha$ such that there
exists a surjection $\pi: \mathbb{R} \rightarrow \alpha$, then
assuming $\ensuremath{\operatorname{ZF}}  + \ensuremath{\operatorname{AD}} $, he showed that $\Theta^{L(\mathbb{R})}$ is a
Woodin cardinal in $\ensuremath{\operatorname{HOD}} ^{L(\mathbb{R})}$ (see \cite{KW10}). The fact
that these models of the form $\ensuremath{\operatorname{HOD}} ^M$ can have large cardinals as for
example Woodin cardinals motivates the question if they are in some
sense fine structural as for example the models $L[x], M_n(x)$, and
$L(\mathbb{R})$ are. A good test question for this is whether these
models $\ensuremath{\operatorname{HOD}} ^M$ satisfy the generalized continuum hypothesis
$\ensuremath{\operatorname{GCH}} $. If it turns out that $\ensuremath{\operatorname{HOD}} ^M$ is in fact a fine structural
model, it would follow that it satisfies the $\ensuremath{\operatorname{GCH}} $ and even stronger
combinatorial principles as for example the $\Diamond$ principle.

The first model which was analyzed in this sense was
$\ensuremath{\operatorname{HOD}} ^{L(\mathbb{R})}$ under the assumption that every set of reals in
$L(\mathbb{R})$ is determined (short: $\ensuremath{\operatorname{AD}} ^{L(\mathbb{R})}$). Using
purely descriptive set theoretic methods Becker showed in \cite{Be80}
under this hypothesis that $\ensuremath{\operatorname{GCH}} _\alpha$, i.e. $2^\alpha = \alpha^+$,
holds in $\ensuremath{\operatorname{HOD}} ^{L(\mathbb{R})}$ for all
$\alpha < \omega_1^{L(\mathbb{R})}$. Later J. R. Steel and
W. H. Woodin were able to push the analysis of $\ensuremath{\operatorname{HOD}} ^{L(\mathbb{R})}$
forward using more recent advances in inner model theory. In 1993 they
first showed independently that the reals in $\ensuremath{\operatorname{HOD}} ^{L(\mathbb{R})}$
are the same as the reals in $M_\omega$, the least proper class
iterable premouse with $\omega$ Woodin cardinals. Then they showed in
§$4$ of \cite{St93} that $\ensuremath{\operatorname{HOD}} ^{L(\mathbb{R})}$ in fact agrees with
the inner model $N$ up to $\mathcal{P}(\omega_1^{L(\mathbb{R})})$, where $N$
denotes the $\omega_1^{L(\mathbb{R})}$-th linear iterate of $M_\omega$
by its least measure and its images. Building on this, John R. Steel
was able to show in \cite{St95} that $\ensuremath{\operatorname{HOD}} ^{L(\mathbb{R})}$ agrees
with the inner model $\mathcal{M}_\infty$ up to
$(\boldsymbol\delta_1^2)^{L(\mathbb{R})}$, where $\mathcal{M}_\infty$ is a
direct limit of iterates of $M_\omega$ and
$(\boldsymbol\delta_1^2)^{L(\mathbb{R})}$ is the supremum of all
ordinals $\alpha$ such that there exists a surjection
$\pi: \mathbb{R} \rightarrow \alpha$ which is
$\boldsymbol\Delta_1^{L(\mathbb{R})}$ definable. Finally, in 1996 W. Hugh Woodin
extended this (see \cite{StW16}) and showed that in fact
$\ensuremath{\operatorname{HOD}} ^{L(\mathbb{R})} = L[\mathcal{M}_\infty, \Lambda]$, where $\Lambda$ is a
partial iteration strategy for $\mathcal{M}_\infty$. For even larger models of
determinacy $M$ the corresponding model $\ensuremath{\operatorname{HOD}} ^M$ was first analyzed in
\cite{Sa09}, where the second author showed that it is fine structural
using a layered hierarchy. Models of this form are nowadays called
\emph{hod mice}. A different approach for the fine structure of hod
mice called the least branch hierarchy is studied in \cite{St16}.

The question if $\ensuremath{\operatorname{HOD}} ^{L[x]}$ is a model of $\ensuremath{\operatorname{GCH}} $ or even a fine structural model for a Turing cone of reals $x$ under a suitable determinacy hypothesis remains open until today. What has been done is the analysis of the model $\ensuremath{\operatorname{HOD}} ^{L[x][G]}$, where $G$ is $\ensuremath{\operatorname{Col}} (\omega, {<}\kappa_x)$-generic over $\ensuremath{\operatorname{HOD}} ^{L[x]}$ for the least inaccessible cardinal $\kappa_x$ in $L[x]$. Woodin showed in the $1990$'s (see \cite{StW16}) that assuming $\Delta^1_2$ determinacy there is a Turing cone of reals $x$ such that $\ensuremath{\operatorname{HOD}} ^{L[x][G]} = L[\mathcal{M}_\infty, \Lambda]$, where $\mathcal{M}_\infty$ is a direct limit of mice (which are iterates of $M_1$) and $\Lambda$ is a partial iteration strategy for $\mathcal{M}_\infty$.

In this article, we analyze $\ensuremath{\operatorname{HOD}} $ in the model $M_n(x)[g]$ for any real $x$ of sufficiently high Turing degree under the assumption that every $\boldsymbol\Pi^1_{n+2}$ set of reals is determined. Here $g$ is $\ensuremath{\operatorname{Col}} (\omega, {<}\kappa)$-generic over $M_n(x)$, where $\kappa$ denotes the least inaccessible cardinal in $M_n(x)$. We first show that the direct limit model $\cM_{\infty}$, obtained from iterates of suitable premice, agrees up to its bottom Woodin cardinal $\delta_{\infty}$ with $\ensuremath{\operatorname{HOD}} ^{M_n(x)[g]}$. In a second step, we show that the full model $\ensuremath{\operatorname{HOD}} ^{M_n(x)[g]}$ is in fact of the form $M_n(\hat{\cM}_{\infty} | \kappa_\infty, \Lambda)$, where $\hat{\cM}_{\infty} = M_n(\cM_{\infty} | \delta_{\infty})$, $\kappa_\infty$ is the least inaccessible cardinal of $\hat{\cM}_{\infty}$ above $\delta_{\infty}$, and $\Lambda$ is a partial iteration strategy for $\cM_{\infty}$. Here and below $M_n(\hat{\cM}_{\infty}|\kappa_{\infty}, \Lambda)$ denotes the canonical fine structural model with $n$ Woodin cardinals build over the coarse objects $\hat{\cM}_{\infty}|\kappa_{\infty}$ and $\Lambda$. Our proof in fact shows that $\ensuremath{\operatorname{HOD}} ^{M_n(x)[g]}$ is a model of $\ensuremath{\operatorname{GCH}} $, $\Diamond$, and other combinatorial principles which are consequences of fine structure.

In the statement of the following main theorem and in fact everywhere
in this article whenever we write $\ensuremath{\operatorname{HOD}} ^M$ for some premouse $M$ we
mean $\ensuremath{\operatorname{HOD}} ^{\lfloor M \rfloor}$, where $\lfloor M \rfloor$ denotes the
universe of the model $M$. In particular, we do not allow the extender
sequence of $M$ as a parameter in the definition of $\ensuremath{\operatorname{HOD}} $. It will be clear from the context if
we consider the model $M$ or the universe $\lfloor M \rfloor$ of $M$,
therefore we decided for the sake of readability to not distinguish
the notation for these two objects.

The main result of this paper is the following theorem.

\begin{thm}\label{thm:main}
  Let $n < \omega$ and assume
  $\boldsymbol\Pi^1_{n+2}$-determinacy. Then for a Turing cone of
  reals $x$,
  \[ \ensuremath{\operatorname{HOD}} ^{M_n(x)[g]} = M_n(\hat{\cM}_{\infty}|\kappa_{\infty}, \Lambda), \] where $g$ is
  $\ensuremath{\operatorname{Col}} (\omega, {<}\kappa)$-generic over $M_n(x)$, $\kappa$ denotes
  the least inaccessible cardinal in $M_n(x)$,
  $\hat{\cM}_{\infty}$ is a direct limit of iterates of
  $M_{n+1}$, $\delta_{\infty}$ is the least Woodin
  cardinal in $\hat{\cM}_{\infty}$, $\kappa_{\infty}$ is the least inaccessible cardinal of $\hat{\cM}_{\infty}$ above $\delta_{\infty}$, and $\Lambda$ is a partial iteration strategy
  for $\cM_{\infty}$.
\end{thm}

Our proof in fact shows the following corollary.

\begin{cor}\label{cor:main}
  Assume $\boldsymbol\Pi^1_{n+2}$-determinacy. Then for a Turing cone
  of reals $x$, \[\ensuremath{\operatorname{HOD}^{M_n(x)[g]}}  \vDash \ensuremath{\operatorname{GCH}} ,\] where $g$ is
  $\ensuremath{\operatorname{Col}} (\omega, {<}\kappa)$-generic over $M_n(x)$ and $\kappa$ denotes
  the least inaccessible cardinal in $M_n(x)$.
\end{cor}

\begin{remark}
  In fact the full strength of $\boldsymbol\Pi^1_{n+2}$-determinacy is not needed
  for these results. It suffices to assume that $M_n^\#(x)$ exists and
  is $\omega_1$-iterable for all reals $x$ (or equivalently
  $\boldsymbol\Pi^1_{n+1}$-determinacy, see \cite{MSW} and \cite{Ne02}) and that
  $M_{n+1}^\#$ exists and is $\omega_1$-iterable. This is all we will
  use in the proof.
\end{remark}

Finally, we summarize some open questions related to these results. The following question already appears in \cite{StW16}.

\begin{question}
  Assume $\boldsymbol\Delta^1_2$ determinacy. Is $\ensuremath{\operatorname{HOD}} ^{L[x]}$ for a cone of reals
  $x$ a fine structural model?
\end{question}

\begin{question}
  Assume $\boldsymbol\Pi^1_{n+2}$ determinacy. Is $\ensuremath{\operatorname{HOD}} ^{M_n(x)}$ for a cone of
  reals $x$ a fine structural model?
\end{question}

This article is structured as follows. In Section \ref{sec:prelim} we
recall some preliminaries and fix the basic notation. In Section
\ref{sec:dlm} we recall the relevant notions from \cite{Sa13} and
define the direct limit system converging to $\cM_{\infty}$, before we compute
$\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $ up to its Woodin cardinal in Section \ref{sec:dmr}. In
Section \ref{sec:fullHOD} we then show how this can be used to compute
the full model $\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $, i.e., we finish the proof of Theorem
\ref{thm:main}. The authors thank Farmer Schlutzenberg for the helpful
discussions during the 4th Münster conference on inner model theory
in the summer of 2017. Finally, the authors thank the referee for
carefully reading the paper and making several helpful comments and
suggestions.

\section{Preliminaries and notation}\label{sec:prelim}

Whenever we say \emph{reals} we mean elements of the Baire space
${}^\omega\omega$. We also write $\mathbb{R}$ for ${}^\omega\omega$. $\ensuremath{\operatorname{HOD}} $ denotes the class of all
hereditarily ordinal definable sets. Moreover $\ensuremath{\operatorname{HOD}} _x$ for any
$x \in {}^\omega\omega$ denotes the class of all sets which are hereditarily
ordinal definable over $\{x\}$.\footnote{In the literature this is
  sometimes also called $\ensuremath{\operatorname{HOD}} _{\{x\}}$.} That means we let
$A \in \ensuremath{\operatorname{OD}} _x$ iff there is a formula $\varphi$ such that
$A = \{ v \mid \varphi(v,\alpha_1, \dots, \alpha_n,x) \}$ for some
ordinals $\alpha_1, \dots, \alpha_n$. Then $A \in \ensuremath{\operatorname{HOD}} _x$ iff
$\ensuremath{\operatorname{TC}} (\{A\}) \subset \ensuremath{\operatorname{OD}} _x$, where $\ensuremath{\operatorname{TC}} (\{A\})$ denotes the transitive
closure of the set $\{A\}$.

We use the notions of premice and iterability from \cite[§$1-4$]{St10}
and assume that the reader is familiar with the basic concepts defined
there. In most cases we will demand $(\omega,\omega_1,\omega_1)$-iterability in the sense of Definition $4.4$ in \cite{St10} for our mice, but in other cases or if it is not clear from the context we will state the precise amount of iterability. We say a
\emph{cutpoint} of a premouse $\mathcal{M}$ is an infinite ordinal $\gamma$
such that there is no extender $E$ on the $\mathcal{M}$-sequence with
$\ensuremath{\operatorname{crit}} (E) \leq \gamma \leq \ensuremath{\operatorname{lh}} (E)$.\footnote{Such a cutpoint $\gamma$
  is often also called a strong cutpoint.}

For some $\ensuremath{\operatorname{ZFC}} $ model $M$ and some real
$x \in M$ we write $L[E](x)^M$ for the result of a fully
backgrounded extender construction above $x$ inside $M$ in the sense
of \cite{MS94}, with the minimality condition relaxed to $\omega$-small premice. Moreover, we let for a premouse $\mathcal{M}$ with $\mathcal{M} \vDash \ensuremath{\operatorname{ZFC}} $, a cardinal cutpoint $\eta$ of $\mathcal{M}$, and a premouse $\mathcal{N}$ of height $\eta$ such that $\mathcal{N} \in \mathcal{P}(\mathcal{M} | \eta) \cap \mathcal{M} | (\eta + \omega)$, $\mathcal{P}^\mathcal{M}(\mathcal{N})$ denote the
result of a $\mathcal{P}$-construction over $\mathcal{N}$ inside the model $\mathcal{M}$ in
the sense of \cite{SchSt09} or \cite[Proposition 2.3 and Definition
2.4]{Sa13}.

For $x \in {}^\omega\omega$ and $n \leq \omega$ we let $M_n^\#(x)$, if it exists,
denote a countable, sound, $\omega_1$-iterable $x$-premouse which is
not $n$-small but all of whose proper initial segments are
$n$-small. In fact, $\omega_1$-iterability suffices to show that such
an $M_n^\#(x)$ is unique. If $M_n^\#(x)$ exists, we let $M_n(x)$ be
the proper class premouse obtained by iterating the top extender of
$M_n^\#(x)$ out of the universe.

\section{The direct limit system}\label{sec:dlm}

To show that $\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $ is a fine structural inner model, we will use an
extension of the direct limit system introduced in \cite{Sa13}. For
the reader's convenience we will first recall the relevant definitions
and results from \cite{Sa13}, obtaining a direct limit system which is
definable in $M_n(x)$. We use the chance to correct some minor errors
in the presentation of that direct limit system in \cite{Sa13}. Then
we discuss the changes we need to make to obtain a direct limit system
definable in $M_n(x)[g]$. Another application of a similar but slightly
different direct limit system as in \cite{Sa13} can be found in
\cite{SaSch18}.

Fix an arbitrary natural number $n$. Throughout the rest of this article we will assume that $M_{n+1}^\#$ exists and is $(\omega,\omega_1,\omega_1)$-iterable and fix a real $x$ that codes $M_{n+1}^\#$. This implies $\boldsymbol\Pi^1_{n+1}$ determinacy or equivalently that
$M_{n}^\#(z)$ exists and is $(\omega, \omega_1, \omega_1)$-iterable for all reals $z$ (see
\cite{Ne95} and \cite{MSW} for a proof of this equivalence due to Itay
Neeman and W. Hugh Woodin). Finally, we fix a $\ensuremath{\operatorname{Col}} (\omega, {<}\kappa)$-generic $g$ over $M_n(x)$, where $\kappa$ is the least inaccessible cardinal in $M_n(x)$.

\subsection*{The first direct limit system}

We first recall the definition of a lower part premouse.

\begin{definition}
  Let $a$ be a countable, transitive, self-wellordered\footnote{We say
  a transitive set $a$ is \emph{self-wellordered} iff $a$ is
  wellordered in $L_{\omega}[a]$.} set. Then we
define the lower part model $Lp^n(a)$ as the model theoretic union of all countable
$a$-premice $M$ with $\rho_\omega(M) = a$ which are $n$-small, sound,
and $(\omega, \omega_1, \omega_1)$-iterable.
\end{definition}

If $\mathcal{N}$ is a countable premouse, we also use $Lp^n(\mathcal{N})$ to denote
the premouse extending $\mathcal{N}$ which is defined similarly as the model
theoretic union of premice $M \unrhd \mathcal{N}$ with $\rho_\omega(M) \leq \mathcal{N} \cap \ensuremath{\operatorname{Ord}} $ which have $\mathcal{N} \cap \ensuremath{\operatorname{Ord}} $ as a cutpoint, are $n$-small above $\mathcal{N} \cap \ensuremath{\operatorname{Ord}} $, sound above $\mathcal{N} \cap \ensuremath{\operatorname{Ord}} $, and $(\omega, \omega_1, \omega_1)$-iterable above $\mathcal{N} \cap \ensuremath{\operatorname{Ord}} $.

\begin{definition} \label{def:nsuit} A countable premouse $\mathcal{N}$ is
  \emph{$n$-suitable}\comm{Usually my notation for this is
    $(n+1)$-suitable, so be careful} iff there is an ordinal $\delta$
  such that
 \begin{enumerate}
 \item $\mathcal{N} \vDash \text{``}\ensuremath{\operatorname{ZFC}}  - \text{Replacement''}$ and
   $ \mathcal{N} \cap \ensuremath{\operatorname{Ord}}  = \sup_{i<\omega} (\delta^{+i})^\mathcal{N}$,
 \item $\mathcal{N} \vDash \text{``} \delta \text{ is a Woodin cardinal''}$,
 \item $\mathcal{N}$ is $(n+1)$-small,
 \item for every cutpoint $\gamma < \delta$ of $\mathcal{N}$, $\gamma$ is not
   Woodin in $Lp^n(\mathcal{N}|\gamma)$,
 \item $\mathcal{N} | (\delta^{+(i+1)})^\mathcal{N} = Lp^n(\mathcal{N} | (\delta^{+i})^\mathcal{N})$ for all $i<\omega$, and
 \item for all $\eta < \delta$, $\mathcal{N} \vDash \text{``} \mathcal{N} | \delta \text{ is } (\omega,\eta,\eta)\text{-iterable''}$.
 \end{enumerate}
\end{definition}

If $\mathcal{N}$ is an $n$-suitable premouse we denote the ordinal
$\delta$ from Definition \ref{def:nsuit} by
$\delta^\mathcal{N}$. Moreover, we write $\hat\mathcal{N} = M_n(\mathcal{N}|\delta^{\mathcal{N}})$ for any $n$-suitable premouse $\mathcal{N}$. Then $\mathcal{N} = \hat\mathcal{N} | ((\delta^\mathcal{N})^{+\omega})^{\hat\mathcal{N}}$ for every $n$-suitable premouse $\mathcal{N}$ by well-known properties of the lower part model $Lp^n$. We now give some definitions indicating how $n$-suitable premice can be iterated.

\begin{definition}
  Let $\mathcal{N}$ be an arbitrary premouse and let $\mathcal{T}$ be an iteration tree
  on $\mathcal{N}$ of limit length.
  \begin{enumerate}[(1)]
  \item We say a premouse $\mathcal{Q} = \mathcal{Q}(\mathcal{T})$ is a \emph{$\mathcal{Q}$-structure for
      $\mathcal{T}$} iff $\mathcal{M}(\mathcal{T}) \unlhd \mathcal{Q}$, $\mathcal{Q}$ is sound, $\delta(\mathcal{T})$ is a cutpoint of
    $\mathcal{Q}$, $\mathcal{Q}$ is $(\omega, \omega_1, \omega_1)$-iterable above $\delta(\mathcal{T})$, and if $\mathcal{Q} \neq \mathcal{M}(\mathcal{T})$
    \[ \mathcal{Q} \vDash \text{``} \delta(\mathcal{T}) \text{ is a Woodin
      cardinal''}, \] and
    \begin{enumerate}[$(i)$]
    \item over $\mathcal{Q}$ there exists an $r\Sigma_n$-definable set
      $A \subset \delta(\mathcal{T})$ such that there is no
      $\kappa < \delta(\mathcal{T})$ such that $\kappa$ is strong up to
      $\delta(\mathcal{T})$ with respect to $A$ as being witnessed by extenders
      on the sequence of $\mathcal{Q}$ for some $n < \omega$, or
  \item  $\rho_n(\mathcal{Q}) < \delta(\mathcal{T})$ for some $n<\omega$.
    \end{enumerate}
  \item Let $b$ be a cofinal well-founded branch through $\mathcal{T}$. Then we
    say a premouse $\mathcal{Q} = \mathcal{Q}(b, \mathcal{T})$ is a \emph{$\mathcal{Q}$-structure for $b$
      in $\mathcal{T}$} iff $\mathcal{Q}$ is sound and
    $\mathcal{Q} = \mathcal{M}_b^\mathcal{T} | \gamma$, where $\gamma \leq \mathcal{M}_b^\mathcal{T} \cap \ensuremath{\operatorname{Ord}} $ is
    the least ordinal such that either
    \[ \gamma < \mathcal{M}_b^\mathcal{T} \cap \ensuremath{\operatorname{Ord}}  \text{ and } \mathcal{M}_b^\mathcal{T} | (\gamma+1)
    \vDash \text{``}\delta(\mathcal{T}) \text{ is not Woodin'',} \] or
    \[ \gamma = \mathcal{M}_b^\mathcal{T} \cap \ensuremath{\operatorname{Ord}}  \text{ and }
    \rho_n(\mathcal{M}_b^\mathcal{T}) < \delta(\mathcal{T}) \]
    for some $n<\omega$ or over $\mathcal{M}_b^\mathcal{T}$ there exists an
    $r\Sigma_n$-definable set $A \subset \delta(\mathcal{T})$ such that there
    is no $\kappa < \delta(\mathcal{T})$ such that $\kappa$ is strong up to
    $\delta(\mathcal{T})$ with respect to $A$ as being witnessed by extenders
    on the sequence of $\mathcal{M}_b^\mathcal{T}$ for some $n < \omega$.\\
    If no such ordinal $\gamma \leq \mathcal{M}_b^\mathcal{T} \cap \ensuremath{\operatorname{Ord}} $ exists, we let
    $\mathcal{Q}(b,\mathcal{T})$ be undefined.
    \end{enumerate}
  \end{definition}

  \begin{remark}
  If it exists, $M_{n+1}|(\delta_0^{+\omega})^{M_{n+1}}$ is
  $n$-suitable, where $\delta_0$ is the least Woodin cardinal in
  $M_{n+1}$. We denote this premouse by $M_{n+1}^-$ and write
  $\Sigma_{M_{n+1}^-}$ for its iteration strategy induced by
  the canonical $\mathcal{Q}$-structure guided iteration strategy $\Sigma_{M_{n+1}}$ for $M_{n+1}$ for countable stacks of normal trees without drops on the main branches.
\end{remark}

Our goal is to approximate the iteration strategy
$\Sigma_{M_{n+1}^-}$ inside $\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $. Analogous to \cite[Definition 5.32]{SchlTr} we define the following requirement, which will be used in Definition \ref{def:sti} to make
the proof of Lemmas \ref{lem:pseudocomp} and \ref{lem:pseudogenit} work.

\begin{definition}
  Let $\mathcal{N}$ be an $n$-suitable premouse and let $\mathcal{T}$ be a normal
  iteration tree on $\mathcal{N}$ of length $< \omega_1^V$. Then we say that
  $\mathcal{T}$ is \emph{suitability strict} iff for all $\alpha < \ensuremath{\operatorname{lh}} (\mathcal{T})$,
  \begin{enumerate}[$(i)$]
  \item if $[0, \alpha]_T$ does not drop then $\mathcal{M}_\alpha^\mathcal{T}$ is
    $n$-suitable, and
  \item if $[0, \alpha]_T$ drops then no $\mathcal{R} \unlhd \mathcal{M}_\alpha^\mathcal{T}$
    is $n$-suitable.
  \end{enumerate}
\end{definition}

\begin{definition}
  \label{def:short} Let $\mathcal{N}$ be an $n$-suitable premouse and let
  $\mathcal{T}$ be a normal iteration tree on $\mathcal{N}$ of length $< \omega_1^V$.
  \begin{enumerate}
  \item $\mathcal{T}$ is \emph{correctly guided} iff for every limit ordinal
    $\lambda < \ensuremath{\operatorname{lh}} (\mathcal{T})$, if $b$ is the branch choosen for
    $\mathcal{T} \upharpoonright \lambda$ in $\mathcal{T}$, then
    $\mathcal{Q}(b, \mathcal{T} \upharpoonright \lambda)$ exists and
    $\mathcal{Q}(b, \mathcal{T} \upharpoonright \lambda) \unlhd M_n(\mathcal{M}(\mathcal{T}
    \upharpoonright \lambda))$.
  \item $\mathcal{T}$ is \emph{short} iff $\mathcal{T}$ is correctly guided and in
    case $\mathcal{T}$ has limit length $\mathcal{Q}(\mathcal{T})$ exists and $\mathcal{Q}(\mathcal{T}) \unlhd
    M_n(\mathcal{M}(\mathcal{T}))$.
  \item $\mathcal{T}$ is \emph{maximal} iff $\mathcal{T}$ is correctly guided and not
    short.
  \end{enumerate}
\end{definition}

\begin{definition}\label{def:sti}
  Let $\mathcal{N}$ be an $n$-suitable premouse. We say $\mathcal{N}$ is \emph{short
    tree iterable} \index{short tree iterable} iff whenever $\mathcal{T}$ is a
  short tree on $\mathcal{N}$,
  \begin{enumerate}[$(i)$]
  \item $\mathcal{T}$ is suitability strict,
  \item if $\mathcal{T}$ has a last model, then every putative\footnote{An
      iteration tree $\mathcal{U}$ is a \emph{putative iteration tree} if
      $\mathcal{U}$ satisfies all properties of an iteration tree, but in case
      $\mathcal{U}$ has a last model we allow this last model to be
      ill-founded.} iteration tree $\mathcal{U}$ extending $\mathcal{T}$ such that
    $\ensuremath{\operatorname{lh}} (\mathcal{U}) = \ensuremath{\operatorname{lh}} (\mathcal{T}) +1$ has a well-founded last model, and
  \item if $\mathcal{T}$ has limit length, then there exists a cofinal
    well-founded branch $b$ through $\mathcal{T}$ such that
    $\mathcal{Q}(b,\mathcal{T}) = \mathcal{Q}(\mathcal{T})$.
  \end{enumerate}
\end{definition}

This can be generalized to stacks of correctly guided normal trees.

\begin{definition}\label{def:fincorrectlyguidedstack}
  Let $\mathcal{N}$ be an $n$-suitable premouse and $m < \omega$. Then we say
  $(\mathcal{T}_i, \mathcal{N}_i \mid i \leq m)$ is a \emph{correctly guided finite
    stack} on $\mathcal{N}$ iff
  \begin{enumerate}[$(i)$]
  \item $\mathcal{N}_0 = \mathcal{N}$,
  \item $\mathcal{N}_i$ is $n$-suitable and $\mathcal{T}_i$ is a correctly guided
    normal iteration tree on $\mathcal{N}_i$ which acts below $\delta^{\mathcal{N}_i}$
    for all $i \leq m$,
  \item for every $i<m$ either $\mathcal{T}_i$ has a last model which is equal
    to $\mathcal{N}_{i+1}$ and the iteration embedding
    $i^{\mathcal{T}_i}: \mathcal{N}_i \rightarrow \mathcal{N}_{i+1}$ exists or $\mathcal{T}_i$ is
    maximal and
    $\mathcal{N}_{i+1} = M_n(\mathcal{M}(\mathcal{T}_i)) |
    (\delta(\mathcal{T}_i)^{+\omega})^{M_n(\mathcal{M}(\mathcal{T}_i))}$.
  \end{enumerate}
  Moreover, we say that $\mathcal{M}$ is the last model of
  $(\mathcal{T}_i, \mathcal{N}_i \mid i \leq m)$ iff either
  \begin{enumerate}[$(i)$]
  \item $\mathcal{T}_m$ has a last model which is equal to $\mathcal{M}$ and the
    iteration embedding $i^{\mathcal{T}_m}: \mathcal{N}_m \rightarrow \mathcal{M}$ exists,
  \item $\mathcal{T}_m$ is of limit length and short and there is a
    non-dropping cofinal well-founded branch $b$ through $\mathcal{T}_m$ such
    that $\mathcal{Q}(b,\mathcal{T})$ exists, $\mathcal{T}_m{}^\smallfrown b$ is correctly
    guided, and $\mathcal{M} = \mathcal{M}_b^{\mathcal{T}}$, or
  \item $\mathcal{T}_m$ is maximal and
    $\mathcal{M} = M_n(\mathcal{M}(\mathcal{T}_m)) |
    (\delta(\mathcal{T}_m)^{+\omega})^{M_n(\mathcal{M}(\mathcal{T}_m))}$.
  \end{enumerate}
  Finally, we say that $\mathcal{M}$ is a \emph{correct iterate} of $\mathcal{N}$ iff
  there is a correctly guided finite stack on $\mathcal{N}$ with last model
  $\mathcal{M}$. In case there is a correctly guided finite stack on $\mathcal{N}$
  with last model $\mathcal{M}$ of length $1$, i.e., such that $m=0$, we say
  that $\mathcal{M}$ is a \emph{pseudo-normal iterate} (or just
  \emph{pseudo-iterate}) of $\mathcal{N}$.
\end{definition}

Analogous to Theorem $3.14$ in \cite{StW16} we also have a version of
the comparison lemma for short tree iterable premice and pseudo-normal
iterates.

\begin{lemma}[Pseudo-comparison lemma]\label{lem:pseudocomp}
  Let $\mathcal{N}$ and $\mathcal{M}$ be $n$-suitable premice which are short tree
  iterable. Then there is a common pseudo-normal iterate
  $\mathcal{R} \in M_n(y)$ such that
  $\delta^\mathcal{R} \leq \omega_1^{M_n(y)}$, where
  $y$ is a real coding $\mathcal{N}$ and $\mathcal{M}$.
\end{lemma}

The proof of Lemma \ref{lem:pseudocomp} is similar to the proof of
Theorem $3.14$ in \cite{StW16}, so we omit it. Similarly, we have an
analogue to the pseudo-genericity iteration (see Theorem $3.16$ in
\cite{StW16}).

\begin{lemma}[Pseudo-genericity iterations]\label{lem:pseudogenit}
  Let $\mathcal{N}$ be an $n$-suitable premouse which is short tree iterable
  and let $z$ be a real. Then there is a pseudo-normal iterate $\mathcal{R}$
  of $\mathcal{N}$ in $M_n(y,z)$ such that $z$ is $\mathbb{B}^\mathcal{R}$-generic
  over $\mathcal{R}$ and $\delta^\mathcal{R} \leq \omega_1^{M_n(y,z)}$, where
  $y$ is a real coding $\mathcal{N}$ and $\mathbb{B}^\mathcal{R}$ denotes Woodin's
  extender algebra inside $\mathcal{R}$.
\end{lemma}

For the definition of the direct limit system converging to $\ensuremath{\operatorname{HOD}} $ we
need the notion of $s$-iterability. To define this, we first introduce
some notation.
For an $n$-suitable premouse $\mathcal{N}$, a finite sequence of ordinals $s$,
and some $k < \omega$ let
\begin{align*}
  T_{s,k}^\mathcal{N} = \{ (t, \ulcorner \phi \urcorner) \in
  [((\delta^\mathcal{N})^{+k})^\mathcal{N}]^{<\omega} & \times \omega \mid \phi \text{ is
                                        a } \Sigma_1\text{-formula and
                                        }\\ & M_n(\mathcal{N} | \delta^\mathcal{N})
                                              \vDash \phi[t,s] \},
\end{align*}
where $\ulcorner \phi \urcorner$ denotes the G\"odel number of
$\phi$. Let $Hull_1^\mathcal{N}$ denote an uncollapsed $\Sigma_1$ hull in
$\mathcal{N}$. Then we let
\[ \gamma_s^\mathcal{N} = \sup(Hull_1^\mathcal{N}(\{ T_{s,k}^\mathcal{N} \mid k < \omega \}) \cap
  \delta^\mathcal{N})\] and
\[ H_s^\mathcal{N} = Hull_1^\mathcal{N}( \gamma_s^\mathcal{N} \cup \{ T_{s,k}^\mathcal{N} \mid k <
  \omega \}). \] Then $\gamma_s^\mathcal{N} = H_s^\mathcal{N} \cap \delta^\mathcal{N}$. For
$s_m = (u_1, \dots, u_{m})$ the sequence of the first $m$ uniform
indiscernibles, we write $\gamma_m^\mathcal{N} = \gamma_{s_m}^\mathcal{N}$ and
$H_m^\mathcal{N} = H_{s_m}^\mathcal{N}$. Then we have that
$\sup_{m \in \omega} \gamma_m^\mathcal{N} = \delta^\mathcal{N}$ (see Lemma 5.3 in
\cite{Sa13}).

\begin{definition}\label{def:siterable}
  Let $\mathcal{N}$ be an $n$-suitable premouse and $s$ a finite sequence of
  ordinals. Then $\mathcal{N}$ is \emph{$s$-iterable} iff every correct iterate of $\mathcal{N}$ is short tree
  iterable and for every correctly guided finite stack
  $(\mathcal{T}_i, \mathcal{N}_i \mid i \leq m)$ on $\mathcal{N}$ with last model $\mathcal{M}$ there
  is a sequence of non-dropping branches $(b_i \mid i \leq m)$ and a sequence of
  embeddings $(\pi_i \mid i \leq m)$ such that
  \begin{enumerate}[$(i)$]
  \item if $\mathcal{T}_i$ has successor length $\alpha +1$, then
    $b_i = [0,\alpha]_{T_i}$ and $\pi_i = i_{0,\alpha}^{\mathcal{T}_i}$ is the corresponding
    iteration embedding for $i \leq m$,
  \item if $\mathcal{T}_m$ is short, then $b_m$ is the unique cofinal
    well-founded branch through $\mathcal{T}_m$ such that $\mathcal{Q}(b_m,\mathcal{T}_m)$
    exists and $\mathcal{T}_m{}^\smallfrown b_m$ is correctly guided and
    $\pi_m = i^{\mathcal{T}_m}_{b_m}$ is the corresponding iteration
    embedding,
  \item if $\mathcal{T}_i$ is maximal, then $b_i$ is a cofinal well-founded
    branch through $\mathcal{T}_i$ such that $\mathcal{M}_{b_i}^{\mathcal{T}_i} = \mathcal{N}_{i+1}$
    if $i<m$ or $\mathcal{M}_{b_i}^{\mathcal{T}_i} = \mathcal{M}$ if $i =m$, and
    $\pi_i = i^{\mathcal{T}_i}_{b_i}$ is the corresponding iteration embedding
    for $i \leq m$, and
  \item if we let
    $\pi = \pi_m \circ \pi_{m-1} \circ \dots \circ \pi_0$ then for
    every $k< \omega$, \[\pi(T_{s,k}^\mathcal{N}) = T_{s,k}^\mathcal{M}.\]
  \end{enumerate}
  In this case we say that the sequence $\vec{b} = (b_i \mid i \leq m)$
  \emph{witnesses $s$-iterability} for
  $\vec{\mathcal{T}} = (\mathcal{T}_i, \mathcal{N}_i \mid i \leq m)$ or that $\vec{b}$ is an
  \emph{$s$-iterability branch} for $\vec{\mathcal{T}}$ and we write
  $\pi_{\vec{\mathcal{T}}, \vec{b}} = \pi$.
\end{definition}

Now for every two $s$-iterability branches for $\vec{\mathcal{T}}$ on $\mathcal{N}$
their corresponding iteration embeddings agree on $H_s^\mathcal{N}$.

\begin{lemma}[Uniqueness of $s$-iterability embeddings, Lemma $5.5$ in
  \cite{Sa13}]\label{lem:uniqsitemb}
  Let $\mathcal{N}$ be an $n$-suitable premouse, $s$ a finite sequence of
  ordinals, and $\vec{\mathcal{T}}$ a correctly guided finite stack on
  $\mathcal{N}$. Moreover let $\vec{b}$ and $\vec{c}$ be $s$-iterability
  branches for $\vec{\mathcal{T}}$. Then
  \[ \pi_{\vec{\mathcal{T}}, \vec{b}} \upharpoonright H_s^\mathcal{N} =
    \pi_{\vec{\mathcal{T}}, \vec{c}} \upharpoonright H_s^\mathcal{N}. \]
\end{lemma}

The uniqueness of $s$-iterability embeddings yields that for every $n$-suitable, $s$-iterable
$\mathcal{N}$, every correctly guided finite stack $\vec{\mathcal{T}}$ on $\mathcal{N}$ and
every $s$-iterability branch $\vec{b}$ for $\vec{\mathcal{T}}$, the embedding
$\pi_{\vec{\mathcal{T}}, \vec{b}} \upharpoonright H_s^\mathcal{N}$ is independent of
the choice of $\vec{b}$, but it might still depend on
$\vec{\mathcal{T}}$. This motivates the following definition.

\begin{definition}\label{def:stronglysiterable}
  Let $\mathcal{N}$ be an $n$-suitable premouse and $s$ a finite sequence of
  ordinals. Then $\mathcal{N}$ is \emph{strongly $s$-iterable} iff for every correct iterate $\mathcal{R}$ of $\mathcal{N}$, $\mathcal{R}$ is $s$-iterable and for every two correctly guided finite stacks
  $\vec{\mathcal{T}}$ and $\vec{\mathcal{U}}$ on $\mathcal{R}$ with common last model $\mathcal{M}$
  and $s$-iterability witnesses $\vec{b}$ and $\vec{c}$ for
  $\vec{\mathcal{T}}$ and $\vec{\mathcal{U}}$ respectively, we have that
  \[ \pi_{\vec{\mathcal{T}}, \vec{b}} \upharpoonright H_s^\mathcal{R} =
    \pi_{\vec{\mathcal{U}}, \vec{c}} \upharpoonright H_s^\mathcal{R}. \]
\end{definition}

A so-called \emph{bad sequence argument} shows the following lemma,
which yields the existence of strongly $s$-iterable premice.

\begin{lemma}[Lemma $5.9$ in \cite{Sa13}]\label{lem:stronglysiterable}
  For every finite sequence of ordinals $s$ and any short tree
  iterable $n$-suitable premouse $\mathcal{N}$ there is a pseudo-normal
  iterate $\mathcal{M}$ of $\mathcal{N}$ such that $\mathcal{M}$ is strongly $s$-iterable.
\end{lemma}

If $\mathcal{N}$ is strongly $s$-iterable and $\vec{\mathcal{T}}$ is a correctly
guided finite stack on $\mathcal{N}$ with last model $\mathcal{M}$, let
$\pi_{\mathcal{N},\mathcal{M},s} : H_s^\mathcal{N} \rightarrow H_s^\mathcal{M}$ denote the embedding
given by any $s$-iterability branch $\vec{b}$ for $\vec{\mathcal{T}}$. As
$\mathcal{N}$ is strongly $s$-iterable, the embedding $\pi_{\mathcal{N},\mathcal{M},s}$ does
not depend on the choice of $\vec{\mathcal{T}}$ and $\vec{b}$.

Recall that we write
$M_{n+1}^- = M_{n+1} | (\delta_0^{+\omega})^{M_{n+1}}$, where
$\delta_0$ is the least Woodin cardinal in $M_{n+1}$, and
$\Sigma_{M_{n+1}^-}$ for the canonical iteration strategy for
$M_{n+1}^-$ induced by $\Sigma_{M_{n+1}}$. Moreover, recall that for $m<\omega$, we write $s_m$ for the set of the first $m$ uniform indiscernibles. Then $M_{n+1}^-$ is
$n$-suitable and strongly $s_m$-iterable for every $m$. Moreover, if
$\vec{\mathcal{T}}$ is a correctly guided finite stack on $M_{n+1}^-$ with
last model $\mathcal{M}$, then $\pi_{M_{n+1}^-, \mathcal{M},s_m}$ agrees with the
iteration embedding according to $\Sigma_{M_{n+1}^-}$ on $H_{s_m}^{M_{n+1}^-}$. The first direct limit
system we define will consist of iterates of $M_{n+1}^-$.

\begin{definition}
  Let
  \[{\tilde\mathcal{F}}^+ = \{ \mathcal{N} \mid \mathcal{N} \text{ is an iterate of } M_{n+1}^- \text{
      via } \Sigma_{M_{n+1}^-} \text{ by a finite stack of trees}\}\] and for $\mathcal{N}, \mathcal{M} \in {\tilde\mathcal{F}}^+$ let
  $\mathcal{N} \leq^+ \mathcal{M}$ iff $\mathcal{M}$ is an iterate of $\mathcal{N}$ via the tail
  strategy $\Sigma_\mathcal{N}$ as witnessed by some finite stack of iteration
  trees. Then we let ${\tilde\cM_{\infty}}^+$ be the direct limit of
  $({\tilde\mathcal{F}}^+, \leq^+)$ under the iteration maps. \comm{Moreover for
  $\mathcal{N} \in {\tilde}\mathcal{F}^+$ let $i_{\mathcal{N},\infty} : \mathcal{N} \rightarrow {\tilde\cM_{\infty}}^+$
  denote the corresponding direct limit embedding.}
\end{definition}

\begin{remark}
  The prewellordering $\leq^+$ on ${\tilde\mathcal{F}}^+$ is directed and the direct
  limit ${\tilde\cM_{\infty}}^+$ is well-founded as the limit system
  $({\tilde\mathcal{F}}^+, \leq^+)$ only consists of iterates of $M_{n+1}^-$ via the
  canonical iteration strategy $\Sigma_{M_{n+1}^-}$.
\end{remark}

Since ${\tilde\mathcal{F}}^+$ is not definable enough for our purposes, we now
introduce another direct limit system which has the same direct limit
${\tilde\cM_{\infty}}^+$.

\begin{definition}
  Let
  \[ \tilde\mathcal{I} = \{ (\mathcal{N}, s) \mid \mathcal{N} \text{ is } n\text{-suitable}, s \in
    [\ensuremath{\operatorname{Ord}} ]^{<\omega}, \text{ and } \mathcal{N} \text{ is strongly }
    s\text{-iterable} \} \] and
  \[ \tilde\mathcal{F} = \{ H_s^\mathcal{N} \mid (\mathcal{N},s) \in \tilde\mathcal{I} \}. \] For
  $(\mathcal{N},s), (\mathcal{M},t) \in \tilde\mathcal{I}$ we let $(\mathcal{N},s) \leq_{\tilde\mathcal{I}} (\mathcal{M},t)$ iff
  there is a correctly guided finite stack on $\mathcal{N}$ with last model
  $\mathcal{M}$ and $s \subseteq t$. In this case we let
  $\pi_{(\mathcal{N},s), (\mathcal{M},t)}:H_s^{\mathcal{N}} \rightarrow H_t^{\mathcal{M}}$ denote
  the canonical corresponding embedding.
\end{definition}

\begin{remark}
  The prewellordering $\leq_{\tilde\mathcal{I}}$ on $\tilde\mathcal{I}$ is directed: Let
  $(\mathcal{N},s), (\mathcal{M},t) \in \tilde\mathcal{I}$. By Lemma \ref{lem:stronglysiterable}
  there exists an $n$-suitable premouse $\mathcal{R}$ which is strongly
  $(s \cup t)$-iterable. Let $\mathcal{S}$ be the result of simultaneously
  comparing $\mathcal{N}$, $\mathcal{M}$ and $\mathcal{R}$ in the sense of Lemma
  \ref{lem:pseudocomp}. Then $(\mathcal{S}, s \cup t) \in \tilde\mathcal{I}$,
  $(\mathcal{N}, s) \leq_{\tilde\mathcal{I}} (\mathcal{S}, s \cup t)$, and
  $(\mathcal{M}, t) \leq_{\tilde\mathcal{I}} (\mathcal{S}, s \cup t)$, as desired.
\end{remark}

\begin{definition}
  Let $\tilde\cM_{\infty}$ be the direct limit of $(\tilde\mathcal{F}, \leq_{\tilde\mathcal{I}})$ under the
  embeddings $\pi_{(\mathcal{N},s), (\mathcal{M},t)}$. For $(\mathcal{N}, s) \in \tilde\mathcal{I}$ let
  $\pi_{(\mathcal{N},s),\infty} : H_s^\mathcal{N} \rightarrow \tilde\cM_{\infty}$ denote the
  corresponding direct limit embedding.
\end{definition}

The fact that $\tilde\cM_{\infty}$ is well-founded follows from the next lemma.

\begin{lemma}[Lemma $5.10$ in \cite{Sa13}]\label{lem:dlmequal}
  $\tilde\cM_{\infty} = {\tilde\cM_{\infty}}^+$.
\end{lemma}

\subsection*{The second direct limit system}

To obtain $\ensuremath{\operatorname{HOD}} $ of some inner model from the direct limit, we in
particular need to show that the direct limit is in fact contained
in $\ensuremath{\operatorname{HOD}} $ of that inner model. In our setting we therefore need to
internalize the direct limit system into the inner model $M_n(x)[g]$ fixed above. We first aim to define a direct limit system similar to
$(\tilde\mathcal{F}, \leq_{\tilde\mathcal{I}})$ in $M_n(x)$ analogous to \cite{Sa13}. In
a second step, we then modify the system to obtain direct limit
systems with the same direct limit which are definable in
$M_n(x)[g]$.

The notion of $n$-suitability from Definition \ref{def:nsuit} is
already internal to $M_n(x)$ and $M_n(x)[g]$, i.e., if $\mathcal{N} \in M_n(x)|\kappa$
then $\mathcal{N}$ is $n$-suitable in $V$ iff $\mathcal{N}$ is $n$-suitable in
$M_n(x)$ by the following lemma.

\begin{lemma}\label{lem:closureSn} Let $\delta_0$ denote the least Woodin cardinal in $M_n(x)$.
  \begin{enumerate}
  \item For all $y \in V^{M_n(x)[g]}_{\delta_0}$, $Lp^n(y) \in \ensuremath{\operatorname{HOD}} _y^{M_n(x)[g]}$.
  \item $V^{M_n(x)}_{\delta_0}$ and $V^{M_n(x)[g]}_{\delta_0}$ are closed under the operation $y \mapsto Lp^n(y)$.
  \end{enumerate}
\end{lemma}

\begin{proof}
  Let $y \in V^{M_n(x)[g]}_{\delta_0}$ be arbitrary. The model $M_n(x)[g]$ can be organized as a $V_\kappa^{M_n(x)[g]}$-premouse and as such it inherits the iterability from $M_n(x)$ and is in fact equal to $M_n(V_\kappa^{M_n(x)[g]})$. Consider $L[E](y)^{M_n(x)[g]}$, the result of a fully backgrounded extender construction above $y$ using extenders from the sequence of $M_n(x)[g]$ organized as a $V_\kappa^{M_n(x)[g]}$-premouse, and compare it with $Lp^n(y)$. First, we argue that $Lp^n(y)$ does not move. If it would move, the $Lp^n(y)$-side of the coiteration would have to drop because $Lp^n(y)$ does not have any total extenders. Moreover, it would have to iterate to a proper class model which is equal to an iterate of $L[E](y)^{M_n(x)[g]}$. As $L[E](y)^{M_n(x)[g]}$ has $n$ Woodin cardinals, this would imply that $Lp^n(y)$ has a level which is not $n$-small, contradicting the definition of $Lp^n(y)$.

  Therefore, $Lp^n(y) \lhd \mathcal{R}$ for some iterate $\mathcal{R}$ of $L[E](y)^{M_n(x)[g]}$. The iteration from $L[E](y)^{M_n(x)[g]}$ to $\mathcal{R}$ resulting from the comparison process can be defined over $L[E](y)^{M_n(x)[g]}$ from the extender sequence of $L[E](y)^{M_n(x)[g]}$ and a finite sequence of ordinals as it cannot leave any total measures behind and thus can only use measures of order $0$. The extender sequence of the $V_\kappa^{M_n(x)[g]}$-premouse $M_n(x)[g]$ is in $\ensuremath{\operatorname{HOD}} ^{M_n(x)[g]}_{V_\kappa^{M_n(x)[g]}} = \ensuremath{\operatorname{HOD}} ^{M_n(x)[g]}$. Therefore $Lp^n(y) \in \ensuremath{\operatorname{HOD}} ^{M_n(x)[g]}$ by the definability of the $L[E]$-construction.

  For $(2)$, the closure of $V^{M_n(x)[g]}_{\delta_0}$ follows immediately from $(1)$. For $V^{M_n(x)}_{\delta_0}$ notice that for $y \in V^{M_n(x)}_{\delta_0}$, $Lp^n(y) \in \ensuremath{\operatorname{HOD}} _y^{M_n(x)[g]} \subseteq \ensuremath{\operatorname{HOD}} _y^{M_n(x)}$ by homogeneity of the forcing.
\end{proof}

By \emph{stacking} the $Lp^n$-operation, this lemma in fact shows that for all $y \in V_{\delta_0}^{M_n(x)}$, $M_n(y)|\kappa_0 \in \ensuremath{\operatorname{HOD}^{M_n(x)[g]}} _y$, where $\kappa_0$ denotes the least measurable cardinal in $M_n(y)$.

The definitions of short tree, maximal tree, and correctly guided finite stack we gave above are internal to $M_n(x)$ and $M_n(x)[g]$ as well, as they can be defined only using the $Lp^n$-operation. The only notion we have to take care of is $s$-iterability since it is not even clear how the sets $T_{s,k}^\mathcal{N}$ can be identified inside $M_n(x)$. This obstacle is solved by shrinking the direct limit system $(\tilde\mathcal{F}, \leq_{\tilde\mathcal{I}})$ to a dense subset as follows.

\begin{definition}
  Let
  \begin{align*}
    \mathcal{G} & = \;   \{ \mathcal{N} \in M_n(x) | \kappa \mid \mathcal{N} \text{ is }
                   n\text{-suitable and } M_n(x) \vDash \text{``for
                      some cardinal}\\
                 & \; \text{cutpoint } \eta,
                   \delta^\mathcal{N} = \eta^+, \mathcal{N} | \delta^\mathcal{N} \in \mathcal{P}(M_n(x) | \eta^+) \cap M_n(x) | (\eta^+ + \omega), \\
                &  \;  \text{and } M_n(x) | \eta \text{ is generic
                   over } \mathcal{N} \text{ for the } \delta^\mathcal{N}\text{-generator version of} \\ & \; \; \; \; \; \; \text{the extender algebra at } \delta^\mathcal{N} \text{''} \}.
  \end{align*}
\end{definition}

See for example Section $4.1$ in \cite{Fa} for an introduction to the
$\delta$-generator version of the extender algebra at some Woodin
cardinal $\delta$.
The following lemma shows how we can use the fact that $\mathcal{N} \in \mathcal{G}$ to
detect $M_n(\mathcal{N} | \delta^{\mathcal{N}})$ inside $M_n(x)$. For some premouse
$\mathcal{R} \in \mathcal{G}$ we denote the last model of a $\mathcal{P}$-construction
above $\mathcal{R}|\delta^\mathcal{R}$ performed inside $M_n(x)$ as introduced in \cite{SchSt09}
(see also Proposition $2.3$ and Definition $2.4$ in \cite{Sa13}) by
$\mathcal{P}^{M_n(x)}(\mathcal{R}|\delta^\mathcal{R})$.

\begin{lemma}[Lemma $5.11$ in \cite{Sa13}] \label{lem:Pconstr} Let
  $\mathcal{N} \in M_n(x)|\kappa$ be an $n$-suitable premouse such that for
  some cardinal cutpoint $\eta < \delta^\mathcal{N}$ of $M_n(x)$, we have that
  $\mathcal{N} | \delta^\mathcal{N} \in \mathcal{P}(M_n(x) | \eta^+) \cap M_n(x) | (\eta^+ + \omega)$ and
  $M_n(x) | \eta$ is generic over $\mathcal{N}$ for the $\delta^\mathcal{N}$-generator
  version of the extender algebra at $\delta^\mathcal{N}$. Then
  $\mathcal{N} \in \mathcal{G}$ and
  \[ \mathcal{P}^{M_n(x)}(\mathcal{N} | \delta^\mathcal{N}) = M_n(\mathcal{N} | \delta^\mathcal{N}). \] In particular, $M_n(\mathcal{N}|\delta^\mathcal{N})[M_n(x)|\eta] = M_n(x)$.
\end{lemma}

Using pseudo-genericity iterations (see Lemma \ref{lem:pseudogenit})
we can obtain the following corollary.

\begin{cor}\label{cor:itintoG}
  Let $\mathcal{N}$ be a short tree iterable $n$-suitable premouse such that
  $\mathcal{N} \in M_n(x) | \kappa$. Then there is a correctly guided finite
  stack on $\mathcal{N}$ with last model $\mathcal{M}$ such that $\mathcal{M} \in \mathcal{G}$
  and $\mathcal{P}^{M_n(x)}(\mathcal{M} | \delta^\mathcal{M}) = M_n(\mathcal{M} | \delta^\mathcal{M})$.
\end{cor}

Now the following definition of $s$-iterability agrees with the
previous one given in Definition \ref{def:siterable} for $n$-suitable
premice in $\mathcal{G}$.

\begin{definition}\label{def:siterableinternal}
  For $\mathcal{N} \in \mathcal{G}$, $s \in [\ensuremath{\operatorname{Ord}} ]^{<\omega}$, and $k < \omega$
  let
  \begin{align*}
    T_{s,k}^{\mathcal{N},*} = \{ (t, \ulcorner\phi\urcorner) \in
                        [((\delta^\mathcal{N})^{+k})^\mathcal{N}]^{<\omega} & \times
                                                              \omega \mid \phi \text{ is a }
                        \Sigma_1\text{-formula and } \\
                      & \mathcal{P}^{M_n(x)}(\mathcal{N} | \delta^\mathcal{N}) \vDash \phi[t,s]
                        \}.
  \end{align*}
  Then we say for $\mathcal{N} \in \mathcal{G}$ and $s \in [\ensuremath{\operatorname{Ord}} ]^{<\omega}$ that
  $M_n(x) \vDash$ ``$\mathcal{N}$ is $s$-iterable below $\kappa$'' iff for every $\ensuremath{\operatorname{Col}} (\omega, {<}\kappa)$-generic $G$ over $M_n(x)$ and every correctly guided finite stack $\vec{\mathcal{T}} = (\mathcal{T}_i, \mathcal{N}_i \mid i \leq m) \in \ensuremath{\operatorname{HC}} ^{M_n(x)[G]}$ on
  $\mathcal{N}$ with last model $\mathcal{M} \in \mathcal{G}$, there is a
  sequence of branches $\vec{b} = (b_i \mid i \leq m) \in M_n(x)[G]$
  and a sequence of embeddings $(\pi_i \mid i \leq m)$ satisfying
  $(i)-(iii)$ in Definition \ref{def:siterable} such that if we let
  $\pi_{\vec{\mathcal{T}},\vec{b}} = \pi_m \circ \pi_{m-1} \circ \dots \circ
  \pi_0$, then for every $k<\omega$,
  \[ \pi_{\vec{\mathcal{T}},\vec{b}}(T_{s,k}^{\mathcal{N},*}) = T_{s,k}^{\mathcal{M},*}. \]
\end{definition}

In addition, we define $M_n(x) \vDash$ ``$\mathcal{N}$ is strongly
$s$-iterable below $\kappa$'' analogous to Definition
\ref{def:stronglysiterable} for all $\ensuremath{\operatorname{Col}} (\omega,{<}\kappa)$-generic $G$ and stacks $\vec\mathcal{T}, \vec\mathcal{U} \in M_n(x)[G]$. For $\mathcal{N} \in \mathcal{G}$,
$s \in [\ensuremath{\operatorname{Ord}} ]^{<\omega}$, and $k < \omega$, we have
$T_{s,k}^{\mathcal{N},*} = T_{s,k}^{\mathcal{N}}$, so we will omit the $*$ for
$\mathcal{N} \in \mathcal{G}$. Using this, $\gamma_s^{\mathcal{N}}$ and $H_s^{\mathcal{N}}$ are
defined as before. Then we can define the internal direct limit system
as follows.

\begin{definition}
  Let
  \begin{align*}
     \mathcal{I} = \{ (\mathcal{N},s) & \mid \mathcal{N} \in \mathcal{G}, s \in
    [\ensuremath{\operatorname{Ord}} ]^{<\omega}, \text{ and } \\ & M_n(x) \vDash \text{``} \,\mathcal{N} \text{
      is strongly } s\text{-iterable below } \kappa\text{''} \}
  \end{align*}
  and
  \[ \mathcal{F} = \{ H_s^{\mathcal{N}} \mid (\mathcal{N},s) \in \mathcal{I} \}. \]
  Moreover, for $(\mathcal{N},s), (\mathcal{M},t) \in \mathcal{I}$ we let
  $(\mathcal{N},s) \leq (\mathcal{M},t)$ iff there is a correctly guided finite
  stack on $\mathcal{N}$ with last model $\mathcal{M}$ and $s \subseteq t$. In this
  case we let as before
  $\pi_{(\mathcal{N},s), (\mathcal{M},t)}:H_s^{\mathcal{N}} \rightarrow H_t^{\mathcal{M}}$ denote the
  canonical corresponding embedding.
\end{definition}

For clarity, we sometimes write $\leq_\mathcal{I}$ for $\leq$. Similar as before we have that for every $\mathcal{N} \in \mathcal{G}$ and $s \in [\ensuremath{\operatorname{Ord}} ]^{<\omega}$ there is a normal correct iterate $\mathcal{M}$ of $\mathcal{N}$ such that $(\mathcal{M},s) \in \mathcal{I}$. Using the fact that $\kappa$ is inaccessible and a limit of cutpoints in $M_n(x)$ we can obtain the following lemma.

\begin{lemma}[Lemma $5.14$ in \cite{Sa13}]
  $\leq$ is directed.
\end{lemma}

Therefore we can again define the direct limit.

\begin{definition}
  Let $\cM_{\infty}$ be the direct limit of $(\mathcal{F}, \leq)$ under
  the embeddings $\pi_{(\mathcal{N},s),(\mathcal{M},t)}$. Moreover, let
  $\delta_{\infty} = \delta^{\cM_{\infty}}$ be the Woodin cardinal in $\cM_{\infty}$ and
  $\pi_{(\mathcal{N},s), \infty} : H_s^{\mathcal{N}} \rightarrow \cM_{\infty}$ be the direct
  limit embedding for all $(\mathcal{N}, s) \in \mathcal{I}$.
\end{definition}

An argument similar to the one for Lemma \ref{lem:dlmequal} shows that
this direct limit is well-founded as well. As we will use ideas from
this proof in the next section, we will give some details here. We
again first define another direct limit system which consists of
iterates of $M_{n+1}^-$ and then show that its direct limit $\cM_{\infty}^+$
is equal to $\cM_{\infty}$.

\begin{definition}
  Let
  \begin{align*}
    \mathcal{F}^+ = \{ \mathcal{Q} \in \mathcal{G} \mid \mathcal{Q} & \text{ is the last
      model of a correctly guided} \\ & \text{finite stack on } M_{n+1}^- \text{
      via } \Sigma_{M_{n+1}^-} \}.
  \end{align*}
  Moreover, let $\mathcal{P} \leq^+ \mathcal{Q}$ for $\mathcal{P}, \mathcal{Q} \in \mathcal{F}^+$
  iff there is a correctly guided finite stack on $\mathcal{P}$ according to
  the tail strategy $\Sigma_{\mathcal{P}}$ with last model $\mathcal{Q}$. In this case
  we let $i_{\mathcal{P}, \mathcal{Q}}: \mathcal{P} \rightarrow \mathcal{Q}$ denote the corresponding
  iteration embedding.
\end{definition}

Then $\leq^+$ on $\mathcal{F}^+$ is directed, so we can define
the direct limit.

\begin{definition}
  Let $\cM_{\infty}^+$ be the direct limit of $(\mathcal{F}^+, \leq^+)$
  under the embeddings $i_{\mathcal{P}, \mathcal{Q}}$. Moreover, let
  $i_{\mathcal{Q},\infty}: \mathcal{Q} \rightarrow \cM_{\infty}^+$ denote the direct limit
  embedding for all $\mathcal{Q} \in \mathcal{F}^+$.
\end{definition}

Then it is easy to see that $\cM_{\infty}^+$ is well-founded as $\mathcal{F}^+$
only consists of iterates of $M_{n+1}^-$ according to the canonical
iteration strategy $\Sigma_{M_{n+1}^-}$.

\begin{lemma}[Lemma $5.15$ in \cite{Sa13}] \label{lem:dlmeqdlmplus}
  $\cM_{\infty}^+ = \cM_{\infty}$ and hence $\cM_{\infty}$ is well-founded.
\end{lemma}

\begin{proof}
  We construct a sequence $(\mathcal{Q}_i \mid i < \omega)$ of iterates of
  $M_{n+1}^-$ such that $\mathcal{Q}_i \in \mathcal{F}^+$ for every
  $i < \omega$ and $(\mathcal{Q}_i \mid i < \omega)$ is cofinal in
  $\mathcal{G}$, i.e., for every $\mathcal{N} \in \mathcal{G}$ there is an
  $i<\omega$ such that $\mathcal{Q}_i$ is the last model of a correctly guided
  finite stack on $\mathcal{N}$.

  In $V$, fix some sequence $(\xi_i \mid i < \omega)$ of ordinals cofinal in $\kappa$. We define $(\mathcal{Q}_i \mid i < \omega)$ together with a strictly
  increasing sequence $(\eta_i \mid i < \omega)$ of cardinal cutpoints
  of $M_n(x)|\kappa$ by induction on $i < \omega$. So let
  $\mathcal{Q}_0 = M_{n+1}^-$ and let $\eta_0 < \kappa$ be a cardinal cutpoint
  of $M_n(x)$. Moreover assume that we already constructed
  $(\mathcal{Q}_i \mid i \leq j)$ and $(\eta_i \mid i \leq j)$ with the above
  mentioned properties such that in addition
  $(\mathcal{Q}_i \mid i \leq j) \in M_n(x) | \eta_j$. Let $\mathcal{Q}_{j+1}^*$ be the
  result of simultaneously pseudo-comparing (in the sense of Lemma
  \ref{lem:pseudocomp}) all $n$-suitable premice $\mathcal{M}$ such that
  $\mathcal{M} \in \mathcal{G} \cap M_n(x) | \eta_j$. Then in particular
  $\mathcal{Q}_{j+1}^*$ is a normal iterate of $\mathcal{Q}_{j}$ according to the
  canonical tail iteration strategy $\Sigma_{\mathcal{Q}_j}$, but
  $\mathcal{Q}_{j+1}^*$ might not be in $\mathcal{G}$. Let $\nu$ be a cardinal
  cutpoint of $M_n(x)$ such that $\eta_j < \nu < \kappa$ and
  $\mathcal{Q}_{j+1}^* \in M_n(x) | \nu$. Note that such a $\nu$ exists as
  $\kappa$ is inaccessible and a limit of cardinal cutpoints in
  $M_n(x)$. Let $\mathcal{Q}_{j+1}$ be the normal iterate of $\mathcal{Q}_{j+1}^*$
  according to the canonical tail strategy $\Sigma_{\mathcal{Q}_{j+1}^*}$ of
  $\Sigma_{\mathcal{Q}_j}$ obtained by Woodin's genericity iteration such that
  $M_n(x) | \nu$ is generic over $\mathcal{Q}_{j+1}$ for the
  $\delta^{\mathcal{Q}_{j+1}}$-generator version of the extender algebra (see
  for example Section $4.1$ in \cite{Fa}). Then
  $\mathcal{Q}_{j+1} \in \mathcal{G}$ is as desired. Finally choose
  $\eta_{j+1} < \kappa$ such that $\eta_{j+1} > \max(\eta_j, \xi_j)$, $\eta_{j+1}$ is a cardinal cutpoint in $M_n(x)$ and $(\mathcal{Q}_i \mid i \leq j+1) \in M_n(x) | \eta_{j+1}$.

  Now we define an embedding $\sigma : \cM_{\infty} \rightarrow \cM_{\infty}^+$ as
  follows. Let $x \in \cM_{\infty}$. Since $(\mathcal{Q}_i \mid i < \omega)$ is cofinal
  in $\mathcal{G}$, there are $i,m<\omega$ such that
  $(\mathcal{Q}_i,s_m) \in \mathcal{I}$ and
  $x = \pi_{(\mathcal{Q}_i,s_m),\infty}(\bar{x})$ for some
  $\bar{x} \in H_{s_m}^{\mathcal{Q}_i} \subseteq \mathcal{Q}_i$. Then we let
  $\sigma(x) = i_{\mathcal{Q}_i,\infty}(\bar{x})$.

  It follows as in the proof of Lemma $5.10$ in \cite{Sa13} that the
  definition of $\sigma$ does not depend on the choice of
  $i,m < \omega$ and in fact $\sigma = \ensuremath{\operatorname{id}}$.
\end{proof}

Moreover, it is possible to compute $\delta_{\infty}$.

\begin{lemma}[Lemma $5.16$ in \cite{Sa13}]
  $\delta_{\infty} = (\kappa^+)^{M_n(x)}$.
\end{lemma}

\subsection*{Direct limit systems in $\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $}

Finally, we will argue that $\cM_{\infty} \in \ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $ by first defining direct
limit systems in various premice $M(y)$ satisfying certain properties
definable in $M_n(x)[g]$ and then showing that the direct limits
$\cM_{\infty}^{M(y)}$ are equal to $\cM_{\infty}$. A similar approach but in a
completely different setting can be found in \cite{SaSch18}.

In what follows, we will let $(K(z))^N$ denote the core model
constructed above a real $z$ inside some $n$-small model $N$ with $n$
Woodin cardinals in the sense of \cite{Sch06}, i.e., the core model
$K(z)$ is constructed between consecutive Woodin cardinals. Lemma
$1.1$ in \cite{Sch06} (due to John Steel) implies that
$(K(x))^{M_n(x)} = M_n(x)$. We will use this fact and consider more
arbitrary premice with this property in what follows. We
state the following definitions in $V$, but we will later apply them inside
$M_n(x)[g]$.

\begin{definition}\label{def:predlmsuit}
  Let $y \in {}^\omega\omega \cap M_n(x)[g]$. Then we say $y$ is
  \emph{pre-dlm-suitable} iff there is a proper class $y$-premouse
  $M(y)$ satisfying the following properties.
  \begin{enumerate}[$(i)$]
  \item $M(y)$ is $n$-small and has $n$ Woodin cardinals,
  \item the least inaccessible cardinal in $M(y)$ is $\kappa$,
  \item $M(y) = (K(y))^{M(y)}$, and
  \item there is a $\ensuremath{\operatorname{Col}} (\omega, {<}\kappa)$-generic $h$ over $M(y)$
    such that \[ M(y)[h] = M_n(x)[g]. \]
  \end{enumerate}
  We also call such a $y$-premouse $M(y)$ \emph{pre-dlm-suitable} and say
  that \emph{$M(y)$ witnesses that $y$ is pre-dlm-suitable}.
\end{definition}

Using this, we can define a version of the direct limit system
$\mathcal{F}$ inside arbitrary pre-dlm-suitable $y$-premice $M(y)$.

\begin{definition}
  Let $y \in {}^\omega\omega$ be pre-dlm-suitable as witnessed by $M(y)$. Then we let
   \begin{align*}
    \mathcal{G}^{M(y)} & = \;  \{ \mathcal{N} \in M(y)|\kappa \mid \mathcal{N} \text{ is }
                            n\text{-suitable and } M(y) \vDash \text{``for
                      some cardinal}\\
                 & \; \text{cutpoint } \eta,
                   \delta^\mathcal{N} = \eta^+, \mathcal{N} | \delta^\mathcal{N} \in \mathcal{P}(M(y) | \eta^+) \cap M(y) | (\eta^+ + \omega), \\
                &  \;  \text{and } M(y) | \eta \text{ is generic
                   over } \mathcal{N} \text{ for the } \delta^\mathcal{N}\text{-generator version of} \\ & \; \; \; \; \; \; \text{the extender algebra at } \delta^\mathcal{N} \text{''} \}.
  \end{align*}
\end{definition}

Analogous as before, we can now define when for an $n$-suitable premouse $\mathcal{N}$, $M(y) \vDash \text{``} \mathcal{N}$ is strongly $s$-iterable below $\kappa$'' by referring to $\mathcal{P}^{M(y)}(\mathcal{N}|\delta^\mathcal{N})$ in the definition of $(T_{s,k}^{\mathcal{N},*})^{M(y)}$. Let $\gamma_s^{\mathcal{N},M(y)}$ and $H_s^{\mathcal{N},M(y)}$ be defined analogous to $\gamma_s^{\mathcal{N}}$ and $H_s^{\mathcal{N}}$ inside $M(y)$ using $(T_{s,k}^{\mathcal{N},*})^{M(y)}$. For $M(y) = M_n(x)$ and $\mathcal{N} \in \mathcal{G}$ this agrees with our previous definition of strong $s$-iterability.

\begin{definition}
  Let $y \in {}^\omega\omega$ be pre-dlm-suitable as witnessed by $M(y)$. Then we let
  \begin{align*}
    \mathcal{I}^{M(y)} & = \{ (\mathcal{N},s) \mid \mathcal{N} \in \mathcal{G}^{M(y)}, s \in
                                    [\ensuremath{\operatorname{Ord}} ]^{<\omega}, \text{ and} \\ & M(y)
                                                               \vDash
                                                               \text{``}
                                                               \,\mathcal{N}
                                                               \text{
                                                               is
                                                               strongly
                                                               }
                                                               s\text{-iterable
                                                               below }
                                                               \kappa\text{''}
                                                               \}
  \end{align*}
  and
  \[ \mathcal{F}^{M(y)} = \{ H_s^{\mathcal{N},M(y)} \mid (\mathcal{N},s) \in
    \mathcal{I}^{M(y)} \}. \] Moreover, for
  $(\mathcal{N},s), (\mathcal{M},t) \in \mathcal{I}^{M(y)}$ we let
  $(\mathcal{N},s) \leq_{\mathcal{I}^{M(y)}} (\mathcal{M},t)$ iff there is a
  correctly guided finite stack on $\mathcal{N}$ with last model $\mathcal{M}$ and
  $s \subseteq t$. In this case we let
  $\pi^{M(y)}_{(\mathcal{N},s), (\mathcal{M},t)}:H_s^{\mathcal{N},M(y)} \rightarrow
  H_t^{\mathcal{M},M(y)}$ denote the canonical corresponding embedding. Finally, let $\cM_{\infty}^{M(y)}$ denote the direct limit of
  $(\mathcal{F}^{M(y)}, \leq_{\mathcal{I}^{M(y)}})$ under these
  embeddings.
\end{definition}

We will now strengthen this and define when a real $y \in {}^\omega\omega$ (or a
$y$-premouse $M(y)$) is dlm-suitable.

\begin{definition}\label{def:dlmsuit}
  Let $y \in {}^\omega\omega \cap M_n(x)[g]$ be pre-dlm-suitable as witnessed by
  some $y$-premouse $M(y)$. We say that $y$ is \emph{dlm-suitable}
  (witnessed by $M(y)$) iff
  \begin{enumerate}[$(i)$]
  \item for every $s \in [\ensuremath{\operatorname{Ord}} ]^{<\omega}$ there is a premouse $\mathcal{N}$
    such that $(\mathcal{N},s) \in \mathcal{I}^{M(y)}$, and
  \item for every $\mathcal{N} \in \mathcal{G}^{M(y)}$,
    \[\mathcal{P}^{M(y)}(\mathcal{N}|\delta^{\mathcal{N}}) = K^{M_n(x)[g]}(\mathcal{N}|\delta^{\mathcal{N}}).\]
  \end{enumerate}
\end{definition}

\begin{lemma}
  $M_n(x)$ witnesses that $x$ is dlm-suitable.
\end{lemma}
\begin{proof}
  The fact that $M_n(x)$ satisfies $(i)$ follows from Lemma
  \ref{lem:stronglysiterable} and Corollary \ref{cor:itintoG}, so we
  only have to show $(ii)$.  Let $\mathcal{N} \in \mathcal{G}$. Then
  $\mathcal{P}^{M_n(x)}(\mathcal{N}|\delta^\mathcal{N}) = M_n(\mathcal{N}|\delta^\mathcal{N})$ by Lemma
  \ref{lem:Pconstr}. Moreover, there is some $G$ generic over the
  result of the $\mathcal{P}$-construction $\mathcal{P}^{M_n(x)}(\mathcal{N}|\delta^\mathcal{N})$ for
  the $\delta^\mathcal{N}$-generator version of the extender algebra at
  $\delta^\mathcal{N}$ with $\mathcal{P}^{M_n(x)}(\mathcal{N}|\delta^\mathcal{N})[G] = M_n(x)$. That
  means
  \[ M_n(\mathcal{N}|\delta^\mathcal{N})[G] = M_n(x). \] Now,
  \begin{align*}
    K^{M_n(x)[g]}(\mathcal{N}|\delta^\mathcal{N}) & =
    K^{M_n(\mathcal{N}|\delta^\mathcal{N})[G][g]}(\mathcal{N}|\delta^\mathcal{N}) =
    K^{M_n(\mathcal{N}|\delta^\mathcal{N})}(\mathcal{N}|\delta^\mathcal{N}) \\ & = M_n(\mathcal{N}|\delta^\mathcal{N}) =
    \mathcal{P}^{M_n(x)}(\mathcal{N}|\delta^\mathcal{N}),
  \end{align*}
  by generic absoluteness of the core model and Lemma 1.1 in
  \cite{Sch06} (due to Steel).
\end{proof}

Condition $(ii)$ in Definition \ref{def:dlmsuit} will ensure that for
any dlm-suitable $y$-premouse $M(y)$ and
$(\mathcal{N},s), (\mathcal{M},t) \in \mathcal{I} \cap \mathcal{I}^{M(y)}$ with
$(\mathcal{N},s) \leq_{\mathcal{I}} (\mathcal{M},t)$ and
$(\mathcal{N},s) \leq_{\mathcal{I}^{M(y)}} (\mathcal{M},t)$, the induced embeddings
$\pi_{(\mathcal{N},s), (\mathcal{M},t)}$ and $\pi^{M(y)}_{(\mathcal{N},s), (\mathcal{M},t)}$
agree. Hence we can show in the following lemma that the direct limit
$\cM_{\infty}^{M(y)}$ defined inside some dlm-suitable $M(y)$ will in fact be
the same as the direct limit $\cM_{\infty}$ defined inside $M_n(x)$.

\begin{lemma}\label{lem:dlmM(y)eq}
  Let $y \in {}^\omega\omega$ be dlm-suitable as witnessed by $M(y)$. Then
  $\mathcal{F}$ and $\mathcal{F}^{M(y)}$ have cofinally many points in
  common and $\cM_{\infty} = \cM_{\infty}^{M(y)}$.
\end{lemma}

\begin{proof}
  Let $h$ be $\ensuremath{\operatorname{Col}} (\omega, {<}\kappa)$-generic over $M(y)$ such that
  $M(y)[h] = M_n(x)[g]$. Let $(\mathcal{N},s) \in \mathcal{I}$ and
  $(\mathcal{N}^\prime,s^\prime) \in \mathcal{I}^{M(y)}$. We aim to show that
  there is some $(\mathcal{M}, t) \in \mathcal{I} \cap \mathcal{I}^{M(y)}$ such
  that $(\mathcal{N},s) \leq_{\mathcal{I}} (\mathcal{M},t)$ and
  $(\mathcal{N}^\prime, s^\prime) \leq_{\mathcal{I}^{M(y)}} (\mathcal{M},t)$. As
  condition $(ii)$ in Definition \ref{def:dlmsuit} yields that the
  embeddings associated to $\mathcal{F}$ and $\mathcal{F}^{M(y)}$ agree,
  this suffices to show that $\cM_{\infty} = \cM_{\infty}^{M(y)}$.

  Let $t = s \cup s^\prime$. By assumption, there is a $t$-iterable
  premouse $\mathcal{R}$ in $M_n(x)$ and a $t$-iterable premouse $\mathcal{R}^\prime$
  in $M(y)$. Therefore we can assume that $\mathcal{N}$ and $\mathcal{N}^\prime$ are
  both $t$-iterable in $M_n(x)$ and $M(y)$ respectively as we can
  replace them by the result of their coiteration with $\mathcal{R}$ and
  $\mathcal{R}^\prime$ respectively.

  By the choice of $M(y)$ and generic absoluteness of the core model
  we have
  \begin{align}
    \label{eq:1}
    M(y) & = (K(y))^{M(y)} = (K(y))^{M(y)[h]} \\ & = (K(y))^{M_n(x)[g]} =
    (K(y))^{M_n(x)[g \upharpoonright \xi]}, \nonumber
  \end{align}
  where $\xi < \kappa$ is
  such that $y \in M_n(x)[g \upharpoonright \xi]$. Analogously, using
  Lemma $1.1$ in \cite{Sch06} due to Steel and generic absoluteness of
  the core model again,
  \begin{align}
    \label{eq:2}
    M_n(x) & = (K(x))^{M_n(x)} = (K(x))^{M_n(x)[g]} \\ & = (K(x))^{M(y)[h]}
    = (K(x))^{M(y)[h \upharpoonright \xi^\prime]}, \nonumber
  \end{align}
  where $\xi^\prime < \kappa$ is such that
  $x \in M(y)[h \upharpoonright \xi^\prime]$. Now we can obtain the following claim.

  \begin{claim}\label{cl:ctpts}
    $M(y)$ and $M_n(x)$ have cofinally many common
    cardinal cutpoints below $\kappa$.
  \end{claim}
  \begin{proof}
    As $M(y) = K(y)^{M_n(x)[g \upharpoonright\xi]}$ is an inner model of $M_n(x)[g \upharpoonright \xi]$, every cardinal above $\xi$ in $M_n(x)$ is a cardinal in $M(y)$. Now let $\eta > \xi, \xi^\prime$ be a cutpoint of $M_n(x)$ which is large enough such that in $M(y)$ there is some cutpoint between $\xi^\prime$ and $\eta$. Suppose $\eta$ is not a cutpoint of $M(y)$, say there is an extender $E$ overlapping $\eta$ in $M(y)$. Since there is some cutpoint in $M(y)$ between $\xi^\prime$ and $\eta$, it follows that $\ensuremath{\operatorname{crit}} (E) > \xi^\prime$. Then, as $M_n(x) = K(x)^{M(y)[h \upharpoonright \xi^\prime]}$, by maximality of the core model there is also an extender on the $M_n(x)$-sequence overlapping $\eta$, contradicting the assumption that $\eta$ is a cutpoint of $M_n(x)$.
  \end{proof}

Moreover, Equations \eqref{eq:1} and \eqref{eq:2} yield
\[M(y) \subseteq M_n(x)[g \upharpoonright \xi] \subseteq M(y)[h
  \upharpoonright \zeta],\] where $\xi^\prime < \zeta < \kappa$ is
such that $g \upharpoonright \xi \in M(y)[h \upharpoonright
\zeta]$. By the intermediate model theorem (see for example Lemma
$15.43$ in \cite{Je03}) this implies that
$M_n(x)[g \upharpoonright \xi]$ is a generic extension of $M(y)$ for a
forcing of size less than $\kappa$.\footnote{I.e. $M(y)$ is a ground
  of $M_n(x)[g \upharpoonright \xi]$. See for example \cite{FHR15} or
  \cite{Us17} for an introduction to the theory of grounds.} Since
$M_n(x)[g \upharpoonright \xi]$ is a generic extension of $M_n(x)$ for
a forcing of size less than $\kappa$ as well, this implies by Theorem
$1.3$ in \cite{Us17} that there is some common inner model
$W \subseteq M_n(x) \cap M(y)$ such that
$M_n(x)[g \upharpoonright \xi]$ is a generic extension of $W$ for a
forcing of size less than $\kappa$.

  As every generic extension via a forcing of size less than $\kappa$
  can be absorbed by the collapse of some ordinal $\beta < \kappa$,
  this yields that we can fix some ordinal $\beta < \kappa$ and some
  $\ensuremath{\operatorname{Col}} (\omega,\beta)$-generic $b \in M_n(x)[g]$ over $W$ such that
  $x,y,\mathcal{N},\mathcal{N}^\prime \in W[b]$. Then $M_n(x)$ and $M(y)$ exist in
  $W[b]$ as definable subclasses because
  \[(K(x))^{W[b]} = (K(x))^{M_n(x)[g \upharpoonright \xi]} =
    (K(x))^{M_n(x)} = M_n(x)\] and similarly
  \[(K(y))^{W[b]} = (K(y))^{M_n(x)[g \upharpoonright \xi]} =
    (K(y))^{M_n(x)[g]} = (K(y))^{M(y)[h]}= M(y)\] by generic
  absoluteness of the core model again. Let
  $\dot{x},\dot{y},\dot{\mathcal{N}}$ and $\dot{\mathcal{N}^\prime}$ be
  $\ensuremath{\operatorname{Col}} (\omega,\beta)$-names for $x,y,\mathcal{N}$ and $\mathcal{N}^\prime$ in
  $W$. Moreover, let $p \in \ensuremath{\operatorname{Col}} (\omega,\beta)$ force all properties
  we need about $\dot{x},\dot{y},\dot{\mathcal{N}}$ and
  $\dot{\mathcal{N}^\prime}$. For $q \leq_{\ensuremath{\operatorname{Col}} (\omega,\beta)} p$ let $b_q$ be
  the $\ensuremath{\operatorname{Col}} (\omega,\beta)$-generic filter over $W$ such that
  $\bigcup b_q$ agrees with $q$ on $\ensuremath{\operatorname{dom}}(q)$ and with $\bigcup b$
  everywhere else.

  Now we construct $(\mathcal{M}, t) \in \mathcal{I} \cap
  \mathcal{I}^{M(y)}$. Let $\eta < \kappa$ be a cardinal
  cutpoint of both $M(y)$ and $M_n(x)$ such that
  $\xi, \xi^\prime < \eta$, which exists by Claim \ref{cl:ctpts}. Then
  in fact $(\eta^+)^{M_n(x)} = (\eta^+)^{M(y)}$ as by Equations
  $(\ref{eq:1})$ and $(\ref{eq:2})$ at the beginning of the proof
  \[ (\eta^+)^{M(y)} \leq (\eta^+)^{M_n(x)[g \upharpoonright \xi]} =
    (\eta^+)^{M_n(x)} \leq (\eta^+)^{M(y)[h \upharpoonright
      \xi^\prime]} = (\eta^+)^{M(y)}. \] By the same argument,
  $(\eta^+)^{K(\dot{x}^{b_q})} = (\eta^+)^{K(\dot{y}^{b_q})}$ for all
  $q \leq_{\ensuremath{\operatorname{Col}} (\omega,\beta)} p$.

  Work in $W[b]$. Using Lemmas \ref{lem:pseudocomp} and
  \ref{lem:pseudogenit}, we obtain an inner model $\mathcal{M}$ by
  pseudo-comparing all $(\dot{\mathcal{N}})^{b_q}$ and
  $(\dot{\mathcal{N}^\prime})^{b_q}$ for $q \leq_{\ensuremath{\operatorname{Col}} (\omega,\beta)} p$ and
  simultaneously pseudo-genericity iterating such that
  $K(\dot{x}^{b_q}) | \eta$ and $K(\dot{y}^{b_q}) | \eta$ are generic
  over $\mathcal{M}$ and
  $\delta^\mathcal{M} = (\eta^+)^{K(\dot{x}^{b_q})} =
  (\eta^+)^{K(\dot{y}^{b_q})}$. Since $\mathcal{M}$ is definable in $W[b]$
  from $\{b_q \mid q \leq_{\ensuremath{\operatorname{Col}} (\omega,\beta)} p \}$ and parameters
  from $W$, we have that in fact
  $\mathcal{M} \in W \subseteq M_n(x) \cap M(y)$, as $\mathcal{M}$ does not depend on
  the choice of the generic $b$. Moreover, $\mathcal{M}$ is a correct iterate
  of $\mathcal{N}$ in $M_n(x)$ and a correct iterate of $\mathcal{N}^\prime$ in
  $M(y)$.

  As argued above, we can assume that $\mathcal{N}$ and $\mathcal{N}^\prime$ are
  $t$-iterable in $M_n(x)$ and $M(y)$ respectively for
  $t = s \cup s^\prime$. Therefore $\mathcal{M}$ is $t$-iterable in both,
  $M_n(x)$ and $M(y)$. Hence,
  $(\mathcal{M},t) \in \mathcal{I} \cap \mathcal{I}^{M(y)}$,
  $(\mathcal{N},s) \leq_{\mathcal{I}} (\mathcal{M},t)$, and
  $(\mathcal{N}^\prime, s^\prime) \leq_{\mathcal{I}^{M(y)}} (\mathcal{M},t)$, as
  desired.
\end{proof}

This yields that $\cM_{\infty} \in \ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $.

\section{$\ensuremath{\operatorname{HOD}} $ below $\delta_{\infty}$}\label{sec:dmr}

In this section we will show that $\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $ and $\cM_{\infty}$ agree up to
$\delta_{\infty}$ by generalizing the arguments in Section $3.4$ in
\cite{StW16}. We show a version of Woodin's derived model resemblance for our setting. For this, we do not need to talk about generic extensions such as $M(y)[h]$ and work with $M(y)$ directly instead. Choose for
 any ordinal $\alpha$ an arbitrary $(\mathcal{N},s) \in \mathcal{I}$ such that
 $\alpha \in s$ and let
 $\alpha^* = \pi_{(\mathcal{N},s),\infty}(\alpha)$. Note that the value
 of $\alpha^*$ does not depend on the choice of $(\mathcal{N},s)$. We also let
 $t^* = \{ \alpha^* \mid \alpha \in t \}$ for $t \in [\ensuremath{\operatorname{Ord}} ]^{<\omega}$.

 \begin{lemma}\label{lem:dmr}
   Let $\mathcal{N}$ be an $n$-suitable premouse and $s \in [\ensuremath{\operatorname{Ord}} ]^{<\omega}$
   such that $(\mathcal{N}, s) \in \mathcal{I}$. Let
   $\bar{\xi} < \gamma_s^{\mathcal{N}}$,
   $\xi = \pi_{(\mathcal{N},s),\infty}(\bar{\xi})$ and
   $t \in [\ensuremath{\operatorname{Ord}} ]^{<\omega}$. Moreover, let $\varphi(v_0,v_1)$ be a
   formula in the language of premice, i.e., we allow the extender sequence as a predicate. Then the following are equivalent.
  \begin{enumerate}[$(a)$]
  \item $M_n(\cM_{\infty} | \delta_{\infty}) \vDash \varphi(\xi, t^*)$,
  \item in $M_n(x)[g]$, there is some dlm-suitable $y \in {}^\omega\omega$
    witnessed by $M(y)$ with $(\mathcal{N},s) \in \mathcal{I}^{M(y)}$ and a correctly guided
    finite stack on $\mathcal{N}$ with last model $\mathcal{M} \in M(y)$ such that
    whenever $\mathcal{R} \in \mathcal{G}^{M(y)}$ is the last model of a
    correctly guided finite stack on $\mathcal{M}$, then
    $\mathcal{P}^{M(y)}(\mathcal{R}|\delta^\mathcal{R}) \vDash \varphi(\pi^{M(y)}_{(\mathcal{N},s),(\mathcal{R},s)}(\bar{\xi}), t)$.
  \end{enumerate}
\end{lemma}

\begin{proof}
  To prove that $(a)$ implies $(b)$ we assume toward a contradiction
  that $(b)$ is false. So in $M_n(x)[g]$ for all dlm-suitable $y \in {}^\omega\omega$ and $M(y)$
  witnessing this with $(\mathcal{N}, s) \in \mathcal{I}^{M(y)}$ and all correctly guided finite
  stacks on $\mathcal{N}$ with last model $\mathcal{M} \in M(y)$, there is a correctly
  guided finite stack on $\mathcal{M}$ with last model
  $\mathcal{R} \in \mathcal{G}^{M(y)}$ such that
  $\mathcal{P}^{M(y)}(\mathcal{R}|\delta^\mathcal{R}) \vDash \neg \varphi(\pi^{M(y)}_{(\mathcal{N},s),(\mathcal{R},s)}(\bar{\xi}), t)$.

  We can assume without loss of generality that $\mathcal{N} \in M_n(x)$ is
  the last model of a correctly guided finite stack on $M_{n+1}^-$ via
  the canonical iteration strategy $\Sigma_{M_{n+1}^-}$ and strongly
  $s$-iterable below $\kappa$ with respect to branches choosen by
  $\Sigma_{M_{n+1}^-}$. Moreover, we can assume that $max(s)$ is a uniform indiscernible. If this is not already the case, we replace $\mathcal{N}$ by a
  pseudo-iterate of the result of the pseudo-comparison of $\mathcal{N}$ with
  $M_{n+1}^-$ using Lemma \ref{lem:pseudocomp} and Corollary
  \ref{cor:itintoG}.

  \begin{claim}
    There are $n$-suitable premice $\mathcal{N}_k \in \mathcal{F}^+$ for
    $k < \omega$ which are cofinal in $\mathcal{F}^+$ such that
    $\mathcal{N}_0 = \mathcal{N}$ and for all $k<\omega$,
    \[ M_n(\mathcal{N}_k|\delta^{\mathcal{N}_k}) \vDash \neg\varphi(\bar{\xi}_k,t), \] where
    $\bar{\xi}_k = i_{\mathcal{N}_0,\mathcal{N}_k}(\bar{\xi})$ is the image of
    $\bar{\xi}$ under the iteration map induced by
    $\Sigma_{M_{n+1}^-}$.
  \end{claim}
  \begin{proof} Let $(\mathcal{Q}_i \mid i < \omega)$ be an enumeration of
    $\mathcal{F}^+$ and $\mathcal{N}_0 = \mathcal{N}$. Then we construct $\mathcal{N}_{k+1}$
    inductively. So assume that we already constructed $\mathcal{N}_k$ and
    pseudo-coiterate $\mathcal{N}_k$ with $\mathcal{Q}_k$ to some model $\mathcal{N}_k^*$ (see
    Lemma \ref{lem:pseudocomp}). By assumption $(b)$ is false, so let
    $\mathcal{R}$ be a counterexample witnessing this for $\mathcal{N}_k^*$ and the
    dlm-suitable premouse $M_n(x)$. That means $\mathcal{R} \in \mathcal{G}$ is
    the last model of a correctly guided finite stack on $\mathcal{N}_k^*$
    such that
    $M_n(\mathcal{R}|\delta^\mathcal{R}) = \mathcal{P}^{M_n(x)}(\mathcal{R}|\delta^\mathcal{R}) \vDash \neg \varphi(i_{\mathcal{N},\mathcal{R}}(\bar{\xi}),t)$ as
    $i_{\mathcal{N},\mathcal{R}} \upharpoonright H_s^{\mathcal{N}} =
    \pi_{(\mathcal{N},s),(\mathcal{R},s)}$. But $\mathcal{R} \in \mathcal{F}^+$ since
    $\mathcal{R} \in \mathcal{G}$ and it is a correct iterate of $\mathcal{Q}_k$. Thus
    we can let $\mathcal{N}_{k+1} = \mathcal{R}$.
  \end{proof}

  Since $(\mathcal{N}_k \mid k < \omega)$ is cofinal in
  $\mathcal{F}^+$, it follows that the direct limit of
  $(\mathcal{N}_k, i_{\mathcal{N}_k,\mathcal{N}_l} \mid k<l<\omega)$ is equal to $\cM_{\infty}^+$. Let
  $\hat{\mathcal{N}_k} = M_n(\mathcal{N}_k | \delta^{\mathcal{N}_k})$ and let
  $\hat{i}_{\hat{\mathcal{N}}_k,\infty} : \hat{\mathcal{N}_k} \rightarrow M_n(\cM_{\infty}^+ |
  \delta^{\cM_{\infty}^+}) = \hat{\cM}_{\infty}^+$ be the corresponding extension of the
  direct limit map $i_{\mathcal{N}_k, \infty}$. Then we have for all sufficiently large $k$ that
  \[ M_n(\cM_{\infty}^+ | \delta^{\cM_{\infty}^+}) \vDash \neg\varphi(i_{\mathcal{N}_k,
      \infty}(\bar{\xi}_k),
    \hat{i}_{\hat{\mathcal{N}}_k,\infty}[t]). \] Since we assumed
  that $\mathcal{N}$ is strongly $s$-iterable below $\kappa$ with respect to
  branches choosen by $\Sigma_{M_{n+1}^-}$ and
  $\bar{\xi} < \gamma_s^{\mathcal{N}}$, it follows that
  $i_{\mathcal{N}_k, \infty}(\bar{\xi}_k) = i_{\mathcal{N},\infty}(\bar{\xi}) =
  \pi_{(\mathcal{N},s),\infty}(\bar{\xi}) = \xi$ as
  $\bar{\xi}_k = i_{\mathcal{N},\mathcal{N}_k}(\bar{\xi})$.

  Let $k<\omega$ be large enough such that
  $(\mathcal{N}_k, s \cup t) \in \mathcal{I}$ and
  $\hat{i}_{\hat{\mathcal{N}}_l,\hat{\mathcal{N}}_{l+1}}(s) = s$ for all $l \geq
  k$. Such a $k$ exists by a so-called bad sequence argument similar
  to the one in the proof of Lemma $5.8$ in \cite{Sa13}. For $l \geq k$ and $s^- = s \setminus \{max(s)\}$, let
 \[ \gamma_s^{\hat{\mathcal{N}}_l} = \sup(Hull_1^{\hat{\mathcal{N}}_l |
     max(s)}(s^-) \cap \delta^{\mathcal{N}_l}), \] and
 \[ H_s^{\hat{\mathcal{N}}_l} = Hull_1^{\hat{\mathcal{N}}_l | max(s)}(\gamma_s^{\hat{\mathcal{N}}_l}
   \cup s^-). \] Now we let for $l < j$,
 $\hat{\pi}_{(\mathcal{N}_l,s),(\mathcal{N}_j,t)} : H_s^{\hat{\mathcal{N}}_l} \rightarrow
 H_t^{\hat{\mathcal{N}}_j}$ denote the canonical corresponding embedding extending $\pi_{(\mathcal{N}_l,s^-),(\mathcal{N}_j,t^-)}$ given by the iteration embedding via a tail of the iteration strategy $\Sigma_{M_{n+1}}$. Let $\hat{\cM}_{\infty}$ be the direct limit under these embeddings and let $\hat{\pi}_{(\mathcal{N}_l,s),\infty} : H_s^{\hat{\mathcal{N}}_l} \rightarrow \hat{\cM}_{\infty}$
 for $l \geq k$ denote the direct limit embedding.

 Now consider the map
  \[ \hat{\sigma}: \hat{\cM}_{\infty} \rightarrow \hat{\cM}_{\infty}^+ =
    M_n(\cM_{\infty}^+|\delta^{\cM_{\infty}^+}) \] which is the canonical extension of
  the map $\sigma: \cM_{\infty} \rightarrow \cM_{\infty}^+$ defined in the proof of
  Lemma \ref{lem:dlmeqdlmplus}, i.e., for $x \in \hat{\cM}_{\infty}$, say
  $x = \hat{\pi}_{(\mathcal{N}_l,s),\infty}(\bar{x})$ for some
  $\bar{x} \in H_s^{\hat{\mathcal{N}}_l}$ and $k \leq l < \omega$, let
  $\hat{\sigma}(x) = \hat{i}_{\hat{\mathcal{N}}_l,\infty}(\bar{x})$. Then it
  follows as in the proof of Lemma 5.10 in \cite{Sa13} that
  $\hat{\sigma} = \ensuremath{\operatorname{id}}$ and $\hat{\cM}_{\infty} = M_n(\cM_{\infty}|\delta_{\infty})$. Moreover, we have that
  $\hat{\sigma}[t^*] = \hat{\sigma}(\hat{\pi}_{(\mathcal{N}_k,s \cup
    t),\infty}[t]) = \hat{i}_{\hat{\mathcal{N}}_k,\infty}[t]$. Therefore
  pulling back under $\hat{\sigma}$ yields that
  \[ M_n(\cM_{\infty} | \delta_{\infty}) \vDash \neg\varphi(\xi,t^*). \] This is the desired
  contradiction to $(a)$.

  To show that $(b)$ implies $(a)$ we now assume that $(b)$ is
  true. Let $M(y)$ be the dlm-suitable premouse with $(\mathcal{N},s) \in \mathcal{I}^{M(y)}$
  given by $(b)$. As before we can assume without loss of generality
  that $\mathcal{N}$ is the last model of a correctly guided finite stack on
  $M_{n+1}^-$ via the canonical iteration strategy
  $\Sigma_{M_{n+1}^-}$, that $\mathcal{N}$ is strongly $s$-iterable below $\kappa$ with
  respect to branches choosen by $\Sigma_{M_{n+1}^-}$, that $max(s)$ is a uniform indiscernible, and that
  $\mathcal{N} \in \mathcal{G} \cap \mathcal{G}^{M(y)}$ using Lemma \ref{lem:dlmM(y)eq}.

  \begin{claim}
    There are $n$-suitable premice $\mathcal{N}_k \in \mathcal{F}^+$ for
    $k < \omega$ which are cofinal in $\mathcal{F}^+$ such that
    $\mathcal{N}_0 = \mathcal{N}$ and for all $k<\omega$,
    \[ M_n(\mathcal{N}_k|\delta^{\mathcal{N}_k}) \vDash \varphi(\bar{\xi}_k,t), \] where
    $\bar{\xi}_k = i_{\mathcal{N}_0,\mathcal{N}_k}(\bar{\xi})$ is the image of
    $\bar{\xi}$ under the iteration map induced by $\Sigma_{M_{n+1}^-}$.
  \end{claim}

  \begin{proof}
    By the proof of Lemma \ref{lem:dlmM(y)eq}, we can pick a sequence $(\mathcal{Q}_i \mid i < \omega)$ of premice cofinal in $\mathcal{F}^+$ such that $\mathcal{Q}_i \in \mathcal{F}^{M(y)}$ for all $i < \omega$. Let $\mathcal{N}_0 = \mathcal{N}$ and construct $\mathcal{N}_{k+1} \in M(y)$
    inductively. Assume that we already constructed $\mathcal{N}_k$ and let
    $\mathcal{M} \in M(y)$ be the last model of a correctly guided finite stack on
    $\mathcal{N}$ witnessing that $(b)$ is true. Simultaneously
    pseudo-coiterate $\mathcal{M}$ with $\mathcal{N}_k$ and $\mathcal{Q}_k$ to some premouse
    $\mathcal{N}_k^*$. Using genericity iterations and Lemma
    \ref{lem:dlmM(y)eq}, there is a pseudo-iterate $\mathcal{R}$ of $\mathcal{N}_k^*$
    such that $\mathcal{R} \in \mathcal{G} \cap \mathcal{G}^{M(y)}$ (see also
    Corollary \ref{cor:itintoG}). In particular, we have by dlm-suitability of
    $M(y)$ that
    \begin{align*}
      \mathcal{P}^{M(y)}(\mathcal{R}|\delta^\mathcal{R}) & = K^{M_n(x)[g]}(\mathcal{R}|\delta^\mathcal{R}) = K^{M_n(\mathcal{R}|\delta^\mathcal{R})[G][g]}(\mathcal{R}|\delta^\mathcal{R}) \\ & = K^{M_n(\mathcal{R}|\delta^\mathcal{R})}(\mathcal{R}|\delta^\mathcal{R}) = M_n(\mathcal{R}|\delta^\mathcal{R})
    \end{align*}
    for some $G$ generic over $M_n(\mathcal{R}|\delta^\mathcal{R})$ for the extender algebra and therefore
    $M_n(\mathcal{R}|\delta^\mathcal{R}) \vDash \varphi(i_{\mathcal{N},\mathcal{R}}(\bar{\xi}),t)$ using
    $(b)$ as
    $i_{\mathcal{N},\mathcal{R}}(\bar{\xi}) = \pi_{(\mathcal{N},s),(\mathcal{R},s)}(\bar{\xi}) =
    \pi^{M(y)}_{(\mathcal{N},s),(\mathcal{R},s)}(\bar{\xi})$. Moreover, $\mathcal{R}$ is the last model of a
    correctly guided finite stack on $\mathcal{Q}_k$ and thus
    $\mathcal{R} \in \mathcal{F}^+$, so we can let $\mathcal{N}_{k+1} = \mathcal{R}$.
  \end{proof}

  As before we can use this claim to obtain that
  \[ M_n(\cM_{\infty} | \delta_{\infty}) \vDash \varphi(\xi,t^*), \] which proves $(a)$.
\end{proof}

Let $\kappa_\infty$ be the least inaccessible cardinal above $\delta_{\infty}$ in $\hat{\cM}_{\infty} = M_n(\cM_{\infty}|\delta_{\infty})$ and fix some $H$ which is $\ensuremath{\operatorname{Col}} (\omega, {<}\kappa_\infty)$-generic over $\hat{\cM}_{\infty}$. Then Lemma \ref{lem:dmr} implies for example that $\hat{\cM}_{\infty}[H]$ and $M_n(x)[g]$ are elementary equivalent (for formulae in the language of set theory) as for $\mathcal{R}$ as in the statement of Lemma \ref{lem:dmr}, there is some $\ensuremath{\operatorname{Col}} (\omega, {<}\kappa^\mathcal{R})$-generic $G$, where $\kappa^\mathcal{R}$ is the least inaccessible cardinal above $\delta^\mathcal{R}$ in $\mathcal{P}^{M(y)}(\mathcal{R}|\delta^\mathcal{R})$, such that $\mathcal{P}^{M(y)}(\mathcal{R}|\delta^\mathcal{R})[G] = M_n(x)[g]$.

We defined a direct limit system $\mathcal{F}^{M(y)}$ for all dlm-suitable $M(y)$ in $M_n(x)[g]$. Therefore, there is a direct limit system $\mathcal{F}^{*, M(y)}$ with the same properties for each dlm-suitable $M(y)$ in $\hat{\cM}_{\infty}[H]$ (adapting the definition of dlm-suitable to $\hat{\cM}_{\infty}[H]$). It is easy to see that Lemma \ref{lem:dmr} implies that $\cM_{\infty}$ is strongly $s^*$-iterable in all dlm-suitable $M(y)$ in $\hat{\cM}_{\infty}[H]$ for all $s \in [\ensuremath{\operatorname{Ord}} ]^{<\omega}$. So we
can consider its direct limit embedding
\[ \pi_\infty^{M(y)} = \bigcup \{ (\pi_{(\cM_{\infty},s^*),\infty}^{M(y)})^{\mathcal{F}^{*, M(y)}}
  \mid s \in [\ensuremath{\operatorname{Ord}} ]^{<\omega}\} \] in the system $\mathcal{F}^{*, M(y)}$. But in fact, $\pi_\infty^{M(y)} = \pi_\infty^{M(z)}$ for two dlm-suitable models $M(y)$ and $M(z)$, so we call this unique embedding $\pi_\infty$.

\begin{lemma}\label{lem:piinftyid}
  For all $\eta < \delta_{\infty}$ we have that $\pi_\infty(\eta) = \eta^*$.
\end{lemma}

\begin{proof}
  This is again a consequence of Lemma
  \ref{lem:dmr}. Consider the dlm-suitable premouse $M_n(x)$. Let
  $\eta = \pi_{(\mathcal{N},s),\infty}(\bar{\eta})$ for some
  $(\mathcal{N},s) \in \mathcal{I}$ and $\bar{\eta} < \gamma_s^{\mathcal{N}}$ and
  consider the formula
  \begin{align*}
    \varphi(&v_0,v_1,v_2,v_3) = \text{``}1 \forces{}{\ensuremath{\operatorname{Col}} (\omega,{<}\kappa^*)} \text{for all dlm-suitable } y \text{ with } v_0 \in \mathcal{G}^{M(y)}, \\ &
    \text{we have } (v_0,v_1) \in \mathcal{I}^{M(y)}, v_2 <
    \gamma_{v_1}^{v_0, M(y)}, \text{ and }
    \pi_{(v_0,v_1),\infty}^{M(y)}(v_2) = v_3\text{''},
  \end{align*}
  where $\kappa^*$ refers to the least inaccessible cardinal above the least Woodin cardinal of the current model. Recall that for any dlm-suitable $y$ and $z$ witnessed by $M(y)$ and $M(z)$, for any $(\mathcal{N},s), (\mathcal{M},t) \in \mathcal{I}^{M(y)} \cap \mathcal{I}^{M(z)}$ with $(\mathcal{N},s) \leq_{\mathcal{I}^{M(y)}} (\mathcal{M},t)$ and $(\mathcal{N},s) \leq_{\mathcal{I}^{M(z)}} (\mathcal{M},t)$ the induced embeddings $\pi_{(\mathcal{N},s),(\mathcal{M},t)}^{M(y)}$ and $\pi_{(\mathcal{N},s),(\mathcal{M},t)}^{M(z)}$ agree. Hence, in $M_n(x)[g]$, we have for every $\mathcal{R} \in \mathcal{G}$ which is the last model
  of a correctly guided finite stack on $\mathcal{N}$ that for all dlm-suitable $y$ such that $\mathcal{R} \in \mathcal{G}^{M(y)}$, in fact $(\mathcal{R},s) \in \mathcal{I}^{M(y)}$, $\pi_{(\mathcal{N},s),(\mathcal{R},s)}(\bar{\eta}) < \gamma_{s}^{\mathcal{R}, M(y)}$, and $\pi_{(\mathcal{R},s),\infty}^{M(y)}(\pi_{(\mathcal{N},s),(\mathcal{R},s)}(\bar{\eta})) = \eta$. Therefore,
  $\mathcal{P}^{M(y)}(\mathcal{R}|\delta^{\mathcal{R}}) \vDash \varphi(\mathcal{R}, s,
  \pi_{(\mathcal{N},s),(\mathcal{R},s)}(\bar{\eta}), \eta)$. So Lemma \ref{lem:dmr}
  yields that $\hat{\cM}_{\infty} \vDash \varphi(\cM_{\infty}, s^*, \eta, \eta^*)$. So in $\hat{\cM}_{\infty}[H]$, for all dlm-suitable $y$, we have $(\pi^{M(y)}_{(\cM_{\infty},s^*),\infty})^{\mathcal{F}^*, M(y)}(\eta) = \eta^*$, as desired.
\end{proof}

\begin{thm}\label{thm:HODuptoDelta}
  $V_{\delta_{\infty}}^{\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} } = V_{\delta_{\infty}}^{\cM_{\infty}}$.
\end{thm}

\begin{proof}
  By the internal definition of $\cM_{\infty}$ from Lemma \ref{lem:dlmM(y)eq}
  we have that
  $V_{\delta_{\infty}}^{\cM_{\infty}} \subseteq V_{\delta_{\infty}}^{\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} }$. For the
  other inclusion we first show the following claim.
\begin{claim}\label{cl:*}
  $\pi_\infty \upharpoonright \alpha \in \hat{\cM}_{\infty}$ for all
  $\alpha < \delta_{\infty}$.
\end{claim}

\begin{proof}
  As $\alpha < \delta_{\infty}$, there exists an $s \in [\ensuremath{\operatorname{Ord}} ]^{<\omega}$ such
  that for all dlm-suitable $M(y)$ in $\hat{\cM}_{\infty}[H]$, $\alpha < \gamma_{s^*}^{\cM_{\infty}, M(y)}$. For any such $s$ and $M(y)$ we have by definition that
  $\pi_\infty \upharpoonright \alpha =
  (\pi^{M(y)}_{(\cM_{\infty},s^*),\infty})^{\mathcal{F}^*, M(y)} \upharpoonright
  \alpha$. Therefore $\pi_\infty \upharpoonright \alpha \in
  \ensuremath{\operatorname{HOD}} ^{\hat{\cM}_{\infty}[H]}_{\cM_{\infty}}$ and thus
  $\pi_\infty \upharpoonright \alpha \in \hat{\cM}_{\infty}$ by homogeneity of
  the forcing $\mathbb{P} = \ensuremath{\operatorname{Col}} (\omega, {<}\kappa_\infty)$.
\end{proof}
Now let $A \in V_{\delta_{\infty}}^{\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} }$ be arbitrary. Let
$\alpha < \delta_{\infty}$ be such that $A \subset \alpha$ is defined over
$M_n(x)[g]$ by a formula $\varphi$ with ordinal parameters from
$t \in [\ensuremath{\operatorname{Ord}} ]^{<\omega}$ and let $\beta < \alpha$ be arbitrary. That
means $\beta \in A$ iff $M_n(x)[g] \vDash \varphi(\beta,t)$. Lemma \ref{lem:dmr} yields that this is
the case iff $\hat{\cM}_{\infty}[H] \vDash \varphi(\beta^*, t^*)$. Since
$\beta < \alpha < \delta_{\infty}$, we have that
$\beta^* = \pi_\infty(\beta)$ by Lemma \ref{lem:piinftyid}. Moreover,
we have by Claim \ref{cl:*} that
$\pi_\infty \upharpoonright \alpha \in \hat{\cM}_{\infty}$. Therefore, it follows
by homogeneity of the forcing
$\mathbb{P} = \ensuremath{\operatorname{Col}} (\omega, {<}\kappa_\infty)$ that $A \in \hat{\cM}_{\infty}$
since $t^*$ is a fixed parameter in $\hat{\cM}_{\infty}$. Thus
$A \in V_{\delta_{\infty}}^{\cM_{\infty}}$, as desired.
\end{proof}

\section{The full $\ensuremath{\operatorname{HOD}} $ in $M_n(x)[g]$}\label{sec:fullHOD}

To compute the full model $\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $, i.e., prove Theorem
\ref{thm:main}, we first show the following lemma.

\begin{lemma}\label{lem:HODeqMn(A)}
  $\ensuremath{\operatorname{HOD}^{M_n(x)[g]}}  = M_n(A)$ for some set $A \subseteq \omega_2^{M_n(x)[g]}$ with $A \in \ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $.
\end{lemma}

\begin{proof}
  Let $\mathbb{V}$ denote the Vop\v{e}nka algebra in $M_n(x)[g]$ for making a
  real generic over $\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $. By Vop\v{e}nka's theorem (see for example Theorem $15.46$ in \cite{Je03} or Theorem $9.0.1$ in
  \cite{La17}) there is a $\mathbb{V}$-generic $G_x$ over $\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $
  such that $x \in \ensuremath{\operatorname{HOD}^{M_n(x)[g]}} [G_x]$ and in fact
  $\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} [G_x] = \ensuremath{\operatorname{HOD}^{M_n(x)[g]}} _x$.

  \begin{claim}
    There is some $\tilde\mathbb{V} \in \ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $ which is isomorphic to $\mathbb{V}$ and a subset of $\omega_2^{M_n(x)[g]}$.
  \end{claim}

  \begin{proof}
    Work in $M_n(x)[g]$. Each real, i.e., element of $\mathcal{P}(\omega)$, can be coded by a countable ordinal and each set of reals can be coded by an ordinal $< \omega_2$. Forcing with the Vop\v{e}nka algebra $\mathbb{V}$ is $\omega_2$-c.c. in $M_n(x)[g]$ as otherwise there would be an $\omega_2$ sequence of pairwise distinct non-empty sets of reals, contradicting $\ensuremath{\operatorname{CH}} $. The Vop\v{e}nka algebra is in $\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $ and when considering $\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} [G_x]$ cardinals $\geq (\kappa^+)^{M_n(x)}$ are preserved. Since $(\kappa^{+\omega})^{M_n(x)}$ is below the least measurable cardinal of $M_n(x)$, $M_n(x)|(\kappa^{+\omega})^{M_n(x)}$ can be written as the $Lp^n$-stack of height $(\kappa^{+\omega})^{M_n(x)}$ above $x$ and is therefore by the argument in Lemma \ref{lem:closureSn} an element of $\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} _x = \ensuremath{\operatorname{HOD}^{M_n(x)[g]}} [G_x]$. But the Vop\v{e}nka algebra is a subset of some ordinal $\alpha < (\kappa^{++})^{M_n(x)} = (\kappa^{++})^{\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} [G_x]} = (\kappa^{++})^{\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} }$, so there is some $\tilde\mathbb{V} \in \ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $ which is isomorphic to $\mathbb{V}$ and a subset of $(\kappa^+)^{M_n(x)}$.
  \end{proof}

  For the rest of this proof we write $\mathbb{V}$ for the $\tilde\mathbb{V}$ from the previous claim and show that $M_n(\mathbb{V}) = \ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $.

  \begin{claim}
    $G_x$ is $\mathbb{V}$-generic over $M_n(\mathbb{V})$.
  \end{claim}

  \begin{proof}
    The dense sets in question are elements of $\mathcal{P}(\mathbb{V})^{M_n(\mathbb{V})}$ and hence elements of $Lp^n(\mathbb{V}) = \bigcup \{N \, | \, N \text{ is a countable } \mathbb{V}\text{-premouse with } \rho_\omega(N) = \mathbb{V} \text{ which is } n\text{-small, sound, and }(\omega,\omega_1,\omega_1)\text{-iterable}\}$. As $\mathbb{V} \in \ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $, Lemma \ref{lem:closureSn} yields that $Lp^n(\mathbb{V}) \in \ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $, which implies the claim.
  \end{proof}

  \begin{claim}\label{cl:sameleastmeas}\label{cl:1-}
    $M_n(x)$ and $M_n(\mathbb{V})[G_x]$ have the same least measurable cardinal $\kappa_0$. Moreover, $V_{\kappa_0}^{M_n(x)} = V_{\kappa_0}^{M_n(\mathbb{V})[G_x]}$.
  \end{claim}
  \begin{proof}
    Write $\kappa_0^{M_n(x)}$ and $\kappa_0^{M_n(\mathbb{V})}$ for the least measurable cardinal of $M_n(x)$ and $M_n(\mathbb{V})$ respectively. $M_n(\mathbb{V})$ and $M_n(\mathbb{V})[G_x]$ have the same least measurable cardinal. The proof of Lemma \ref{lem:closureSn} shows that $Lp^n(z) \in M_n(\mathbb{V})[G_x]$ for any $z \in V_{\delta_0}^{M_n(\mathbb{V})[G_x]}$, where $\delta_0$ denotes the least Woodin cardinal in $M_n(\mathbb{V})[G_x]$. As $M_n(x)|\kappa_0^{M_n(x)}$ is equal to the $Lp^n$-stack of height $\kappa_0^{M_n(x)}$ over $x$, it follows that $M_n(x)|\kappa_0^{M_n(x)} \subseteq M_n(\mathbb{V})[G_x]$. Analogously, $M_n(\mathbb{V})|\kappa_0^{M_n(\mathbb{V})} \subseteq M_n(x)$ and in fact $M_n(\mathbb{V})[G_x]|\kappa_0^{M_n(\mathbb{V})} \subseteq M_n(x)$.

      Suppose $\kappa_0^{M_n(\mathbb{V})} < \kappa_0^{M_n(x)}$ and let $\mathcal{U}$ be the measure on $\kappa_0^{M_n(\mathbb{V})}$ in $M_n(\mathbb{V})$ (which we identify with the lift of this measure to $M_n(\mathbb{V})[G_x]$). In particular, $\mathcal{U}$ measures all subsets of $\kappa_0^{M_n(\mathbb{V})}$ in $M_n(x)$ as well and $\kappa_0^{M_n(\mathbb{V})}$ is a cardinal in $M_n(x)$ because otherwise the function witnessing this would be an element of $M_n(x)|\kappa_0^{M_n(x)}$ and hence in $M_n(\mathbb{V})[G_x]$. So \[ V_{\kappa_0^{M_n(\mathbb{V})}}^{M_n(\mathbb{V})[G_x]} = V_{\kappa_0^{M_n(\mathbb{V})}}^{M_n(x)}. \] Now $M_n(x)|(\kappa_0^{M_n(\mathbb{V})})^+ = Lp^n(M_n(x)|\kappa_0^{M_n(\mathbb{V})})$ and hence it contains a mouse with the measure $\mathcal{U}$ on $\kappa_0^{M_n(\mathbb{V})}$. This contradicts the fact that $\kappa_0^{M_n(x)}$ is the least measurable cardinal in $M_n(x)$. The argument in the case $\kappa_0^{M_n(\mathbb{V})} > \kappa_0^{M_n(x)}$ is analogous. Therefore, $M_n(x)$ and $M_n(\mathbb{V})[G_x]$ have the same least measurable cardinal $\kappa_0$ and the argument above shows $V_{\kappa_0}^{M_n(x)} = V_{\kappa_0}^{M_n(\mathbb{V})[G_x]}$.
  \end{proof}

  For what follows, it suffices to work with the least inaccessible $\lambda < \kappa_0$ of $M_n(x)$ which is above $\kappa$, so we restrict ourselves to this situation.

  \begin{claim}\label{cl:0}
    $V_\lambda^{M_n(\mathbb{V})} \subseteq \ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $.
  \end{claim}
  \begin{proof}
    This follows from the proof of Lemma \ref{lem:closureSn} as $M_n(\mathbb{V})|\lambda$ can be obtained as the $Lp^n$-stack of height $\lambda$ over $\mathbb{V}$ and $\mathbb{V} \in \ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $.
  \end{proof}

  Now we can show that the lemma holds below $\lambda$.

  \begin{claim}\label{cl:HODagreementuptolambda}
    $V_\lambda^{M_n(\mathbb{V})} = V_\lambda^{\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} }$.
  \end{claim}

  \begin{proof}
    We first show that $V_\lambda^{M_n(\mathbb{V})}[G_x] =
    V_\lambda^{\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} }[G_x]$. The inclusion $\subseteq$ follows from Claim
    \ref{cl:0}. For the other inclusion we have that
    \[\ensuremath{\operatorname{HOD}} ^{M_n(x)[g]}[G_x] = \ensuremath{\operatorname{HOD}} _x^{M_n(x)[g]} \subseteq
    \ensuremath{\operatorname{HOD}} _x^{M_n(x)} \subseteq M_n(x), \] using
    the homogeneity and ordinal definability of the forcing
    $\ensuremath{\operatorname{Col}} (\omega, {<}\kappa)$. Therefore by Claim \ref{cl:1-}
    \[V_\lambda^{\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} }[G_x] \subseteq V_\lambda^{M_n(x)} = V_\lambda^{M_n(\mathbb{V})}[G_x]. \] Finally, we argue that the equality
    $V_\lambda^{M_n(\mathbb{V})}[G_x] = V_\lambda^{\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} }[G_x]$ also holds true
    without adding the generic $G_x$. As by Claim \ref{cl:0} we have
    $V_\lambda^{M_n(\mathbb{V})} \subseteq V_\lambda^{\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} }$, we are again left
    with proving the other inclusion. Let $\mathbb{P} = \mathbb{V} \times \ensuremath{\operatorname{Col}} (\omega,{<}\kappa)$.
    Then $(G_x,g)$ is
    $\mathbb{P}$-generic over both $V_\lambda^{M_n(\mathbb{V})}$ and $V_\lambda^{\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} }$,
    and $V_\lambda^{M_n(\mathbb{V})}[G_x,g] = V_\lambda^{\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} }[G_x,g]$. Let
    $a \in V_\lambda^{\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} }$ be a set of ordinals. Then there is a
    $\mathbb{P}$-name $\sigma \in V_\lambda^{M_n(\mathbb{V})}$ such that
    $\sigma_{(G_x,g)} = a$. This is forced over $V_\lambda^{\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} }$,
    i.e., there is a $p \in \mathbb{P}$ such that
    $V_\lambda^{\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} } \vDash \text{``}p \forces{}{} \sigma =
    \check{a}$''. Thus $V_\lambda^{M_n(\mathbb{V})}$ can compute the elements of
    $a$ using the forcing relation for $\mathbb{P}$ below $p$. Hence
    $a \in V_\lambda^{M_n(\mathbb{V})}$, as desired.
  \end{proof}

  Now we are able to extend Claim \ref{cl:1-} to the full models.

  \begin{claim}\label{cl:1}
    $M_n(\mathbb{V})[G_x] = M_n(x)$.
  \end{claim}
  \begin{proof}
    Consider $M_n(x)[g]$ as a $V_\lambda^{M_n(x)[g]}$-premouse and note that it equals $M_n(V_\lambda^{M_n(x)[g]})$. We use $\mathcal{P}^{M_n(x)[g]}(M_n(\mathbb{V})|\lambda)$ to denote the result of
    a $\mathcal{P}$-construction in the sense of \cite{SchSt09} above
    $M_n(\mathbb{V})|\lambda$ inside the $V_\lambda^{M_n(x)[g]}$-premouse $M_n(x)[g]$. By Claim
    \ref{cl:1-}, $V_\lambda^{M_n(\mathbb{V})}[G_x] = V_\lambda^{M_n(x)}$, so
    $V_\lambda^{M_n(\mathbb{V})}[G_x][g] = V_\lambda^{M_n(x)[g]}$ and this
    $\mathcal{P}$-construction is well-defined. Moreover, the following
    argument shows that the construction never projects across
    $\lambda$.

    Assume toward a contradiction that there is a level $\mathcal{P}$ of the
    $\mathcal{P}$-construction above $M_n(\mathbb{V})|\lambda$ inside $M_n(x)[g]$ such
    that $\rho_\omega(\mathcal{P}) = \rho < \lambda$. That means there is an
    $r\Sigma_{k+1}(\mathcal{P})$-definable set $a \subseteq \rho$ for some
    $k < \omega$ such that $a \notin \mathcal{P}$. As by the proof of Claim
    \ref{cl:0}, $M_n(\mathbb{V})|\lambda \in \ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $ it follows by
    definability of the $\mathcal{P}$-construction and of the extender
    sequence of $M_n(V_\lambda^{M_n(x)[g]})$ (see Lemma $1.1$ in \cite{Sch06} due to J. Steel) that
    $\mathcal{P} \in \ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $. This means that in particular $a \in
    \ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $. But $a \subseteq \rho < \lambda$ and by Claim
    \ref{cl:HODagreementuptolambda},
    $V_\lambda^{\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} } = V_\lambda^{M_n(\mathbb{V})} = V_\lambda^\mathcal{P}$, so
    $a \in \mathcal{P}$. Contradiction.

    Now it follows by construction (see \cite{SchSt09}) that
    \[\mathcal{P}^{M_n(x)[g]}(M_n(\mathbb{V})|\lambda)[G_x][g] = M_n(x)[g].\] But this
    yields that $\mathcal{P}^{M_n(x)[g]}(M_n(\mathbb{V})|\lambda)[G_x] = M_n(x)$,
    without adding the generic $g$, by an argument as the one at the end of
    the previous claim. Moreover,
    $\mathcal{P}^{M_n(x)[g]}(M_n(\mathbb{V})|\lambda) = M_n(\mathbb{V})$ and thus
    $M_n(\mathbb{V})[G_x] = M_n(x)$, as desired.
  \end{proof}

  This argument also shows the following claim.

  \begin{claim}\label{cl:0+}
     $M_n(\mathbb{V}) \subseteq \ensuremath{\operatorname{HOD}} ^{M_n(x)[g]}$.
   \end{claim}

  Now, the next claim follows from the first half of the proof of Claim \ref{cl:HODagreementuptolambda}.

  \begin{claim}\label{cl:2}
    $M_n(\mathbb{V})[G_x] = \ensuremath{\operatorname{HOD}} ^{M_n(x)[g]}[G_x]$.
  \end{claim}

  Finally, the statement of Claim \ref{cl:2} also holds true without
  adding the generic $G_x$ by the argument at the end of the proof of
  Claim \ref{cl:HODagreementuptolambda}. Hence
  $M_n(\mathbb{V}) = \ensuremath{\operatorname{HOD}} ^{M_n(x)[g]}$, as desired.
\end{proof}

\begin{cor}\label{cor:HODF}
  Let $F(s) = s^*$ for $s \in [\ensuremath{\operatorname{Ord}} ]^{<\omega}$. Then
  \[\ensuremath{\operatorname{HOD}^{M_n(x)[g]}}  = M_n(\cM_{\infty}|\delta_{\infty}, F \upharpoonright
    \delta_{\infty}). \]
\end{cor}

\begin{proof}
  Note that $\cM_{\infty}|\delta_{\infty}$ and $F \upharpoonright \delta_{\infty}$ are elements of $\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $ by construction. Let $\eta = \sup F \, " \delta_{\infty}$ and let $\gamma$ be the least inaccessible cardinal of $M_n(\cM_{\infty}|\delta_{\infty}, F \upharpoonright \delta_{\infty})$ above $\eta$. Let $A \subseteq \omega_2^{M_n(x)[g]}$ be as
  in the statement of Lemma \ref{lem:HODeqMn(A)},
  i.e., such that $\ensuremath{\operatorname{HOD}^{M_n(x)[g]}}  = M_n(A)$. Moreover, let
  $\varphi$ be a formula defining $A$, i.e., $\xi \in A$ iff $M_n(x)[g]
  \vDash \varphi(\xi)$. Then, as $F(\xi) = \pi_\infty(\xi)$ for $\xi < \delta_\infty$ by Lemma \ref{lem:piinftyid},
  \begin{align*}
    \xi \in A \text{ iff } M_n(\cM_{\infty} | \delta_{\infty}) \vDash \text{``}1&
    \forces{\mathbb{P}}{} \varphi(\pi_\infty(\xi)), \text{where } \pi_\infty \text{ is the direct limit}\\ &\text{embedding from the systems on }\cM_{\infty}\text{''}
  \end{align*}
  for $\mathbb{P} = \ensuremath{\operatorname{Col}} (\omega, {<}\kappa_\infty)$. Consider
  $L[E](\cM_{\infty} | \delta_{\infty})^{M_n(\cM_{\infty}|\delta_{\infty}, F \upharpoonright
    \delta_{\infty})}$, the result of a fully backgrounded
  extender construction in the sense of \cite{MS94} inside
  $M_n(\cM_{\infty}|\delta_{\infty}, F \upharpoonright \delta_{\infty})$ above
  $\cM_{\infty} | \delta_{\infty}$. The premice $M_n(\cM_{\infty} | \delta_{\infty})$ and
  $L[E](\cM_{\infty} | \delta_{\infty})^{M_n(\cM_{\infty}|\delta_{\infty}, F \upharpoonright
    \delta_{\infty})}$ successfully
  compare to a common proper class premouse without drops on the main
  branches. Since the iterations take place above $\delta_{\infty}$,
  $\xi < \delta_{\infty}$ is not moved and we have by elementarity
  \begin{align*}
    \xi \in A \text{ iff } L[E]&(\cM_{\infty} |
    \delta_{\infty})^{M_n(\cM_{\infty}|\delta_{\infty}, F \upharpoonright
      \delta_{\infty})} \vDash \text{``}1 \forces{\mathbb{P}}{}
   \varphi(\pi_\infty(\xi)), \text{where } \pi_\infty\\ &\text{is the direct limit embedding from the systems on }\cM_{\infty}\text{''}.
  \end{align*}
 Therefore it follows that
  $A \in M_n(\cM_{\infty}|\delta_{\infty}, F \upharpoonright \delta_{\infty})$.

By the same argument as in the proof of Claim \ref{cl:sameleastmeas} in the proof of Lemma \ref{lem:HODeqMn(A)} we now obtain that the universes of $M_n(\cM_{\infty}|\delta_{\infty}, F \upharpoonright \delta_{\infty})$ and $M_n(A)$ agree up to their common least measurable cardinal. In particular, $\gamma$ is also the least inaccessible cardinal above $\eta$ of $M_n(A)$ and we can rearrange
  $M_n(\cM_{\infty}|\delta_{\infty}, F \upharpoonright \delta_{\infty})$ and
  $M_n(A)$ as
  $V_\gamma^{M_n(\cM_{\infty}|\delta_{\infty}, F \upharpoonright
  \delta_{\infty})}$-premice. As such it follows that the
  following equalities for classes (not structures) hold:
  \begin{align*}
    M_n(\cM_{\infty}|\delta_{\infty}, F \upharpoonright \delta_{\infty}) & =
                                                                 M_n(V_\gamma^{M_n(\cM_{\infty}|\delta_{\infty},
                                                                 F
                                                                 \upharpoonright
                                                                 \delta)})
    \\  & = M_n(A) = \ensuremath{\operatorname{HOD}^{M_n(x)[g]}} .
  \end{align*}
\end{proof}

The following corollary follows immediately from Lemma
\ref{lem:piinftyid} and Corollary \ref{cor:HODF}.

\begin{cor}\label{cor:HODpiinfty}
  $\ensuremath{\operatorname{HOD}^{M_n(x)[g]}}  = M_n(\cM_{\infty}|\delta_{\infty}, \pi_\infty \upharpoonright
  \delta_{\infty})$.
\end{cor}

We now consider the iteration strategy for $\cM_{\infty}$. Let $\Lambda$ be
the restriction of $\Sigma_{M_{n+1}^{-}}$ to correctly guided finite
stacks $\vec{\mathcal{T}}$ on $\cM_{\infty}|\delta_{\infty}$ such that
$\vec{\mathcal{T}} \in \hat{\cM}_{\infty}|\kappa_\infty$, where $\kappa_\infty$ is the
least inaccessible cardinal in $\hat{\cM}_{\infty}$ above
$\delta_{\infty}$.

\begin{lemma}\label{lem:LambdaHOD}
  $\Lambda \in \ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $.
\end{lemma}

\begin{proof}
  Let $\mathcal{T}$ be a maximal tree on $\cM_{\infty} | \delta_{\infty}$ with $\mathcal{T} \in
  \hat{\cM}_{\infty}|\kappa_\infty$. Moreover, let $b = \Lambda(\mathcal{T})$. Let $\mathcal{R} = \mathcal{M}_b^\mathcal{T}$ be the last model of $\mathcal{T}^\smallfrown b$. Then
  $\mathcal{R} \in \ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $. Moreover, let $\delta_{\infty}^{\mathcal{F}^*}$ be the least Woodin
  cardinal in $\cM_{\infty}^{\mathcal{F}^*}$, the direct limit of the system
  $\mathcal{F}^{*,M(y)}$ for some/all dlm-suitable $M(y)$ in $\hat{\cM}_{\infty}[H]$. Then
  $\cM_{\infty}^{\mathcal{F}^*} | \delta_{\infty}^{\mathcal{F}^*}$ is an iterate of $\mathcal{R}$. As
  $\pi_\infty \upharpoonright \delta_{\infty} \in \ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $, we can identify
  $b$ inside $M_n(x)[g]$ as the unique branch through $\mathcal{T}$ which is
  $(\pi_\infty \upharpoonright \delta_{\infty})$-realizable, i.e., such that
  there is an elementary embedding
  $\sigma: \mathcal{M}_b^\mathcal{T} \rightarrow \cM_{\infty}^{\mathcal{F}^*} | \delta_{\infty}^{\mathcal{F}^*}$
  with $\pi_\infty \upharpoonright \delta_{\infty} = \sigma \circ i_b^\mathcal{T}$.

  The same argument applies to pseudo-normal iterates $\mathcal{N}$ of $\cM_{\infty}$
  with $\mathcal{N}|\delta^{\mathcal{N}} \in \hat{\cM}_{\infty}|\kappa_\infty$ and maximal
  iteration trees $\mathcal{T}$ on $\mathcal{N} | \delta^{\mathcal{N}}$ such that
  $\mathcal{T} \in \hat{\cM}_{\infty}|\kappa_\infty$, hence $\Lambda \in \ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $.
\end{proof}

Similarly to Lemma $3.47$ in \cite{StW16} we finally need a method of
Boolean-valued comparison. As the proof is analogous we omit it.

\begin{lemma}\label{lem:BooleanComp}
  Let $H$ be $\ensuremath{\operatorname{Col}} (\omega, {<}\kappa_\infty)$-generic over $\hat{\cM}_{\infty}$,
  and let $\mathcal{Q}$ be such that $\hat{\cM}_{\infty}[H] \vDash \text{``}\mathcal{Q} \text{ is
    countable and }n\text{-suitable''}$. Then there is an $\mathcal{R}$ such
  that
  \begin{enumerate}
  \item $\mathcal{R}$ is a pseudo-normal iterate of $\mathcal{Q}$,
  \item $\mathcal{R}$ is a $\Sigma_{M_{n+1}^-}$-iterate of
    $\cM_{\infty}$, and
  \item $\mathcal{R} \in \hat{\cM}_{\infty}$.
  \end{enumerate}
\end{lemma}

Finally, we can finish the proof of Theorem \ref{thm:main}.

\begin{thm}\label{thm:finalmain}
  \[\ensuremath{\operatorname{HOD}^{M_n(x)[g]}}  = M_n(\cM_{\infty}|\delta_{\infty}, \pi_\infty \upharpoonright \delta_{\infty})
    = M_n(\hat{\cM}_{\infty}|\kappa_{\infty}, \Lambda).\]
\end{thm}

\begin{proof}
  $\ensuremath{\operatorname{HOD}^{M_n(x)[g]}}  = M_n(\cM_{\infty}|\delta_{\infty}, \pi_\infty \upharpoonright \delta_{\infty})$
  is Corollary \ref{cor:HODpiinfty}. Moreover,
  $M_n(\cM_{\infty}|\delta_{\infty}, \pi_\infty \upharpoonright \delta_{\infty}) =
  M_n(\hat{\cM}_{\infty}|\kappa_{\infty}, \Lambda)$ follows from Lemma
  \ref{lem:BooleanComp} as follows. First, $\Lambda \in M_n(\cM_{\infty}|\delta_{\infty}, \pi_\infty \upharpoonright \delta_{\infty}) = \ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $ and $\hat{\cM}_{\infty}|\kappa_\infty \in M_n(\cM_{\infty}|\delta_{\infty}, \pi_\infty \upharpoonright \delta_{\infty})$ by considering the $Lp^n$-stack on $\cM_{\infty}|\delta_{\infty}$. The direct limit of $\mathcal{F}^{*,M(y)}$ for some $M(y)$ is the same as
  the direct limit of all $\Lambda$-iterates of $\cM_{\infty}$ which are an
  element of $\hat{\cM}_{\infty}|\kappa_{\infty}$ via the comparison
  maps. Moreover, we have that $\pi_\infty$ is the canonical direct
  limit map of this system and therefore definable from
  $\hat{\cM}_{\infty} | \kappa_{\infty}$ and $\Lambda$. So
  $\pi_\infty \upharpoonright \delta_{\infty} \in M_n(\hat{\cM}_{\infty}|\kappa_{\infty},
  \Lambda)$. Now, $M_n(\cM_{\infty}|\delta_{\infty}, \pi_\infty \upharpoonright \delta_{\infty}) = M_n(\hat{\cM}_{\infty}|\kappa_{\infty}, \Lambda)$ follows analogous to the proof of Corollary \ref{cor:HODF}.
\end{proof}

Note that Theorem \ref{thm:HODuptoDelta} and Lemma \ref{lem:HODeqMn(A)} together imply Corollary \ref{cor:main}, i.e., that the $\ensuremath{\operatorname{GCH}} $ holds in $\ensuremath{\operatorname{HOD}^{M_n(x)[g]}} $. Finally, most of the arguments we gave in this and the previous sections generalize with only small changes to more arbitrary canonical self-iterable inner models, e.g. $M_\omega$, $M_{\omega +42}$. We leave the details to the reader.

\bibliographystyle{abstract}

redpajama_set_name: RedPajamaArXiv