Does non-well-foundedness of a model imply a decreasing sequence of ordinals? (Jech, Theorem 19.7) Theorem 19.7 (by Gaifman) is the following result:

Let $U$ be a $\kappa$-complete nonprincipal ultrafilter on $\kappa$. Then for every $\alpha$, the $\alpha$th iterated ultrapower $\operatorname{Ult}^{(\alpha)}$ is well-founded.

The first paragraph of the proof states the following:

Clearly if $\operatorname{Ult}^{(\alpha)}$ is well-founded, then $\operatorname{Ult}^{(\alpha+1)}$ is well-founded. Thus if $\gamma$ is the least $\gamma$ such that $\operatorname{Ult}^{(\gamma)}$ is not well-founded, then $\gamma$ is a limit ordinal.The ordinals of the model $\operatorname{Ult}^{(\gamma)}$ are not well-ordered; let $\xi$ be the least ordinal such that the ordinals of $\operatorname{Ult}^{(\gamma)}$ below $i_{0,\gamma}(\xi)$ are not well-founded.

My question is: How do we know that the ordinals of the model $\operatorname{Ult}^{(\gamma)}$ is not well-ordered? The naive approach is to take a decreasing sequence of sets $x_0 \ni x_1 \ni \cdots$, then take rank to yield $\operatorname{rank}(x_0) > \operatorname{rank}(x_1) > \cdots$, but I don't think $\operatorname{rank}$ is defined for non-well-founded models.
Any help is appreciated.
 A: There are two ways in which well-foundedness can fail.

*

*Internally, where the model knows that it fails, i.e. the axiom of foundation is false in the model.


*Externally, where the model thinks that the axiom of foundation is true, but we know from outside the model that the relation is not really well-founded.
In the latter case you do have a rank function, since the rank function is internal, and there are no decreasing sequences of ordinals in that model. But externally there is a decreasing sequence nonetheless.
This is akin to non-standard models of $\sf PA$. The model is not well-ordered, and we know that, but the induction axioms are equivalent to stating that any definable set which is not empty has a least element, so this is not something the model knows about.
Note that in the context of ultrapowers, the models are all models of $\sf ZFC$, or a significant fragment thereof which contains the axiom of foundation, and therefore they are all going to fall into the second category.
Consider, if you will, a free ultrafilter $U$ on $\omega$, and consider $V^\omega/U$. This is a definable class, with $E$ denoting its membership relation also being definable. This is an ultrapower of the universe. But it is not well-founded, externally, since $\omega^\omega/U$ is already not well-ordered.
(In the former case you will have a witness that is not well-founded, yes. And the ordinals may or may not be well-founded.)
