2.1. Short-tree-strategy mice

We are assuming that V is the minimal model of $\mathsf {LSA}$ . Suppose $\Lambda $ is a short-tree strategy for a hod mouse ${\mathcal {P}}$ . We let ${\delta }$ be the largest Woodin cardinal of ${\mathcal {P}}$ . Thus, ${\mathcal {P}}=({\mathcal {P}}|{\delta })^\#$ . In this subsection, we would like to convince the reader that the concept of $\Lambda $ -mouse, while much more involved, behaves very similarly to the concept of a $\Sigma $ -mouse where $\Sigma $ is an iteration strategy.

In general, when introducing any notion of a mouse, one has to keep in mind the procedures that allow us to build such mice. Formally speaking, many notions of $\Lambda $ -mice might make perfect sense, but when we factor into it the constructions that are supposed to produce such mice, we run into a key issue.

In any construction that produces some sort of mouse (e.g., $K^c$ -constructions, fully backgrounded constructions, etc.), there are stages where one has to consider certain kinds of Skolem hulls, or as inner model theorists call them, fine structural cores. The reader can view these cores as some carefuly defined Skolem hulls. To illustrate the aformentioned problem, imagine we do have some notion of $\Lambda $ -mice and let us try to run a construction that will produce such mice. Suppose ${\mathcal {T}}$ is a tree according to $\Lambda $ that appears in this construction. Having a notion of a $\Lambda $ -mouse means that we have a prescription for deciding whether $\Lambda ({\mathcal {T}})$ should be indexed in the strategy predicate or not.

Suppose ${\mathcal {T}}$ is a $\Lambda $ -maximal tree. It is hard to see exactly what one can index so that the strategy predicate remembers that ${\mathcal {T}}$ is maximal. And this ‘remembering’ is the issue. Imagine that at a later stage, we have a Skolem hull $\pi : {\mathcal {M}}\rightarrow {\mathcal {N}}$ of our current stage such that ${\mathcal {T}}\in rng(\pi )$ . It is possible that ${\mathcal {U}}=_{def}\pi ^{-1}({\mathcal {T}})$ is $\Lambda $ -short. If we have indexed X in our strategy that proves $\Lambda $ -maximality of ${\mathcal {T}}$ , then $\pi ^{-1}(X)$ now can no longer prove that ${\mathcal {U}}$ is $\Lambda $ -maximal. Thus, the notion of $\Lambda $ -mouse cannot be first order.

The solution is simply not to index anything for $\Lambda $ -maximal trees. This does not quite solve the problem as the above situation implies that nothing should be indexed for many $\Lambda $ -short trees as well. To solve this problem, we will only index the branches of some $\Lambda $ -short trees, those that we can locally prove are $\Lambda $ -short. We explain this below in more details.

Fix an lsa type hod premouse ${\mathcal {P}}$ and let $\Lambda $ be its short-tree strategy. Let ${\delta }$ be the largest Woodin cardinal of ${\mathcal {P}}$ and $\nu $ be the least $<{\delta }$ -strong of ${\mathcal {P}}$ . To explain the exact prescription that we use to index $\Lambda $ , we explain some properties of the models that have already been constructed according to this indexing scheme. Suppose ${\mathcal {M}}$ is a $\Lambda $ -premouse.

Call ${\mathcal {T}}\in {\mathcal {M}}$ universally short ( $\mathsf {uvs}$ ) if ${\mathcal {T}}$ is obviously short (see [Reference Sargsyan and Trang38, Definition 3.3.2]). For instance, it can be that the $\#$ -operator provides a ${\mathcal {Q}}$ -structure and determines a branch c of ${\mathcal {T}}$ such that ${\mathcal {Q}}(c, {\mathcal {T}})$ Footnote ³⁷ exists and ${\mathcal {Q}}(c, {\mathcal {T}})\unlhd {\mathrm m}^+({\mathcal {T}})$ . Another way that a tree can be obviously short is that there could be a model ${\mathcal {Q}}$ in ${\mathcal {T}}$ such that $\pi ^{\mathcal {T}}_{{\mathcal {P}}, {\mathcal {Q}}}:{\mathcal {P}}\rightarrow {\mathcal {Q}}$ is defined and the portion of ${\mathcal {T}}$ that comes after ${\mathcal {Q}}$ is based on ${\mathcal {Q}}^b$ . Here, ${\mathcal {Q}}^b$ is defined as ${\mathcal {Q}}|(\kappa ^+)^{\mathcal {Q}}$ , where $\kappa $ is the supremum of the Woodin cardinals below the largest Woodin of ${\mathcal {Q}}$ . The reader should keep in mind that there is a formula $\zeta $ in the language of $\Lambda $ -premice such that for any $\Lambda $ -premouse ${\mathcal {M}}$ and for any iteration tree ${\mathcal {T}}\in {\mathcal {M}}$ , ${\mathcal {T}}$ is $\mathsf {uvs}$ if and only if ${\mathcal {M}}{\vDash } \zeta [{\mathcal {T}}]$ .

Unfortunately, there can be trees that are not universally short ( $\mathsf {nuvs}$ ). Suppose then ${\mathcal {T}}$ is $\mathsf {nuvs}$ . In this case, whether we index $\Lambda ({\mathcal {T}})$ or not depends on whether we can find a ${\mathcal {Q}}$ -structure that can be authenticated to be the correct one. There can be many ways to certify a ${\mathcal {Q}}$ -structure, and [Reference Sargsyan and Trang38] provides one such method. An interested reader can consult [Reference Sargsyan and Trang38, Chapter 3.7]. Notice that because ${\mathcal {P}}$ has only one Woodin cardinal, not being able to find a ${\mathcal {Q}}$ -structure is equivalent to the tree being maximal. Thus, in a nutshell, the solution proposed by [Reference Sargsyan and Trang38] is that we index only branches that are given by internally authenticated ${\mathcal {Q}}$ -structures.

Suppose now that we have the above Skolem hull situation – namely, that we have $\pi :{\mathcal {M}}\rightarrow {\mathcal {N}}$ and ${\mathcal {T}}$ in ${\mathcal {N}}$ that is $\Lambda $ -maximal but $\pi ^{-1}({\mathcal {T}})$ is short. There is no more indexing problem. The reason is that in order to index $\Lambda (\pi ^{-1}({\mathcal {T}}))$ in ${\mathcal {M}}$ , we need to find an authenticated ${\mathcal {Q}}$ -structure for $\pi ^{-1}({\mathcal {T}})$ . The authentication process is first order, and so if ${\mathcal {N}}$ does not have such an authenticated ${\mathcal {Q}}$ -structure for ${\mathcal {T}}$ , then ${\mathcal {M}}$ cannot have such an authenticated ${\mathcal {Q}}$ -structure for $\pi ^{-1}({\mathcal {T}})$ .

The reader of this paper does not need to know the exact way the authentication procedure works. However, the reader should keep in mind that the authentication procedure is internal to the mouse. More precisely, the following holds:

Internal Definability of Authentication: there is a formula $\phi $ in the appropriate language such that whenever $({\mathcal {P}}, \Lambda )$ is as above and ${\mathcal {M}}$ is a $\Lambda $ -mouse over some set X such that ${\mathcal {P}}\in X$ , for any iteration tree ${\mathcal {T}}\in {\mathcal {M}}$ , ${\mathcal {M}}{\vDash } \phi [{\mathcal {T}}]$ if and only if ${\mathcal {T}}\in dom(\Lambda )$ , ${\mathcal {T}}$ is short and $\Lambda ({\mathcal {T}})\in {\mathcal {M}}$ .

We again note that the Internal Definability of Authentication (IDA) is only shown to be true for the minimal model of $\mathsf {LSA}$ . In general, IDA cannot be true as there can be short trees without ${\mathcal {Q}}$ -structures. The authors have recently discovered another short-tree indexing scheme that can work in all cases but has some weaknesses compared to the one introduced in [Reference Sargsyan and Trang38].

Using the notation in [Reference Sargsyan and Trang38], recall that ${\mathcal {P}}^b$ is the ‘bottom part’ of ${\mathcal {P}}$ (i.e., ${\mathcal {P}}^b = {\mathcal {P}}|(\nu ^+)^{{\mathcal {P}}}$ , where $\nu $ is the supremum of the Woodin cardinals below the top Woodin of ${\mathcal {P}}$ ).

We now describe another key feature of the indexing scheme of [Reference Sargsyan and Trang38] that is of importance here. We say $\Sigma $ is a low-level component of $\Lambda $ if there is a tree ${\mathcal {T}}$ on ${\mathcal {P}}$ according to $\Lambda $ such that $\pi ^{{\mathcal {T}}, b}$ existsFootnote ³⁸ ( ${\mathcal {T}}$ may be $\emptyset $ ) and for some ${\mathcal {R}}\unlhd \pi ^{{\mathcal {T}}, b}({\mathcal {P}}^b)$ , $\Sigma =\Lambda _{\mathcal {R}}$ . Let $LLC(\Lambda )$ be the set of $\Sigma $ that are low-level components of $\Lambda $ . What is shown in [Reference Sargsyan and Trang38] is that $\Lambda $ is determined by $LLC(\Lambda )$ in a strong sense.

Given a transitive model M of a fragment of $\mathsf {ZFC}$ such that ${\mathcal {P}}\in M$ , we say M is closed under $LLC(\Lambda )$ if whenever ${\mathcal {T}}\in M$ is a tree according to $\Lambda $ such that $\pi ^{{\mathcal {T}}, b}$ exists, $\Lambda _{\pi ^{{\mathcal {T}}, b}({\mathcal {P}}^b)}$ has a universally Baire representation over M. More precisely, whenever $g\subseteq Coll(\omega , \pi ^{{\mathcal {T}}, b}({\mathcal {P}}^b))$ is M-generic, for every M-cardinal ${\lambda }$ , there are trees $T, S\in M[g]$ on ${\lambda }$ such that $M[g]{\vDash } \text {`}(T, S)$ are $<{\lambda }$ -complementing’ and for all $<{\lambda }$ -generics h, $(p[T])^{M[g*h]}=Code(\Lambda _{\pi ^{{\mathcal {T}}, b}({\mathcal {P}}^b)})\cap M[g*h]$ . Here, $Code(\Phi )$ is the set of reals coding $\Phi $ (with respect to a fixed coding of elements of $HC$ by reals).

It is shown in [Reference Sargsyan and Trang38] that if, assuming $\mathsf {AD}^+$ , $(M, \Sigma )$ is such that

1. 1. M is a countable model of a fragment of $\mathsf {ZFC}$ ,

2. 2. M has a class of Woodin cardinals,

3. 3. $\Sigma $ is an $\omega _1$ -iteration strategy for M and

4. 4. whenever $i:M\rightarrow N$ is an iteration via $\Sigma $ , N is closed under $LLC(\Lambda )$ ,

then there is a formula $\psi $ such that whenever g is M-generic, for any ${\mathcal {T}}\in M[g]$ ,

(⋆) $$ \begin{align} {\mathcal{T}} \ \text{is according to } \Lambda \text{ if and only if } M[g]{\vDash} \psi[{\mathcal{T}}]. \end{align} $$

The interested reader can consult Chapters 5, 6 and 8 of [Reference Sargsyan and Trang38].

The reason we explained the above is to give the reader some confidence that defining a short-tree strategy $\Lambda $ for a hod premose ${\mathcal {P}}$ is equivalent to describing the set $LLC(\Lambda )$ . This fact is the reason that the indexing schema of [Reference Sargsyan and Trang38] works in the following sense.

Being able to define short-tree-strategy mice is one thing; proving that they are useful is another. Usually what needs to be shown are the following two key statements. We let $\phi _{sts}$ be the formula that is mentioned in the Internal Definability of Authentication.

The Eventual Authentication. Suppose $({\mathcal {P}}, \Lambda )$ is as above and ${\mathcal {M}}$ is a sound $\Lambda $ -mouse over some set X such that ${\mathcal {P}}\in X$ and ${\mathcal {M}}$ projects to X. Suppose ${\mathcal {T}}\in {\mathcal {M}}$ is according to $\Lambda $ and is $\Lambda $ -short. Suppose further that ${\mathcal {M}}{\vDash } \neg \phi _{sts}[{\mathcal {T}}]$ . Then there is a sound $\Lambda $ -mouse ${\mathcal {N}}$ over X such that ${\mathcal {M}}\unlhd {\mathcal {N}}$ and ${\mathcal {N}}{\vDash } \phi _{sts}[{\mathcal {T}}]$ .Footnote ³⁹

Mouse Capturing for $\Lambda $ : Suppose $({\mathcal {P}}, \Lambda )$ is as above. Then for any $x\in \mathbb {R}$ that codes ${\mathcal {P}}$ and any $y\in \mathbb {R}$ , y is ordinal definable from x and $\Lambda $ if and only if there is a $\Lambda $ -mouse ${\mathcal {M}}$ over x such that $y\in {\mathcal {M}}$ .

Both The Eventual Authentication and Mouse Capturing for $\Lambda $ are proven in [Reference Sargsyan and Trang38] (see [Reference Sargsyan and Trang38, Chapter 8, Lemma 8.1.3, Lemma 8.1.5] and [Reference Sargsyan and Trang38, Theorem 10.2.1]).

The next subsection discusses the ${\mathcal {Q}}$ -structure authentication process mentioned above.

2.2. The authentication method

Suppose ${\mathcal {P}}$ is a $\#$ -lsa type hod premouse. Recall from the previous subsections that this means that ${\mathcal {P}}$ has a largest Woodin cardinal ${\delta }$ such that ${\mathcal {P}}=({\mathcal {P}}|{\delta })^\#$ and the least $<{\delta }$ -strong cardinal of ${\mathcal {P}}$ is a limit of Woodin cardinals. We let ${\delta }^{\mathcal {P}}$ be the largest Woodin cardinal of ${\mathcal {P}}$ and ${\kappa }^{\mathcal {P}}$ be the least $<{\delta }^{\mathcal {P}}$ -strong cardinal of ${\mathcal {P}}$ . We shall also require that ${\mathcal {P}}$ is tame, meaning that for any $\nu <{\delta }^{\mathcal {P}}$ , if $({\mathcal {P}}|\nu )^\#$ is of lsa type and ${\mathcal {M}}{\trianglelefteq } {\mathcal {P}}$ is the largest such that ${\mathcal {M}}{\vDash } \text {`}\nu $ is a Woodin cardinal’, then $\nu $ is not overlapped in ${\mathcal {M}}$ .Footnote ⁴⁰

Our goal here is to explain the ${\mathcal {Q}}$ -structure authentication procedure employed by [Reference Sargsyan and Trang38]. Recall our discussion of $\mathsf {uvs}$ and $\mathsf {nuvs}$ trees. The ${\mathcal {Q}}$ -structure authentication procedure applies to only $\mathsf {nuvs}$ trees – trees that are not obviously short.

[Reference Sargsyan and Trang38, Chapters 3.6-3.9] develop the aforementioned authentication procedure. [Reference Sargsyan and Trang38, Definition 3.8.9, 3.8.16, 3.8.17] introduce the sts indexing scheme. For illustrative purposes, it is better to think of the indexing scheme introduced there as a hierarchy of indexing schemes indexed by ordinals. Naturally, this hierarchy is defined by induction. For illustrative purposes we call ${\gamma }$ th level of the hierarchy $sts_{\gamma }$ . Thus, $sts_{\gamma }({\mathcal {P}})$ is the set of all sts premice that are based on ${\mathcal {P}}$ (i.e., their short-tree-strategy predicate describes a short-tree strategy for ${\mathcal {P}}$ ) and have rank $\leq {\gamma }$ .

To begin the induction, we let $sts_0({\mathcal {P}})$ be the set of all sts premice that do not index a branch for any $\mathsf {nuvs}$ tree. More precisely, if ${\mathcal {M}}\in sts_0({\mathcal {P}})$ and ${\mathcal {T}}\in dom(S^{\mathcal {M}})$ , then if $S^{\mathcal {M}}({\mathcal {T}})$ is defined, then ${\mathcal {T}}$ is $\mathsf {uvs}$ .

Below and elsewhere, $S^{\mathcal {M}}$ is the strategy predicate of ${\mathcal {M}}$ . Given $sts_{{\alpha }}({\mathcal {P}})$ , we let $sts_{{\alpha }+1}({\mathcal {P}})$ be the set of all sts premice that index branches of those $\mathsf {nuvs}$ trees that have a ${\mathcal {Q}}$ -structure in $sts_{\alpha }({\mathcal {P}})$ . More precisely, suppose ${\mathcal {M}}\in sts_{{\alpha }+1}({\mathcal {P}})$ and ${\mathcal {T}}\in dom(S^{\mathcal {M}})$ and $S^{\mathcal {M}}({\mathcal {T}})$ is defined. Then either

1. 1. ${\mathcal {T}}$ is $\mathsf {uvs}$ or

2. 2. ${\mathcal {T}}$ is $\mathsf {nuvs}$ and there is ${\mathcal {Q}}\in {\mathcal {M}}$ such that ${\mathcal {M}}{\vDash } \text {`}{\mathcal {Q}}\in sts_{\alpha }({\mathcal {P}})'$ , ${\mathrm m}^+({\mathcal {T}}){\trianglelefteq }{\mathcal {Q}}$ , ${\mathcal {Q}}{\vDash } \text {`}{\delta }({\mathcal {T}})$ is a Woodin cardinal’ but ${\delta }({\mathcal {T}})$ is not a Woodin cardinal with respect to some function definable over ${\mathcal {Q}}$ Footnote ⁴¹ and there is a cofinal branch b of ${\mathcal {T}}$ such that ${\mathcal {Q}}{\trianglelefteq } {\mathcal {M}}^{\mathcal {T}}_b$ .

When ${\mathcal {Q}}$ exhibits the properties listed in clause 2, we say that ${\mathcal {Q}}$ is a ${\mathcal {Q}}$ -structure for ${\mathcal {T}}$ . It follows from the zipper argument of [Reference Martin and Steel25, Theorem 2.2] that for each ${\mathcal {Q}}$ -structure ${\mathcal {Q}}$ , there is at most one branch b with properties described in clause 2 above. However, there is nothing that we have said so far that guarantees the uniqueness of the ${\mathcal {Q}}$ -structure itself. The uniqueness is usually a consequence of iterability and comparison (see [Reference Steel53, Theorem 3.11]).Footnote ⁴² Thus, to make the definition of $sts_{{\alpha }+1}$ complete, we need to impose an iterability condition on ${\mathcal {Q}}$ .

The exact iterability condition that one needs is stated as clause 5 of [Reference Sargsyan and Trang38, Definition 3.8.9]. This clause may seem technical, but there are good reasons for it. For the purposes of identifying a unique branch b saying that ${\mathcal {Q}}$ in clause 2 is sufficiently iterable in ${\mathcal {M}}$ would have sufficed. However, recall the statement of the Internal Definability of Authentication. The problem is that when we require that an ${\mathcal {M}}$ as above is a $\Lambda $ -premouse, we in addition must say that the branch b that the ${\mathcal {Q}}$ -structure ${\mathcal {Q}}$ defines is the exact same branch that $\Lambda $ picks. To guarantee this, we need to impose a condition on ${\mathcal {Q}}$ such that ${\mathcal {Q}}$ will be iterable not just in ${\mathcal {M}}$ but in V. The easiest way of doing this is to say that ${\mathcal {Q}}$ has an iteration strategy in some derived model as then, using genericity iterations (see [Reference Steel53, Chapter 7.2]), we can extend such a strategy for ${\mathcal {Q}}$ to a strategy that acts on iterations in V.

For limit ${\alpha }$ , $sts_{\alpha }({\mathcal {P}})$ is essentially $\bigcup _{{\beta }<{\alpha }}sts_{\beta }({\mathcal {P}})$ . What has been left unexplained is the kind of strategy that the ${\mathcal {Q}}$ -structure ${\mathcal {Q}}$ must have in some derived model. Let $\Sigma $ be this strategy. If ${\mathcal {M}}\in sts_{\alpha }({\mathcal {P}})$ is a $\Lambda $ -mouse, then ${\mathcal {Q}}$ must be a $\Lambda _{{\mathrm m}^+({\mathcal {T}})}$ -mouse over ${\mathrm m}^+({\mathcal {T}})$ . Thus, our next challenge is to find a first-order way of guaranteeing that $\Sigma $ -iterates of ${\mathcal {Q}}$ are $\Lambda _{{\mathrm m}^+({\mathcal {T}})}$ -mice, even those iterates that we will obtain after blowing up $\Sigma $ via genericity iterations.

The solution that is employed in [Reference Sargsyan and Trang38] is that if ${\mathcal {R}}$ is a $\Sigma $ -iterate of ${\mathcal {Q}}$ and ${\mathcal {U}}\in dom(S^{\mathcal {R}})$ , then ${\mathcal {U}}$ itself is authenticated by the extenders of ${\mathcal {M}}$ . Below, we refer to this certification as tree certification. This is again a rather technical notion, but the following essentially illustrates the situation.

Let us suppose ${\mathcal {R}}={\mathcal {Q}}$ and ${\mathcal {U}}\in dom(S^{\mathcal {Q}})$ . The indexing scheme of [Reference Sargsyan and Trang38] does not index all trees in ${\mathcal {P}}$ . In other words, $S^{\mathcal {M}}$ is never total. $dom(S^{\mathcal {M}})$ consists of trees that are built via a comparison procedure that iterates ${\mathcal {P}}$ to a background construction of ${\mathcal {M}}$ . Set ${\mathcal {N}}={\mathrm m}^+({\mathcal {U}})$ . One requirement is that ${\mathcal {N}}$ also iterates to one such background construction to which ${\mathcal {P}}$ also iterates. Let ${\mathcal {S}}$ be this common background construction and suppose ${\alpha }+1<lh({\mathcal {U}})$ is such that ${\alpha }$ is a limit ordinal. First, assume ${\mathcal {U}}{\restriction } {\alpha }$ is $\mathsf {uvs}$ . What is shown in [Reference Sargsyan and Trang38] is that knowing the branch of ${\mathcal {P}}$ -to- ${\mathcal {S}}$ tree, there is a first-order procedure that identifies the branch of ${\mathcal {U}}{\restriction } {\alpha }$ , and that procedure is the tree certification procedure applied to ${\mathcal {U}}{\restriction } {\alpha }$ .

Suppose next that ${\mathcal {U}}{\restriction } {\alpha }$ is $\mathsf {nuvs}$ . Then because ${\alpha }+1<lh({\mathcal {U}})$ , ${\mathcal {U}}{\restriction } {\alpha }$ must be short and the branch chosen for it in ${\mathcal {Q}}$ must have a ${\mathcal {Q}}$ -structure ${\mathcal {Q}}_1$ , which is itself an sts mouse. We have that ${\mathcal {Q}}_1\in {\mathcal {Q}}$ and ${\mathcal {Q}}_1$ must have the same certification in ${\mathcal {Q}}$ that ${\mathcal {Q}}$ has in ${\mathcal {M}}$ . Again, the $\mathsf {nuvs}$ trees in ${\mathcal {Q}}_1$ have a tree certification in ${\mathcal {Q}}$ according to the above procedure. The $\mathsf {uvs}$ ones produce another ${\mathcal {Q}}_2\in {\mathcal {Q}}_1$ . Because we cannot have an infinite descent, the definition of tree certification is meaningful.

This ends our discussion of sts premice. Of course, a lot has been left out, and the mathematical details are unfortunately excruciating, but we hope that the reader has gained some level of intuition to proceed with the paper.

In the next subsection, we will deal with one of the most important aspects of hod mice – namely, the generic interpretability of iteration strategies.

2.3. Generic interpretability

There are several situations when one has to be careful when discussing sts premice and $\Lambda $ -premice in general. First, for an iteration strategy $\Sigma $ , ${\mathcal {M}}_1^{\#, \Sigma }$ makes complete sense. It is the minimal active $\Sigma $ -mouse with a Woodin cardinal. For short-tree strategy $\Lambda $ , the situation is somewhat different. The expression ‘ ${\mathcal {M}}_1^{\#, \Lambda }$ is the minimal active $\Lambda $ -mouse with a Woodin cardinal’ does not say much as we do not say how closed ${\mathcal {M}}_1^{\#, \Lambda }$ must be. One must also add statements of the form ‘in which all $\Lambda $ -short trees are indexed’. This is because it could be that $\Lambda $ -premouse ${\mathcal {M}}$ is active and has a Woodin cardinal but there is a $\Lambda $ -short tree ${\mathcal {T}}\in {\mathcal {M}}$ that has not yet been indexed in ${\mathcal {M}}$ (see The Eventual Certification above). In particular, without extra assumptions, it may be the case that given a $\Lambda $ -sts mouse ${\mathcal {M}}{\vDash } \mathsf {ZFC}$ , $\Lambda {\restriction } {\mathcal {M}}$ is not definable over ${\mathcal {M}}$ . Clearly, such definability holds for many strategy mice.

The above issue becomes somewhat of a problem when dealing with generic interpretability, which is the statement that the internal strategy predicate can be uniquely extended onto generic extensions. For ordinary strategy mice, generic interpretability is, in general, easier to prove. For short-tree-strategy mice, the situation is somewhat parallel to the above anomaly. Suppose ${\mathcal {M}}$ is a $\Lambda $ -mouse where $\Lambda $ is a short-tree strategy and suppose g is ${\mathcal {M}}$ -generic. In general, we cannot hope to prove that $\Lambda {\restriction } {\mathcal {M}}[g]$ is definable over ${\mathcal {M}}[g]$ . In this subsection, we introduce some properties of short-tree strategies that allow us to prove generic interpretability, albeit in a somewhat weaker sense.

The most important concept that is behind most arguments of [Reference Sargsyan and Trang38] is the concept of branch condensation (see [Reference Sargsyan and Trang38, Chapter 4.9]). It is very possible that the concept of full normalization introduced in [Reference Steel55] can be used instead of branch condensation to obtain a greater generality. In fact, the authors have recently discovered a new notion of a short-tree-strategy mouse utilizing full normalization.

Branch condensation implies generic interpretability. The following is our generic interpretability theorem, which is essentially [Reference Sargsyan and Trang38, Theorem 6.1.5]. The aforementioned theorem is stated for strategies with branch condensation that are associated with a pointclass $\Gamma $ . Here, we need strategies whose association with pointclasses is a consequence of some abstract properties that it has, not something explicitly assumed about them. Such strategies can be obtained working inside a model of determinacy. The specific properties that we need are the following properties:

1. 1. hull condensation,

2. 2. strong branch condensation,

3. 3. branch condensation for pull-backs.

The meaning of clause 3 above is as follows. Suppose $({\mathcal {P}}, \Lambda )$ is an sts hod pair. $\Lambda $ has branch condensation for pullbacks if whenever $\xi \in {\mathcal {P}}$ is a limit of Woodin cardinals of ${\mathcal {P}}$ such that ${\mathcal {P}}{\vDash } \text {`}{\mathrm cf}(\xi )=\omega '$ and $\pi :{\mathcal {Q}}\rightarrow {\mathcal {P}}|\xi $ is elementary, the $\pi $ -pullback of $\Lambda _{{\mathcal {P}}|\xi }$ has branch condensation. For more on branch condensation, the reader may consult [Reference Sargsyan and Trang38, Chapter 4.9].

Clause 3 above implies that the pullback of splendid strategies are splendid.Footnote ⁴⁴ It might help to consult Remark 2.2 before reading the next theorem.

Our Theorem 2.4 is weaker than [Reference Sargsyan and Trang38, Theorem 6.1.4]. The conclusion of the aforementioned theorem is that $\Psi ^g=\Lambda {\restriction } {\mathcal {N}}[g]$ . However, in [Reference Sargsyan and Trang38, Theorem 6.1.4], ${\mathcal {N}}$ satisfies a strong iterability hypothesis. Without this iterability hypothesis, $b(\Psi ^g)\subseteq b(\Lambda ){\restriction } {\mathcal {N}}[g]$ is all the proof that [Reference Sargsyan and Trang38, Theorem 6.1.4] gives.

In the next subsection, we will introduce a type of short-tree-strategy mouse that we will use to establish Theorem 1.4.

2.4. Excellent hod premice

Our proof of Theorem 1.4 is an example of how one can translate set theoretic strength from one set of principles to another set of principles by using inner model theoretic objects as intermediaries. Below, we introduce the notion of an excellent hybrid premouse. We will then use this notion to show that both $\mathsf {Sealing}$ and $\mathsf {LSA-over-uB}$ hold in a generic extension of an excellent hybrid premouse. Conversely, we will show that in any model of either $\mathsf {Sealing}$ or $\mathsf {LSA-over-uB}$ , there is an excellent hybrid premouse. We start by introducing some terminology and then introduce the excellent hybrid premice.

To state our generic interpretability results, we need to introduce a form of self-iterability – namely, window-based self-iterability. We say that $[\nu , {\delta }]$ is a window if there are no Woodin cardinals in the interval $(\nu , {\delta })$ . Given a window w, we let $\nu ^w$ and ${\delta }^w$ be such that $w=[\nu ^w, {\delta }^w]$ . We say that a window w is above ${\kappa }$ if $\nu ^w\geq {\kappa }$ . We say that a window w is not overlapped if there is no $\nu ^w$ -strong cardinal. We say w is maximal if $\nu ^w=\sup \{{\alpha }+1: {\alpha }<\nu ^w$ is a Woodin cardinal $\}$ and ${\delta }^w$ is a Woodin cardinal.

Window-Based Self-Iterability. Suppose ${\kappa }$ is a cardinal. We say $\mathsf {WBSI}$ holds at ${\kappa }$ if for any window w that is above ${\kappa }$ and for any successor cardinal $\eta \in (\nu ^w, {\delta }^w)$ , setting $Q= H_{\eta ^+}$ , Q has an $Ord$ -iteration strategy $\Sigma $ which acts on iterations that only use extenders with critical points $>\nu ^w$ .

One usually says that Q is $Ord$ -iterable above $\nu ^w$ to mean exactly what is written above.

When we write $M{\vDash } T_0$ and M has a distinguished extender sequence, then we make the tacit assumption that the large cardinals and specific ultrafilters mentioned in Definition 2.6 are witnessed by extenders on the sequence of M.

For the rest of this paper, we assume the following minimality hypothesis $\neg (\dagger )$ , where

$(\dagger ):$ In some generic extension, there is a (possibly class-sized) excellent hybrid premouse.

We will periodically remind the reader of this. One consequence of this assumption is the following fact, which roughly says that all local non-Woodin cardinals of a hod premouse (or hybrid premouse) are witnessed by ${\mathcal {Q}}$ -structures which are initial segments of the model and are tame. It also shows that if ${\mathcal {P}}$ is a hod mouse such that there is an lsa initial segment ${\mathcal {P}}_0$ of ${\mathcal {P}}$ and there is a Woodin cardinal $\delta> o({\mathcal {P}}_0)$ inside ${\mathcal {P}}$ , then we can construct an excellent hybrid premouse in ${\mathcal {P}}$ by essentially performing a fully backgrounded sts construction in ${\mathcal {P}}|\delta $ above ${\mathcal {P}}_0$ (with respect to the short-tree component of ${\mathcal {P}}_0$ ).

There are a few important facts that we will need about excellent hybrid premice that one can prove by using more or less standard ideas, and that in one form or another have appeared in [Reference Sargsyan and Trang38]. We will use the next subsection recording some of these facts.

2.5. More on self-iterability

Here, we prove that window-based strategy acts on the entire model. The main theorem that we would like to prove is the following.

The proof will be presented as a sequence of lemmas. First we make a few observations. Suppose ${\mathcal {P}}$ is excellent and for some ${\mathcal {P}}$ -cardinal $\xi>{\delta }^{\mathcal {P}}$ is a limit of Woodin cardinals of ${\mathcal {P}}$ , $\pi :{\mathcal {N}}\rightarrow {\mathcal {P}}|\xi $ is an elementary embedding in ${\mathcal {P}}$ such that ${\mathcal {N}}$ is countable. It follows that $\eta =_{def}\sup (\pi [{\delta }^{\mathcal {N}}])<{\delta }^{\mathcal {P}}$ , and therefore, letting $\Lambda =(\pi $ -pullback of $S^{\mathcal {P}}$ ),

(O1) ${\mathcal {P}}{\vDash } \text {`}\Lambda ^{stc}$ is a splendid $Ord$ -strategy for ${\mathcal {N}}_0^{\prime }$ ,Footnote ⁴⁶

(O2) ${\mathcal {P}}{\vDash } \text {"}{\mathcal {N}}$ is a $\Lambda ^{stc}$ -premouse.Footnote ⁴⁷

(O3) in ${\mathcal {P}}$ , Theorem 2.4 applies to ${\mathcal {N}}$ and $\Lambda $ .

(O4) if $i:{\mathcal {N}}\rightarrow {\mathcal {N}}_1$ is such that $\mathrm {crit }(i)>{\delta }^{\mathcal {N}}$ , and for some $\sigma :{\mathcal {N}}_1\rightarrow {\mathcal {P}}|\xi $ , $\pi =\sigma \circ i$ , then ${\mathcal {N}}_1$ is a $\Lambda ^{stc}$ -premouse.

(O4) will be key in many arguments in this paper, but often we will ignore stating it for the sake of succinctness. In each case, however, the reader can easily find the realizable embeddings. The reason (O4) is important is that without, it we cannot really prove any self-iterability results, as if iterating ${\mathcal {N}}$ above destroyed the fact that the resulting premouse is a $\Lambda ^{stc}$ -premouse. Then we could not find the relevant ${\mathcal {Q}}$ -structures using $\Lambda $ or comparison techniques.

In fact, more is true.