Fine structure from normal iterability

In this paper, 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). We also show that (ii) every mouse which is finitely generated above its projectum, is an iterate of its core. That is, let [Formula: see text] and let [Formula: see text] be an [Formula: see text]-sound, [Formula: see text]-iterable premouse. Then (i) [Formula: see text] is [Formula: see text]-solid and [Formula: see text]-universal, [Formula: see text]-condensation holds for [Formula: see text], and if [Formula: see text] then [Formula: see text] is super-Dodd-sound, a slight strengthening of Dodd-soundness, and (ii) if there is [Formula: see text] such that [Formula: see text] is the [Formula: see text]-hull of parameters in [Formula: see text], then [Formula: see text] is a normal iterate of its [Formula: see text]th core [Formula: see text]; in fact, there is an [Formula: see text]-maximal iteration tree [Formula: see text] on [Formula: see text], of finite length, such that [Formula: see text] and [Formula: see text] is just the core embedding. Applying fact (ii), we prove that if [Formula: see text] is a mouse and [Formula: see text] is a ground of [Formula: see text] via a forcing [Formula: see text] such that [Formula: see text] “[Formula: see text] is strategically [Formula: see text]-closed” and [Formula: see text] (that is, the initial segment of [Formula: see text] of height [Formula: see text] is in [Formula: see text]), then [Formula: see text]. We also describe an example of a non-solid premouse, and study mice which fail to be normal iterates of their cores. The results hold for premice with Mitchell-Steel indexing, allowing extenders of superstrong type to appear on the extender sequence.