The maximality of the core model

If T is an iteration tree on K and F is a countably certified extender that coheres with the final model of T, then F is on the extender sequence of the final model of T. Several applications of maximality are proved, including: o K computes successors of weakly compact cardinals correctly. o K^c is an iterate of K. o (with Mitchell) If alpha is a cardinal > aleph_1, then K-restriction-alpha is universal for mice of height alpha. Other results in this paper, when combined with work of Woodin, imply: o If square-kappa-finite fails and kappa is a singular, strong limit cardinal, then Inductive Determinacy holds. o If square-kappa-finite fails and kappa is a weakly compact cardinal, then L(R)-determinacy holds.