Kunen critical sequence ($⟨j^n(\kappa ):n<\omega ⟩$)

The critical sequence of $j$ starts with its critical point $\kappa$ and iterates ${\kappa }_{n+1}=j({\kappa }_n)$. Its supremum $\hat{\kappa }={\sup }_{n<\omega }{j}^n(\kappa )$ is the least fixed point of $j$ above $\kappa$ whenever the relevant iterates lie in the domain.

For an elementary embedding with critical-sequence supremum $\hat{\kappa }$, the setdoes not belong to the transitive target model. The proof uses an omega-Jonsson function on $\hat{\kappa }$.