Ordinal definability in $L[\mathbb{E}]$

TL;DR

This paper proves that tame mice modeling ZFC have definable extender sequences and satisfy certain HOD-related properties, extending some results to non-tame mice under specific hypotheses.

Contribution

It demonstrates the definability of extender sequences and HOD properties in tame mice, and extends some results to non-tame mice with additional hypotheses.

Findings

Mice satisfy V=HOD_x for some real x.

Extender sequence above ω₁^M is definable without parameters.

Many natural φ-minimal mice model V=HOD under certain hypotheses.

Abstract

Let $M$ be a tame mouse modelling ZFC. We show that $M$ satisfies "$V=\mathrm{HOD}_x$ for some real $x$", and that the restriction $\mathbb{E}\upharpoonright[\omega_1^M,\mathrm{OR}^M)$ of the extender sequence $\mathbb{E}^M$ of $M$ to indices above $\omega_1^M$ is definable without parameters over the universe of $M$. We show that $M$ has universe $\mathrm{HOD}^M[X]$, where $X=M|\omega_1^M$ is the initial segment of $M$ of height $\omega_1^M$ (including $\mathbb{E}^M\upharpoonright\omega_1^M$), and that $\mathrm{HOD}^M$ is the universe of a premouse over some $t\subseteq\omega_2^M$. We also show that $M$ has no proper grounds via strategically $\sigma$-closed forcings. We then extend some of these results partially to non-tame mice, including a proof that many natural $\varphi$-minimal mice model "$V=\mathrm{HOD}$", assuming a certain fine structural hypothesis whose proof has almost been given elsewhere.