Supercomplete extenders and type 1 mice. I (Q1877090)

Typically, a core model is constructed ``below \(\Psi\)'', i.e., you assume ZFC and the negation of \(\Psi\) (where \(\Psi\) is a large cardinal axiom) and show that the core model \textbf{K} exists and has certain properties. Earlier core models (the Dodd-Jensen core model due to \textit{A. Dodd} and \textit{R. Jensen} [Ann. Math. Logic 20, 43--75 (1981; Zbl 0457.03051)], the short core model due to \textit{P. Koepke} [Ann. Pure Appl. Logic 37, No. 2, 179--204 (1988; Zbl 0638.03049)], the core model for measures of order zero due to \textit{R. Jensen} [handwritten notes (1988)], and others) have been constructed with just these assumptions, but the Steel construction of higher core models (e.g., below a Woodin cardinal) [\textit{J. R. Steel}, The core model iterability problem, Berlin: Springer, Lecture Notes in Logic 8 (1996; Zbl 0864.03035)] works only under the assumption of ZFC + ``all mice are 1-small'' + ``there is a measurable cardinal''. The additional measurable cardinal is believed to be an artifact of the proof, and Steel has conjectured that this assumption is not necessary. The removal of the additional measurable cardinal has been one of the main technical questions of core model theory since then. Whether this is possible for the core model with one Woodin cardinal is still open, but progress has been made in the programme of removing the additional assumption from intermediate core model constructions (i.e., stronger than the ones known before Steel's construction but weaker than the core model with one Woodin cardinal). \textit{R.-D. Schindler} [Ann. Pure Appl. Logic 116, No. 1--3, 205--272 (2002; Zbl 1017.03029)] constructed the ``core model below zero handgrenade'' (this is what Feng and Jensen would call the ``core model of type 0 mice'') without additional assumptions and used it to improve consistency strength analyses for statements in the realm of several strong cardinals. In the paper under review, Feng and Jensen extend this to the ``core model of type 1 mice''. A cardinal \(\kappa\) is called type 0 if the set of cardinals that are strong up to \(\kappa\) is bounded in \(\kappa\), it is called type \(\geq 1\) if this set of cardinals is unbounded in \(\kappa\). The cardinal \(\kappa\) is called type \(\geq 2\) if it is of type \(\geq 1\) and a limit of cardinals of type \(\geq 1\). A premouse is called type 1 if all of its extenders have critical points that are of type \(\leq 1\) (Definitions 2.1 and 2.2). Schindler's model corresponds to iteration trees with finite branching, whereas type 1 mice can involve infinite branching in iteration trees (Example 2.1). Feng and Jensen give a definition of the \textbf{K}\(^{\text{c}}\)-construction for supercomplete extenders (this is a stronger property than the countable completeness of Schindler's core model) and prove an iterability theorem for it under the meta-assumption of an inaccessible cardinal (Section 4). They mention that they consider this construction to be a ``warm-up'' for a more general construction that will not need the additional assumption of an inaccessible cardinal, and refer the reader to part II of this paper.