[proofplan] We use the explicit partial-construction convention from the statement: a construction stops exactly when a successor ultrapower or a limit direct limit is ill-founded. The external countable completeness hypothesis supplies well-foundedness at every reached successor stage, so the only possible obstruction to reaching all stages of a countable construction is failure of well-foundedness for the pre-collapse direct limit at a limit stage. The forward implication is therefore immediate from countable linear iterability, while the reverse implication follows by induction on the prescribed countable length of a partial construction. [/proofplan]

[step:Fix the convention for linear iteration systems] A partial countable linear measure construction of $(M,U)$ indexed by a countable ordinal $\theta$ is an attempted recursively defined construction. It consists, at every stage reached before $\theta$, of well-founded extensional models $M_i$ identified with their transitive collapses, measurable cardinals $\kappa_i$, image normal measures $U_i$ on $\kappa_i$ over $M_i$, and elementary embeddings \begin{align*} j_{ij}:M_i\to M_j \end{align*} for reached stages $i\leq j<\theta$, satisfying the recursive clauses in the statement. The assumption that $M$ has exactly one normal measure fixes the construction as linear: the successor operation is always the ultrapower by the distinguished current image measure $U_i$, and no alternative measure choice is part of the data. First, $M_0=M$, $\kappa_0=\kappa$, $U_0=U$, and $j_{00}=\operatorname{id}_{M_0}$. Second, if $i+1<\theta$ and $M_i$ has been reached, then $M_{i+1}$ is defined exactly when $\operatorname{Ult}(M_i,U_i)$ is well-founded; in that case $M_{i+1}$ is its transitive collapse, the map \begin{align*} j_{i,i+1}:M_i\to M_{i+1} \end{align*} is the collapsed ultrapower embedding, $\kappa_{i+1}=j_{i,i+1}(\kappa_i)$, and $U_{i+1}=j_{i,i+1}(U_i)$ is the image normal measure on $\kappa_{i+1}$ over $M_{i+1}$. Third, if $\lambda<\theta$ is a limit ordinal and all stages below $\lambda$ have been reached, then $D_\lambda$ denotes the pre-collapse direct limit of the directed system \begin{align*} (M_i,j_{ij})_{i\leq j<\lambda}. \end{align*} The stage $\lambda$ is reached exactly when $D_\lambda$ is well-founded; in that case $M_\lambda$ denotes its transitive collapse, the embeddings $j_{i\lambda}:M_i\to M_\lambda$ are the collapsed direct-limit maps, and for any $i<\lambda$ the coherent images $\kappa_\lambda=j_{i\lambda}(\kappa_i)$ and $U_\lambda=j_{i\lambda}(U_i)$ are the direct-limit measurable cardinal and measure. If a required successor ultrapower or limit direct limit is ill-founded, the attempted construction stops at that first obstruction and no later stages are reached. With this convention, countable linear iterability of $(M,U)$ means precisely that every such partial construction reaches every stage below its prescribed countable ordinal length. [/step]

[step:Use countable completeness to secure every successor ultrapower]Suppose $i$ is a reached stage for which $M_i$ is well-founded and has been identified with its transitive collapse. By the construction convention, $U_i\in M_i$ is a normal measure, hence in particular an ultrafilter on the measurable cardinal $\kappa_i$ over $M_i$, and the ultrapower $\operatorname{Ult}(M_i,U_i)$ is the usual internal ultrapower formed from functions $f:\kappa_i\to M_i$ with $f\in M_i$. Its [equivalence relation](/page/Equivalence%20Relation) is equality on a set in $U_i$, and its membership relation is the relation induced by membership on a set in $U_i$. By hypothesis, applied to this reached stage $i$ before the attempted successor step $i+1$, $U_i$ is externally countably complete over $M_i$. The standard ultrapower well-foundedness lemma says that if a well-founded extensional structure $N$ carries an ultrafilter $W\in N$ over $N$ and $W$ is externally countably complete over $N$, then the ultrapower of $N$ by $W$ using functions in $N$ is well-founded. The hypotheses of this lemma are satisfied here: $M_i$ is well-founded and extensional by construction, $U_i\in M_i$ is an ultrafilter on $\kappa_i$ over $M_i$, the ultrapower is formed using functions $f:\kappa_i\to M_i$ belonging to $M_i$ with the usual ultrapower relations, Łoś's theorem applies to this internal ultrapower after $M_i$ has been collapsed, and external countable completeness of $U_i$ over $M_i$ is assumed. Applying the lemma to $N=M_i$ and $W=U_i$, the ultrapower $\operatorname{Ult}(M_i,U_i)$ is well-founded. Therefore its transitive collapse exists, so $M_{i+1}$ and the collapsed ultrapower embedding $j_{i,i+1}:M_i\to M_{i+1}$ are defined. Here and below we are using the following prerequisite result, written in plain prose because its database theorem ID has not been supplied: countable completeness implies well-founded ultrapower.[/step]

[guided]Assume that the iteration has reached a stage $i$ and that $M_i$ is already well-founded. Since $M_i$ is well-founded, we identify it with its transitive collapse; this makes the phrase “externally countable sequence of members of $U_i$ with each member in $M_i$” meaningful in the ambient universe. The hypothesis says that $U_i$ is externally countably complete over $M_i$: whenever \begin{align*} (X_n)_{n<\omega} \end{align*} is an externally countable sequence with $X_n\in U_i\cap M_i$ for every $n<\omega$, the intersection satisfies \begin{align*} \bigcap_{n<\omega}X_n\neq\varnothing. \end{align*} This is exactly the countable completeness condition needed in the standard ultrapower well-foundedness argument. To see the mechanism, suppose toward a contradiction that the ultrapower had a descending membership chain. Choose representatives $f_n:\kappa_i\to M_i$ with $f_n\in M_i$ for the $n$th element of the chain. For each $n<\omega$, define \begin{align*} A_n=\{\alpha\in\kappa_i:f_{n+1}(\alpha)\in f_n(\alpha)\}. \end{align*} Because $f_n$ and $f_{n+1}$ belong to $M_i$, and because $M_i$ is a premouse with internal separation for the defining formula $f_{n+1}(\alpha)\in f_n(\alpha)$, the set $A_n$ belongs to $M_i$. By Łoś's theorem for the ultrapower, each $A_n$ belongs to $U_i$. Since the sequence $(A_n)_{n<\omega}$ is externally countable and each $A_n\in U_i\cap M_i$, external countable completeness gives an ordinal $\alpha_*\in\bigcap_{n<\omega}A_n$. For this single $\alpha_*$, the sequence \begin{align*} f_0(\alpha_*), f_1(\alpha_*), f_2(\alpha_*),\dots \end{align*} is an infinite descending $\in$-chain inside the well-founded transitive model $M_i$, because $f_{n+1}(\alpha_*)\in f_n(\alpha_*)$ for every $n<\omega$. This contradicts the well-foundedness of $M_i$. Thus $\operatorname{Ult}(M_i,U_i)$ is well-founded. Since every well-founded extensional structure has a transitive collapse, we may define $M_{i+1}$ to be the transitive collapse of $\operatorname{Ult}(M_i,U_i)$. The embedding \begin{align*} j_{i,i+1}:M_i\to M_{i+1} \end{align*} is the ultrapower map followed by this collapse, and the next image measure is \begin{align*} U_{i+1}=j_{i,i+1}(U_i). \end{align*} So the successor step introduces no additional obstruction to well-foundedness.[/guided]

[step:Derive countable linear iterability from well-founded limit direct limits] Assume that every partial countable linear measure construction of $(M,U)$ has a well-founded pre-collapse direct limit at each countable limit stage whenever all earlier stages have been reached. We prove by induction on a countable ordinal $\theta$ that every partial construction prescribed up to length $\theta$ reaches all stages below $\theta$. The initial stage is well-founded because $M_0=M$ is well-founded. At a successor stage $i+1$, the induction hypothesis gives that $M_i$ has been reached and is well-founded, and the previous step gives that $\operatorname{Ult}(M_i,U_i)$ is well-founded; hence $M_{i+1}$ exists as its transitive collapse and the construction reaches $i+1$. At a limit stage $\lambda<\theta$, the induction hypothesis gives that all stages below $\lambda$ have been reached, so the directed system \begin{align*} (M_i,j_{ij})_{i\leq j<\lambda} \end{align*} is already defined. The hypothesis of this implication says exactly that its pre-collapse direct limit $D_\lambda$ is well-founded, so its transitive collapse $M_\lambda$ exists and the construction reaches $\lambda$. Thus every partial countable construction by successive image measures reaches all stages below its prescribed countable length. By the adopted definition, $(M,U)$ is countably linearly iterable. [/step]

[step:Recover the limit direct-limit condition from countable linear iterability] Conversely, assume that $(M,U)$ is countably linearly iterable. Let \begin{align*} (M_i,U_i,j_{ij})_{i\leq j<\theta} \end{align*} be any partial countable linear measure construction of $(M,U)$, and let $\lambda<\theta$ be a limit ordinal such that all stages below $\lambda$ have been reached. By countable linear iterability, the construction reaches every stage below its prescribed countable length, including the limit stage $\lambda$. But reaching $\lambda$ means, by definition of the partial construction, that the pre-collapse direct limit $D_\lambda$ of \begin{align*} (M_i,j_{ij})_{i\leq j<\lambda} \end{align*} is well-founded and that $M_\lambda$ is its transitive collapse. Therefore that direct limit is well-founded. Since the partial construction and the limit stage were arbitrary, every partial countable linear measure construction has a well-founded direct limit at each countable limit stage whose earlier stages have been reached. [/step]

[step:Conclude the equivalence] The successor stages are well-founded under the external countable completeness hypothesis, and the preceding two steps show that the remaining limit-stage condition is equivalent to countable linear iterability. Hence $(M,U)$ is countably linearly iterable if and only if every partial countable linear measure construction by successive image measures has a well-founded pre-collapse direct limit at each countable limit stage whose earlier stages have been reached. [/step]