We prove that in all Mitchell-Steel core models, □k holds for all k. From this we obtain new consistency strength lower bounds for the failure of □k if k is either singular and countably closed, weakly compact, or measurable. Jensen introduced a large cardinal property that we call subcompactness; it lies between superstrength and supercompactness in the large cardinal hierarchy. We prove that in all Jensen core models, □k holds iff k is not subcompact.

We present a general construction of a □κ-sequence in Jensen's fine structural extender models. This construction yields a local definition of a canonical □κ-sequence as well as a characterization of those cardinals κ, for which the principle □κ fails. Such cardinals are called subcompact and can be described in terms of elementary embeddings. Our construction is carried out abstractly, making use only of a few fine structural properties of levels of the model, such as solidity and condensation.

We extend the core model induction technique to a choiceless context, and we exploit it to show that each one of the following two hypotheses individually implies that , the Axiom of Determinacy, holds in the of a generic extension of : every uncountable cardinal is singular, and every infinite successor cardinal is weakly compact and every uncountable limit cardinal is singular.