The domestic levels of $K^c$ are iterable


Alex Andretta, Itay Neeman, and John Steel





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.