Fine structure from normal iterability
Farmer Schlutzenberg
TL;DR
This work establishes that normal iterability suffices to derive the standard fine-structural properties for premice, previously proven via stacks. It proves that m-sound, (m,ω1+1)-iterable premice are (m+1)-solid and (m+1)-universal, with condensation, and that under mild assumptions such premice are normal iterates of their (m+1)-cores when finitely generated above the projectum. The paper develops a robust toolkit—bicephali techniques, finite-support copying, and detrended Dodd-/super-Dodd-structure—to carry out comparisons and to capture extenders, even in the presence of superstrongs. It also shows that countably complete ultrafilters in mice arise from finitely generated iterates, and obtains an initial-segment condition for pseudo-premice under ω1+1-iterability. Collectively, these results advance our understanding of fine structure under normal iterability and clarify when a mouse must be a core-iterate, with wide implications for inner model theory and geology of grounds under σ-closed forcing.
Abstract
We show that (i) the standard fine structural properties for premice follow from normal iterability (whereas the classical proof relies on iterability for stacks of normal trees), and (ii) every mouse which is finitely generated above its projectum, is an iterate of its core. That is, let $m$ be an integer and let $M$ be an $m$-sound, $(m,ω_1+1)$-iterable premouse. Then (i) $M$ is $(m+1)$-solid and $(m+1)$-universal, $(m+1)$ condensation holds for $M$, and if $m\geq 1$ then $M$ is super-Dodd-sound, a slight strengthening of Dodd-soundness. And (ii) if there is $x\in M$ such that $M$ is the $\mathrm{r}Σ_{m+1}$-hull of parameters in $ρ_{m+1}^M\cup\{x\}$, then $M$ is a normal iterate of its $(m+1)$-core $C=\mathfrak{C}_{m+1}(M)$; in fact, there is an $m$-maximal iteration tree $\mathcal{T}$ on $C$, of finite length, such that $M=M^{\mathcal{T}}_\infty$, and $i^{\mathcal{T}}_{0\infty}$ is just the core embedding. Applying fact (ii), we prove that if $M\models\mathrm{ZFC}$ is a mouse and $W\subseteq M$ is a ground of $M$ via a strategically $σ$-closed forcing $\mathbb{P}\in W$, and if $M|\aleph_1^M\in W$ (that is, the initial segment of $M$ of height $\aleph_1^M$ is in $W$), then the forcing is trivial; that is, $M\subseteq W$. And if there is a measurable cardinal, then there is a non-solid premouse. The results hold for premice with Mitchell-Steel indexing, allowing extenders of superstrong type to appear on the extender sequence.