The definability of the extender sequence $\mathbb{E}$ from $\mathbb{E}{\upharpoonright}\aleph_1$ in $L[\mathbb{E}]$
Farmer Schlutzenberg
TL;DR
This work addresses the definability of the extender sequence $\mathbb{E}^M$ from a small initial segment in short extender mice. It develops condensation-stack techniques to bypass reliance on self-iterability and proves that $\mathbb{E}^M$ is $\Delta_2^{\lfloor M\rfloor}(\{\mathbbm m^M\})$-definable for suitable $M$, with corollaries yielding $V=\mathrm{HOD}$ under ZFC and related forcing-local variants. The paper also introduces a direct condensation stack approach in $M[G]$, and furnishes a simplified fine-structure that omits the $u_n$-parameters while preserving the core fine-structural notions. Together, these results deepen the understanding of extender-sequence definability, enable global and local definability conclusions, and connect to HOD-type consequences in Woodin-like settings, via both new methods and a streamlined fine-structure framework.
Abstract
Let $M$ be a short extender mouse. We prove that if $E\in M$ and $M$ satisfies "$E$ is a countably complete short extender whose support is a cardinal $θ$ and $\mathcal{H}_θ\subseteq\mathrm{Ult}(V,E)$", then $E$ is in the extender sequence $\mathbb{E}^M$ of $M$. We also prove other related facts, and use them to establish that if $κ$ is an uncountable cardinal of $M$ and $κ^{+M}$ exists in $M$ then $(\mathcal{H}_{κ^+})^M$ satisfies the Axiom of Global Choice. We prove that if $M$ satisfies the Power Set Axiom then $\mathbb{E}^M$ is definable over the universe of $M$ from the parameter $X=\mathbb{E}^M\upharpoonright\aleph_1^M$, and $M$ satisfies "every set is $\mathrm{OD}_{\{X\}}$". We also prove various local versions of this fact in which $M$ has a largest cardinal, and a version for generic extensions of $M$. As a consequence, for example, the minimal proper class mouse with a Woodin limit of Woodin cardinals models "$V=\mathrm{HOD}$". This adapts to many other similar examples. We also describe a simplified approach to Mitchell-Steel fine structure, which does away with the parameters $u_n$.