Let \delta = (w, \Diamond_h \varphi) be a horizontal defect of \mathfrak{m} and let \sigma : |\mathfrak{m}| \to W^{\rm c} be the simulation such that \mathfrak{m} \rightharpoonup \Phi. We define recursively a sequence \{(\mathfrak{m}_i, e_i, \sigma_i)\}_{i \in \mathbb{N}} such that, for each i \in \mathbb{N}, \mathfrak{m}_i is a \Sigma-quasimoment, e_i is a partial embedding, and \sigma_i : |\mathfrak{m}_i| \to W^{\rm c} is a simulation satisfying
\sigma(u) \prec_h^{\rm c} \sigma_i(e_i(u)) \quad \text{for all } u \in \mathrm{Dom}(e_i)
where \mathrm{Dom}(e_i) denotes the domain of the partial embedding e_i.
We first define \mathfrak{m}_0 := (\{w'\}, \prec_v^0, \ell^0), where \prec_v^0 := \emptyset and \ell^0(w') := \Psi \cap \Sigma for some \Psi \in W^{\rm c} such that \Psi \succ_h^{\rm c} \sigma(w), obtained by the witness Lemma 5.3 from the fact that \Diamond_h \varphi \in \ell^{\mathfrak{m}}(w) = \sigma(w) \cap \Sigma. Define e_0(w) := w' and \sigma_0(w') := \Psi.
Given (\mathfrak{m}_i, e_i, \sigma_i), we construct (\mathfrak{m}_{i+1}, e_{i+1}, \sigma_{i+1}) by extending \mathfrak{m}_i, e_i, and \sigma_i as follows:
For each v \in |\mathfrak{m}| \setminus \mathrm{Dom}(e_i) such that either v is an immediate \prec_v^{\mathfrak m}-predecessor or an immediate \prec_v^{\mathfrak m}-successor of some u\in\mathrm{Dom}(e_i), that is,
v \prec_v^{\mathfrak m} u
\quad\text{and there is no }w \neq u, v \text{ with }
v \prec_v^{\mathfrak m} w \prec_v^{\mathfrak m} u
or
u \prec_v^{\mathfrak m} v
\quad\text{and there is no }w \neq u, v\text{ with }
u \prec_v^{\mathfrak m} w \prec_v^{\mathfrak m} v,
we add a fresh node v' and extend e_i by setting e_{i+1}(v):=v'. The position of v' in \mathfrak{m}_{i+1} is determined by:
(i) v' \prec_v^{{i+1}} e_i(u) if v \prec_v^{\mathfrak{m}} u;
(ii) v' \succ_v^{{i+1}} e_i(u) if v \succ_v^{\mathfrak{m}} u.
Using the properties (LC) and (CR) of the canonical model, we define the label and simulation for v' by setting \ell^{{i+1}}(v') := \Upsilon \cap \Sigma and \sigma_{i+1}(v') := \Upsilon, where \Upsilon \in W^{\rm c} satisfies one of the following conditions:
(i) \sigma(v) \prec_h^{\rm c} \Upsilon \prec_v^{\rm c} \sigma_i(e_i(u)) by the property (LC) if v \prec_v^{\mathfrak{m}} u given that \sigma(v) \prec_v^{\rm c} \sigma(u) \prec_h^{\rm c} \sigma_i(e_i(u));
(ii) \sigma(v) \prec_h^{\rm c} \Upsilon \succ_v^{\rm c} \sigma_i(e_i(u)) by the property (CR) if v \succ_v^{\mathfrak{m}} u given that \sigma(v) \succ_v^{\rm c} \sigma(u) \prec_h^{\rm c} \sigma_i(e_i(u)).
The paper has a figure here, which this page does not show.
First, we show that the construction is well-defined.
Claim. The sequence \{(\mathfrak{m}_i, e_i, \sigma_i)\}_{i \in \mathbb{N}} is well-defined.
Proofof. Claim ? More precisely, we show for every i \in \mathbb{N} that
\mathrm{Dom}(e_i) \subseteq |\mathfrak{m}| equipped with the relation \prec_v^{\mathfrak{m}} restricted to it forms a tree;
e_i : \mathrm{Dom}(e_i) \to |\mathfrak{m}_i| is a \prec_v-isomorphism such that \mathrm{Im}(e_i) = |\mathfrak{m}_i|, where \mathrm{Im}(e_i) denotes the image of e_i;
\mathfrak{m}_i is a \Sigma-quasimoment;
\sigma_i : |\mathfrak{m}_i| \to W^{\rm c} is a simulation satisfying \sigma(u) \prec_h^{\rm c} \sigma_i(e_i(u)) for every u \in \mathrm{Dom}(e_i).
The proof proceeds by induction on i \in \mathbb{N}. The base case is immediate from the construction. For the inductive step, assume that (\mathfrak{m}_i, e_i, \sigma_i) satisfies ?–?, and consider the extension to (\mathfrak{m}_{i+1}, e_{i+1}, \sigma_{i+1}) as defined in the sequence. We provide details for the first three properties, while the verification of ? follows directly from the definition of the recursive construction and is left to the reader.
? By the inductive hypothesis, \mathrm{Dom}(e_i) is a tree. The map e_{i+1} is defined to extend e_i with nodes v \in |\mathfrak{m}| \setminus \mathrm{Dom}(e_i) which are immediate \prec_v^\mathfrak{m}-predecessors or \prec_v^\mathfrak{m}-successors of some u \in \mathrm{Dom}(e_i), together with the edge witnessing this relation. If v \succ_v^\mathfrak{m} u, it is straightforward that the extension is still a tree. Otherwise, if v \prec_v^\mathfrak{m} u, since v \notin \mathrm{Dom}(e_i) but u \in \mathrm{Dom}(e_i), we deduce that u is the root of the tree \mathrm{Dom}(e_i). Therefore, we have the extension is also a tree for this case.
? By construction, every new node v' of \mathfrak{m}_{i+1} arises from a unique v \in |\mathfrak{m}| \setminus \mathrm{Dom}(e_i) which is immediate adjacent (in the \prec_v-tree structure) to some u \in \mathrm{Dom}(e_i). This element v is added to the domain of e_{i+1} and mapped to v' via e_{i+1}(v) := v', so that \mathrm{Im}(e_{i+1}) = |\mathfrak{m}_{i+1}|. Since e_i is a \prec_v-isomorphism by the inductive hypothesis and the construction introduces fresh nodes exactly corresponding to previously unmapped elements while respecting adjacency in the tree structure, it follows that e_{i+1} is again bijective. Moreover, the extension is defined so as to preserve the \prec_v-relation, and therefore e_{i+1} is a \prec_v-isomorphism.
? By ?, \mathrm{Dom}(e_{i+1}) is a tree, and by ? so is (|\mathfrak{m}_{i+1}|, \prec_v^{i+1}). It remains to verify that the labelling satisfies the homomorphism condition: this follows from the inductive hypothesis together with the definition of the labels of the newly added nodes and the transitivity properties of maximal consistent sets. The details are routine and left to the reader.
Next, we show that the sequence stabilizes, meaning that it is eventually constant at some element, which we call its limit.
Claim. The sequence \{(\mathfrak{m}_i, e_i, \sigma_i)\}_{i \in \mathbb{N}} stabilizes.
Proofof. Claim ? Since the construction properly extends by adding fresh nodes corresponding to nodes in \mathfrak{m} that are not in the domain of the corresponding embedding, it suffices to show that there exists k \in \mathbb{N} such that \mathrm{Dom}(e_k) = |\mathfrak{m}|.
To this end, observe that \mathrm{Dom}(e_i) \subseteq \mathrm{Dom}(e_{i+1}) for all i \in \mathbb{N} by a straightforward induction on i \in \mathbb{N}. Moreover, whenever \mathrm{Dom}(e_i) \subsetneq |\mathfrak{m}|, the construction adds at least one new element, so that \mathrm{Dom}(e_i) \subsetneq \mathrm{Dom}(e_{i+1}). Therefore, since |\mathfrak{m}| is finite, there exists k \in \mathbb{N} such that \mathrm{Dom}(e_k) = |\mathfrak{m}|, and the sequence stabilizes.
Let (\hat{\mathfrak{m}}, \hat{e}, \hat{\sigma}) denote the limit of the sequence \{(\mathfrak{m}_i, e_i, \sigma_i)\}_{i \in \mathbb{N}}. We show that this limit is already a successor realizing the horizontal defect \delta, and that it simulates a maximal consistent set that is a horizontal successor of the one simulated by \mathfrak{m}.
Claim. \hat{\mathfrak{m}} is a successor of \mathfrak{m} realizing \delta.
\hat{\mathfrak{m}} \rightharpoonup \Phi' for some \Phi' \succ_h^{\rm c} \Phi.
Proofof. Claim ?
?. It suffices to show that \mathfrak{m} ,\prec_h^\Sigma, \hat{\mathfrak{m}} via the embedding \hat{e}. Once this is established, we obtain that \varphi \in \ell^{\hat{\mathfrak{m}}}(\hat{e}(w)), since \varphi \in \ell^{i}(e_i(w)) for every i \in \mathbb{N}. The latter fact follows by a straightforward induction on i, whose details are left to the reader.
As observed in Claim ?, we have \mathrm{Dom}(\hat{e}) = |\mathfrak{m}|, so \hat{e} : |\mathfrak{m}| \to |\hat{\mathfrak{m}}| is a (total) embedding. To verify that \mathfrak{m} \,\prec_h^\Sigma\, \hat{\mathfrak{m}}, let \Diamond_h \psi \in \Sigma and suppose that either \psi \in \ell^{\hat{\mathfrak{m}}}(\hat{e}(u)) or \Diamond_h \psi \in \ell^{\hat{\mathfrak{m}}}(\hat{e}(u)) for some u \in |\mathfrak{m}|. Since \ell^{\hat{\mathfrak{m}}}(\hat{e}(u)) = \hat{\sigma}(\hat{e}(u)) \cap \Sigma and \sigma(u) \prec_h^{\rm c} \hat{\sigma}(\hat{e}(u)), it follows from the definition of \prec_h^{\rm c} that either \Diamond_h \psi \in \sigma(u) or \Diamond_h \Diamond_h \psi \in \sigma(u). In the latter case, by transitivity and maximal consistency we also obtain \Diamond_h \psi \in \sigma(u). Hence, in both cases we have that \Diamond_h \psi \in \sigma(u), and therefore we conclude \Diamond_h \psi \in \ell^{\mathfrak{m}}(u).
?. Let \Phi' := \hat{\sigma}(r^{\hat{\mathfrak{m}}}). Since r^{\hat{\mathfrak{m}}} = \hat{e}(r^{\mathfrak{m}}), and recalling that \sigma(r^{\mathfrak{m}}) = \Phi, it follows from the construction that \Phi' \succ_h^{\rm c} \Phi. Hence \hat{\mathfrak{m}} \rightharpoonup \Phi' as required.
Finally, we extend the \Sigma-quasimoment \hat{\mathfrak{m}} to a \Sigma-moment \mathfrak{m}' such that \mathfrak{m}' \rightharpoonup \Phi' using Lemma 7.4. Moreover, \hat{e} : |\mathfrak{m}| \to |\mathfrak{m}'| witnesses that \mathfrak m\prec_h^\Sigma \mathfrak m', showing that \mathfrak{m}' realizes the horizontal defect \delta. This concludes the proof.