  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.
