Alex Andretta, Itay Neeman,
and John Steel
Abstract:
We show that the models
produced by the $K^c$ construction
before (if ever) it reaches
a non-domestic premouse are all
iterable. As a corollary we
get that {\sf PFA} plus the
existence of a measurable
cardinal implies the existence of
a non-domestic premouse.