Proof. For \(k=1\), a set of cardinality greater than \(\xi\cdot\nu\) cannot be partitioned into \(\xi\) sets all of cardinality less than \(\nu\). Suppose the assertion is known for \(k\). Choose an infinite initial ordinal \(\alpha\) large enough for that \(k\)-ary assertion with target \(\nu\), and put \(b=\xi^{|\alpha|}\). Consider a coloring \(c\) of the \((k+1)\)-element subsets of an ordinal \(\Omega\) with \(|\Omega|>b\).

Construct a tree of residual subsets of \(\Omega\) through height \(\alpha\). Its root is \(\Omega\). At a nonempty node, name and remove its least point \(x\). The previously named points on its branch, together with \(x\), form an increasing sequence. Partition the remaining residual set according to all values \[u\longmapsto c(s\cup\{u\}), \qquad s\text{ a $k$-subset of that sequence}.\] The nonempty parts are the children. At a limit height, a branch has as its residual set the intersection of the earlier residual sets; retain the node precisely when this intersection is nonempty.

At each node there are at most \(|\alpha|\) coordinates to record and hence at most \(b\) children. The total number of possible nodes through height \(\alpha\) is at most \(b^{|\alpha|}=b\). This includes the limit nodes, which are specified by their branches. At most \(b\) points are removed as node labels. Choose \(u\in\Omega\) which is never removed. At every height it belongs to one residual set; at limit heights it belongs to the intersection on that branch. Consequently it determines a branch with \(\alpha\) named points and nonempty remainder.

For every \(k\)-subset \(s\) of these named points, all later named points give the same value of \(c(s\cup\{x\})\): that value was fixed by the partition immediately after the last point of \(s\) was named. Therefore \(c\) on increasing \((k+1)\)-tuples from the branch depends only on their first \(k\) entries. Apply the \(k\)-ary induction hypothesis to this induced coloring on the branch. Its homogeneous \(\nu\)-subset is homogeneous for \(c\) as well. For example, the recursion just proved allows \(R_{k+1}(\xi,\nu)=(\xi^{R_k(\xi,\nu)})^+\) after increasing the initial \(R_1\) as needed.

For a finite list of arities, work backward to choose a bound large enough for the last desired thinning after all the earlier ones. Successive thinning preserves homogeneity already obtained. This proves the final assertion. ◻

Proof. Take an arbitrarily large \(M\in K\) and distinct elements \((a_i)_{i\in A}\) indexed by a large ordinal \(A\). Recursively on the positive finite size of \(s\subseteq A\), choose \(M_s\leq_KM\) of cardinality at most \(\ell\) containing the displayed elements on \(s\) and every \(M_t\) for nonempty \(t\subsetneq s\). There are only finitely many such \(t\), so the LS axiom applies with bound \(\ell\). Coherence gives \(M_t\leq_KM_s\).

Choose a surjective enumeration \((m_{s,\eta})_{\eta<\ell}\) of each \(M_s\), allowing repetitions. If \(s=\{i_0<\cdots<i_{n-1}\}\), require \(m_{s,j}=a_{i_j}\) for \(j<n\). For an \(n\)-element set \(s\), its color is the complete atomic diagram, including negations and equalities, of all the enumerations \[(m_{t,\eta})_{\eta<\ell}, \qquad \varnothing\ne t\subseteq s,\] with the subsets of \(s\) named by their relative positions. This diagram includes formulas involving entries from different enumerations. There are at most \(\ell\) names and atomic formulas for each fixed \(n\), so its possible colors belong to a fixed set of cardinality at most \(2^\ell\).

We choose colors \(d_n\), for \(n\geq1\), so that for every finite \(n\) there are samples of arbitrarily large cardinality homogeneous in colors \(d_1,\ldots,d_n\). Suppose \(d_1,\ldots,d_{n-1}\) have been chosen with this property. For any prescribed target cardinal, choose such a sample large enough for Lemma 8 at arity \(n\) and thin it to an \(n\)-homogeneous set of the target cardinality. The earlier colors are retained. If every possible \(n\)-color supported only boundedly large such thinnings, the supremum of the bounds over the set of colors would bound all thinnings, a contradiction. Thus one color \(d_n\) supports arbitrarily large thinnings. It restricts on every smaller subset to the previously chosen colors. This proves the recursion and its coherence. It asserts finite-stage realizability in arbitrarily large samples; it does not require an infinite simultaneous homogeneous set inside one sample.

For a nonempty linear order \(I\), introduce symbols \((s,\eta)\) for each finite nonempty \(s\subseteq I\) and \(\eta<\ell\), with \(s\) listed increasingly. Equate \((s,\eta)\) and \((t,\zeta)\) when the color \(d_{|s\cup t|}\) says that the corresponding entries are equal. Coherence makes this independent of passage to a larger finite set of indices. Reflexivity, symmetry, and transitivity hold because any finite instance occurs in a realized color. Form the quotient by this equivalence relation.

Interpret a relation on finitely many quotient elements in a color on the union of their supports. For a function symbol, evaluate it in the enumerated model on that union and use a name for its value. All its arguments belong to that enumerated model, and the model is a substructure, so the value has such a name. Changing representatives or enlarging the finite support gives the same quotient element by the complete atomic diagram and coherence. A constant can be evaluated using any one nonempty finite support. Two such evaluations agree in a color on their union. Thus these rules define a \(\tau\)-structure \(E(I)\).

Let \(E_s(I)\) consist of the elements named by \((s,\eta)\), \(\eta<\ell\). The color \(d_{|s|}\) makes this a full enumerated copy of one of the actual models \(M_s\) in a sample. Names with support \(t\subseteq s\) are included in this copy: their equalities with names in the enumeration on \(s\) were recorded. If \(s\subseteq u\), the pair \(E_s(I)\subseteq E_u(I)\) is isomorphic to an actual pair \(M_s\leq_KM_u\) from a realization of \(d_{|u|}\). Isomorphism invariance therefore makes the inclusion strong. The family of these small models is directed and covers the constructed structure. Its directed union belongs to \(K\), with all \(E_s(I)\leq_KE(I)\).

For an order embedding \(f:I\longrightarrow J\), substitution \((s,\eta)\mapsto(f[s],\eta)\) respects every defining diagram and every inequality of names. It therefore induces an embedding \(E(f):E(I)\longrightarrow E(J)\). On each finite-support model it is an isomorphism onto \(E_{f[s]}(J)\leq_KE(J)\). The common-upper-bound clause applied to their directed union shows that the whole image is strong in \(E(J)\). Substitution also proves \(E(\mathop{\mathrm{id}})=\mathop{\mathrm{id}}\) and \(E(g\circ f)=E(g)\circ E(f)\).

Define \(a_i\) by the first designated name on the singleton \(\{i\}\). The recorded equalities identify this with the designated name for \(i\) on any larger finite support. Distinct indices give distinct elements because every relevant sample had that property. The labels are indexed by \((n,\eta)\) with \(n\geq1\) finite and \(\eta<\ell\), so there are at most \(\ell\) of them. Counting finite supports proves the upper bound on size, and the distinct displayed elements prove the lower bound. ◻

Proof. Finite-support counting gives \(|\Gamma_\delta|=|H(\delta)|=|\delta|\). The group \(\Gamma_\delta\) has least positive element \(e_0\), so every \(g\) has predecessor \(g-e_0\). Its cofinality and coinitiality are both \(\mathop{\mathrm{cf}}(\delta)\). Indeed, the vectors \(e_\alpha\) for \(\alpha\) in a cofinal subset of \(\delta\) are cofinal, and their negatives are coinitial. The supports of fewer than \(\mathop{\mathrm{cf}}(\delta)\) vectors are bounded in \(\delta\), so such a family is neither cofinal nor coinitial.

The order \(H(\delta)\) is a divisible nonzero ordered abelian group, and hence is dense and has no endpoints. If \((g_i)\) is coinitial in \(\Gamma_\delta\), then \((u_{g_i})\) is coinitial in the positive cone of \(H(\delta)\): given a positive vector of rank \(g\), choose \(g_i<g\). Conversely, the ranks of fewer than \(\mathop{\mathrm{cf}}(\delta)\) positive vectors have a strict lower bound in \(\Gamma_\delta\), and a positive basis vector at that lower rank lies below all of them. Thus the positive cone has coinitiality \(\mathop{\mathrm{cf}}(\delta)\). Translation and negation give that character at every point on both sides.

Translations move points and therefore identify rays of a fixed direction. We show that any positive vector can be sent to any other by an increasing automorphism. First translate the index group \(\Gamma_\delta\) so that their greatest support coordinates agree, say at \(g\). Write the two vectors as \[a u_g+v,\qquad b u_g+w, \qquad a,b\in\mathbb Q_{>0},\quad \mathop{\mathrm{rk}}(v),\mathop{\mathrm{rk}}(w)<g,\] allowing zero lower parts. Fix all other basis vectors and replace \(u_g\) by \[\frac ba u_g+\frac{w-v}{a}.\] This is an invertible triangular rational-linear map. It preserves the sign of every nonzero vector, since it either fixes the greatest nonzero coordinate or multiplies its coefficient by \(b/a>0\). It sends the first displayed vector to the second. Combining this map with translations sends any ordered pair of distinct points to any other such pair. Restricting gives the interval assertion.

Finally, an increasing map on ordinal positions preserves the greatest differing position of two integer vectors. The induced map on these integer vectors preserves the greatest differing position of rational vectors as well. This proves the embedding claim. Expanding the finitely many integer-vector positions used by a rational vector gives the asserted finite code and comparison rule. ◻

Proof. First consider a cut \((L,R)\) of \(\Gamma_\delta\). Among the ranks of \(r-l\), with \(l\in L\) and \(r\in R\), choose the least ordinal \(\alpha\). Fix one crossing pair of that rank and its common head above \(\alpha\). In that head, each fiber with a fixed integer coefficient at \(\alpha\) lies wholly on one side: a crossing pair within a fiber would have smaller rank. The resulting cut in the integer coefficients separates two adjacent integers. A point with a head above the fixed head would exceed the fixed upper point, and a point with a head below it would precede the fixed lower point. The two bordering fibers are therefore cofinal and coinitial toward the original cut, and their tails are copies of \(\mathbb Z^{(\alpha)}\). Their end characters agree by negation in that tail group. The case \(\alpha=0\) would give a last lower and a first upper point, and is excluded. This proves balance in \(\Gamma_\delta\).

Now let \((L,R)\) be an interior nonprincipal cut of \(H=H(\delta)\), and put \[T=\{\mathop{\mathrm{rk}}(r-l):l\in L,\ r\in R\}\subseteq\Gamma_\delta.\] This is a final segment: from a crossing pair of rank \(g\), subtract a positive basis vector at any \(h>g\) from its lower point. The new pair still crosses and has rank \(h\).

Suppose first that \(T\) has a least member \(g\). Fix a crossing head above \(g\). Every fiber with a fixed rational coefficient at \(g\) lies on just one side of the cut. Otherwise a crossing difference would have rank below \(g\). The induced cut of \(\mathbb Q\) is nonempty and proper. If neither coefficient side has a nearest rational, countable rational approximations are cofinal and coinitial in the original cut. If the lower coefficients have a greatest member, the entire fiber at that coefficient lies on the lower side and is cofinal there. Its tail, supported below \(g\), has greatest available rank \(g-e_0\), and the vectors \(n u_{g-e_0}\) and \(-n u_{g-e_0}\) show that both its end characters are \(\aleph_0\). On the upper side, rational coefficients decreasing to the greatest lower coefficient give coinitiality \(\aleph_0\). If instead the upper coefficients have a least member, the reversed calculation gives cofinality and coinitiality \(\aleph_0\). These cases exhaust the rational cuts, so the original cut is balanced.

Suppose that \(T\) has no least member, and let \(\epsilon=\mathop{\mathrm{ci}}(T)\). Put \(S=\Gamma_\delta\setminus T\) and let \(H_S\) be the subgroup supported on \(S\). We prove that the lower character is \(\epsilon\) by separating two cases.

Assume there is \(l\in L\) for which \[\{\mathop{\mathrm{rk}}(r-l):r\in R\} \quad\text{is coinitial in }T.\] The coset \(l+H_S\) is contained in \(L\), since a crossing within it would have rank in \(S\). It is cofinal in \(L\). In fact, if a point \(l'\in L\) lay above the entire coset, \(l'-l\) would have positive rank \(h\in T\). Choose \(r\in R\) with \(\mathop{\mathrm{rk}}(r-l)<h\). Then \(r-l<l'-l\), contradicting \(r>l'\). The set \(S\) is nonempty, since otherwise the cofinal coset would be the singleton \(\{l\}\). It has no greatest member: if \(s\) were greatest, \(s+e_0\) would be the least member of \(T\). Balance in \(\Gamma_\delta\), applied to \((S,T)\), gives \(\mathop{\mathrm{cf}}(S)=\epsilon\). The cofinality of \(H_S\) at its upper end equals \(\mathop{\mathrm{cf}}(S)\). A cofinal set of ranks gives cofinal positive basis vectors, while fewer ranks are bounded and cannot give a cofinal family of vectors. Hence \(\mathop{\mathrm{cf}}(L)=\epsilon\) in this case.

In the other case, each \(l\in L\) has a bound \(t_l\in T\) strictly below all ranks \(\mathop{\mathrm{rk}}(r-l)\), \(r\in R\). Choose crossing pairs \((l_i,r_i)\), \(i<\epsilon\), whose ranks are coinitial in \(T\). For fixed \(l\in L\), choose \(i\) with \(\mathop{\mathrm{rk}}(r_i-l_i)\leq t_l\). If \(l_i\leq l\), then \(0<r_i-l\leq r_i-l_i\), whence \(\mathop{\mathrm{rk}}(r_i-l)\leq\mathop{\mathrm{rk}}(r_i-l_i)\leq t_l\), a contradiction. Thus \((l_i)_{i<\epsilon}\) is cofinal in \(L\). If fewer than \(\epsilon\) points of \(L\) were cofinal, their bounds \(t_l\) would have a common strict lower bound in \(T\), since \(\epsilon=\mathop{\mathrm{ci}}(T)\). A crossing pair below that bound would have its lower point above all those points by the same calculation. This is impossible, proving \(\mathop{\mathrm{cf}}(L)=\epsilon\).

Apply the proved lower-side calculation after negating the order and exchanging \(L\) and \(R\). Negation preserves every difference rank, so it has the same \(T\) and \(\epsilon\). It yields \(\mathop{\mathrm{ci}}(R)=\epsilon\). This proves balance also in the no-least-rank case. ◻

Proof. We prove both directions simultaneously by induction on the infinite regular cardinal \(\epsilon\). Consider two lower-side segments and choose strictly increasing sequences \((p_i)_{i<\epsilon}\) and \((q_i)_{i<\epsilon}\) cofinal in their respective cut sides, with the indicated endpoints at index zero. At a stage \(i<\epsilon\), fewer than \(\epsilon\) preceding points are not cofinal, so one can choose the next point above them and above the next point of a fixed cofinal sequence. This gives the required strictly increasing sequences.

Partition the first segment into blocks as follows: \[B_0=\{p_0\},\qquad B_{j+1}=(p_j,p_{j+1}].\] For a nonzero limit \(i<\epsilon\), set \[D_i=\{x\in L:(\exists j<i)\ x\leq p_j\},\quad U_i=L\setminus D_i,\quad \mathfrak c_i=(D_i,U_i),\quad B_i=(\mathfrak c_i,p_i].\] The cut \(\mathfrak c_i\) is interior and nonprincipal. Its lower side has no greatest point and has cofinality \(\mathop{\mathrm{cf}}(i)\): the strictly increasing \(i\)-sequence is cofinal there, and any smaller proposed cofinal family would give a cofinal set of indices in \(i\). Its upper side contains \(p_i\). If that side had a least point \(u\), the earlier sequence would give \(\mathop{\mathrm{cf}}(L_{<u})=\mathop{\mathrm{cf}}(i)<\kappa\), contradicting point character. Balance therefore gives \(\mathfrak c_i\) character \(\mathop{\mathrm{cf}}(i)\) on both sides. Since \(i<\epsilon\), this is a regular cardinal strictly below \(\epsilon\).

Make the corresponding blocks from the \(q_i\). Successor blocks are isomorphic by bounded-interval homogeneity, adjoining their greatest points. At a nonzero limit index \(i\), use the upper-side induction assertion at \(\mathop{\mathrm{cf}}(i)\) to match the blocks. Match the singleton blocks at zero. These are ordered partitions of the two segments. Indeed, for any point in the first segment take the least \(i\) such that it is at most \(p_i\); the three cases for \(i\) put it in exactly the block just specified. Gluing the block maps proves the lower-side assertion.

For the upper-side assertion choose strictly decreasing coinitial sequences. The blocks are \(\{p_0\}\) and \([p_{j+1},p_j)\) at successors. At a nonzero limit \(i\), put \[V_i=\{x\in L:(\exists j<i)\ p_j\leq x\},\qquad W_i=L\setminus V_i,\qquad \mathfrak d_i=(W_i,V_i).\] The set \(V_i\) has no least point and has coinitiality \(\mathop{\mathrm{cf}}(i)\). The set \(W_i\) contains \(p_i\); if it had a greatest point, that point’s upper character would be \(\mathop{\mathrm{cf}}(i)<\kappa\). Thus \(\mathfrak d_i\) is nonprincipal, and balance gives character \(\mathop{\mathrm{cf}}(i)\) on both sides. The block at \(i\) is \([p_i,\mathfrak d_i)\), to which the lower-side induction assertion at \(\mathop{\mathrm{cf}}(i)\) applies. The least index with \(p_i\leq x\) verifies that these blocks, in reverse index order, partition the upper-side segment. For \(\epsilon=\aleph_0\) there are no nonzero limit indices below \(\epsilon\), so this simultaneous induction starts with just the successor blocks. All displayed endpoint points are matched. ◻

Proof. Necessity follows from preservation of order. For sufficiency, the order/equality diagrams give an increasing bijection \(f:A\longrightarrow B\) between the sets of distinct entries, matching the indexed sequences. We extend it separately on each occupied slot.

Choose a point \(p\) in a slot over \(A=A^-\sqcup A^+\). The portion of the slot at or below \(p\) has one of three forms. If \(A^-=\varnothing\), it is \((-\infty,p]\). If \(A^-\) has greatest member \(a\), it is \((a,p]\). Otherwise put \[D=\{x:(\exists a\in A^-)\ x\leq a\},\qquad U=H(\delta)\setminus D.\] The cut \((D,U)\) has no greatest lower point, has \(p\) on its upper side, and has lower character \(\mathop{\mathrm{cf}}(A^-)\leq\theta\). Its upper side has no first point, since such a point would have character at most \(\theta\). By Lemma 12 this is an interior nonprincipal cut of balanced character \(\mathop{\mathrm{cf}}(A^-)\). The slot portion is \(((D,U),p]\).

In the first case its type is fixed by ray homogeneity; in the second case by bounded-interval homogeneity; in the third case by Lemma 13. The portion at or above \(p\) has the corresponding classification using \(A^+\), a least member when present, and otherwise \(\mathop{\mathrm{ci}}(A^+)\). The same descriptions show that the slot has neither endpoint.

The order map \(f\) preserves which boundary case occurs and the cofinality or coinitiality of the relevant part of \(A\). Thus the corresponding occupied slot over \(B\) has matching two halves. Choose an interior point \(q\) there and match the two halves with their common point \(p\) sent to \(q\). They glue to a slot isomorphism. The occupancy assumption ensures that empty slots also correspond. The entry sets and their occupied slots partition the whole order. Choice for this set of slots and gluing with \(f\) produce an increasing bijection of \(H(\delta)\), as required. ◻

Proof. The finitely many positions belonging to each tuple entry can be indexed in \(\theta\times\omega\). Choices of arities and labels number at most \(2^{\ell+\theta}\). The flattened order/equality diagrams number at most \(2^\theta\); their sets of cuts have size at most \(2^\theta\), and occupancy subsets number at most \(2^{2^\theta}\). The displayed generous bound therefore bounds a universal record set.

For a fixed \(\delta\) with \(\mathop{\mathrm{cf}}(\delta)>\theta\), equal records give an order automorphism matching the flattened lists by Theorem 14. Applying \(E\) gives an automorphism of the model matching the tuples. Hence a realized record determines one model orbit. Every tuple has a labeled presentation, so the number of orbits is bounded by the number of records.

For any \(\kappa\geq\max(\ell,\theta^+)\), the ordinal \(\delta=\kappa+\theta^+\), with ordinal addition here, has cardinality \(\kappa\) and cofinality \(\theta^+\). The model \(E(H(\delta))\) has cardinality \(\kappa\) and is therefore a copy of the categoricity model. This proves the bound without any condition on \(\mathop{\mathrm{cf}}(\kappa)\). ◻

Proof. Construct increasing sets \(S_i\subseteq\beta\) for \(i<\theta^+\), starting with \(S\). At a successor stage consider all strict slots over the entire well-ordered set \(S_i\). There are at most \(|S_i|+1\leq a\) of them. In each finite slot add every point; in each infinite slot add a countably infinite subset. Together with \(S_i\) this realizes every finite order/equality pattern over \(S_i\) which occurs in \(\beta\). At limits take unions. The cardinality stays at most \(a\) throughout.

Set \(T_0=\bigcup_{i<\theta^+}S_i\). Every set \(P\subseteq T_0\) of size at most \(\theta\) is contained in some \(S_i\), by regularity of \(\theta^+\). For a given finite tuple, keep any coordinates already in \(S_i\) and match its other coordinates in their respective slots using the next stage. This proves the asserted property over \(P\). Since \(|T_0|\leq a<\mathop{\mathrm{cf}}(\beta)\), \(T_0\) is bounded in \(\beta\). Each \(S_i\) is bounded too, and its uppermost slot is infinite. The next stage therefore contains points above all of \(S_i\). Every at-most-\(\theta\) subset of \(T_0\) is bounded in this way, proving \(\mathop{\mathrm{cf}}(T_0)>\theta\). ◻

Proof. Choose \(\alpha<\beta\) above \(T_0\). Indecomposability of \(\beta\) gives \(\alpha+\delta<\beta\), so \(J=[\alpha,\alpha+\delta)\) is available. Indecomposability of \(\delta\) gives \(\mathop{\mathrm{otp}}(T_0)+\delta=\delta\).

Fix a parameter subset \(P\subseteq T\) of size at most \(\theta\) and a finite tuple in \(\beta\). Match the coordinates below \(\alpha\) into \(T_0\) over \(P\cap T_0\) using Lemma 16. Keep coordinates in \(J\) fixed. The parameters in \(J\), together with these finitely many retained coordinates, are bounded in \(J\) because \(\mathop{\mathrm{cf}}(\delta)>\theta\). Match all coordinates at or beyond the end of \(J\) by suitably many distinct points of \(J\) above that bound, retaining any repetitions. The three portions stay in their correct mutual order, and this gives the required finite tuple over \(P\).

Here \(\Gamma_T=\mathbb Z^{(T)}\) is identified with its image in \(\Gamma_\beta\), and \(H(T)=\mathbb Q^{(\Gamma_T)}\) with its image in \(H(\beta)\). A sequence of at most \(\theta\) points of \(H(T)\) uses at most \(\theta\) ordinal positions in its finite codes. A witness in \(H(\beta)\) to an occupied strict slot uses only finitely many additional ordinal positions. Match those into \(T\) over all the parameter positions and retain the integer and rational coefficients. Lemma 11 makes every comparison with the sequence unchanged. The resulting point of \(H(T)\) witnesses that slot. The reverse implication follows from inclusion. ◻

Proof. Identify \(N\) with the presentation in the first item. Represent the requested set by labeled elements and collect the ordinal positions in the finite codes of their indices. There are at most \(a\) positions. Apply Lemma 16 to obtain \(T_0\). Its order type is below \(a^+\). Choose a profile occurrence \(\delta\) from the second item above \(\mathop{\mathrm{otp}}(T_0)\). Since \(a^+\leq\mathop{\mathrm{cf}}(\beta)\leq\beta\) and \(\delta<a^+\), Lemma 17 applies and gives \(T\) of order type \(\delta\).

The subpresentation \(A=E(H(T))\) is strong in \(N\) and has cardinality \(a\). It contains the requested set. For any \(\theta\)-tuple in \(A\), use a labeled presentation there. Its record is identical in \(E(H(T))\) and \(E(H(\beta))\) by the last assertion of Lemma 17. The order isomorphism \(\delta\cong T\) identifies its record in the former with the same record for \(E(H(\delta))\). The two record-to-name functions belong to the common profile and hence agree. This proves alignment simultaneously for all \(\theta\)-tuples of \(A\). ◻

Proof. Given \(\eta<\kappa^+\), choose a limit ordinal \(\rho>\eta\) with \(\kappa\leq\rho<\kappa^+\) and \(\mathop{\mathrm{cf}}(\rho)=\tau\), for example by appending an ordinal segment of type \(\tau\) beyond \(\eta+\kappa\). Set \(\delta=\omega^\rho\). It is additively indecomposable. A cofinal sequence of exponents gives a cofinal sequence in \(\omega^\rho\) by continuity of exponentiation. Fewer than \(\mathop{\mathrm{cf}}(\rho)\) ordinals below \(\omega^\rho\) have all their Cantor-normal-form exponents bounded below \(\rho\), and are therefore bounded in \(\omega^\rho\). This proves \(\mathop{\mathrm{cf}}(\delta)=\mathop{\mathrm{cf}}(\rho)=\tau\). Every ordinal below \(\omega^\rho\) has a finite Cantor normal form with exponents below \(\rho\). Thus \(|\delta|\leq\max(\aleph_0,|\rho|)=\kappa\). Since \(\delta\geq\rho\geq\kappa\) and \(\rho>\eta\), we have \(|\delta|=\kappa\), \(\delta<\kappa^+\), and \(\delta>\eta\). ◻

Proof. It suffices to treat length exactly \(\theta\); pad a nonempty shorter tuple by repetitions, and use any strong self-map for the empty tuple. In a categoricity model, the asserted reversal is equivalent to symmetry of the arrow relation on its \(\theta\)-tuple orbits. Indeed a reverse orbit arrow can be precomposed and postcomposed with automorphisms to match the particular image tuple and original tuple. The converse follows by applying reversal to a map witnessing an arrow.

Suppose that symmetry fails at unboundedly many categoricity cardinals. Let \(P\) be an infinite cardinal bounding the profile palette; for example take \(P=2^B\). Choose a strictly increasing list of failing categoricity cardinals \((\kappa_i)_{i<P^+}\). At each step choose it large enough that there is an infinite regular \(\tau_i\leq\kappa_i\) exceeding \(\ell\), \(\theta\), and every preceding \(\kappa_j\), and that \[\kappa_i>P,\qquad \kappa_i>\kappa_j^\theta\quad(j<i).\] Such choices are possible by unbounded failure: first bound the set of preceding cardinals and their powers, then choose a regular successor cardinal above the first bounds and a failing cardinal beyond all of them. This is a set-sized recursion.

At size \(\kappa_i\), fix its orbit naming. By Lemma 19, the ordinals of size \(\kappa_i\) and cofinality \(\tau_i\) used there are cofinal in \(\kappa_i^+\). One profile occurs cofinally often among them: otherwise the supremum of at most \(P<\kappa_i^+\) bounded fibers would be below the regular cardinal \(\kappa_i^+\). Since there are \(P^+\) sizes and at most \(P\) profiles, choose two sizes \(a<\mu\) with the same cofinally recurring profile. They satisfy \[\theta^+\leq a,\qquad a^\theta\leq\mu, \qquad \tau_\mu>a.\] Their common named arrow relation has \(p\longrightarrow r\) but no \(r\longrightarrow p\). Both names occur in both sizes. Proposition 18 applies inside every \(\mu\)-sized model, using any of its cofinal profile occurrences.

We construct \(\theta^+\) rounds of an increasing strong chain of \(\mu\)-sized models. At the start of round \(i<\theta^+\), choose an aligned \(a\)-sized submodel \(A_i\) containing all previous \(A_j\). This is possible because their union has cardinality at most \(a\). They are all strong in the current large model, and coherence will make \(A_j\leq_KA_i\) for \(j<i\).

Enumerate all \(\theta\)-tuples of \(A_i\), using \(a^\theta\) steps. At the step for a tuple \(\bar u\), if its current large-model orbit cannot reach \(p\), leave it as it is. If it can reach \(p\), compose such an arrow with \(p\longrightarrow r\) and realize the composite by a strong self-map of the current model. Regard this map as an inclusion into an isomorphic extension: rename its codomain so that the image of each old element becomes that old element. With the transported identification of the codomain, the tuple now has name \(r\). At every later large stage its orbit remains unable to reach \(p\). Otherwise transitivity from \(r\) would give \(r\longrightarrow p\). An orbit already unable to reach \(p\) has the same persistence property.

Take strong unions at every limit step, including between rounds. The entire construction has at most \(\theta^+\cdot a^\theta\leq\mu\) many stages in cardinality. Every large union therefore has size \(\mu\) and is a copy of \(C_\mu\) by categoricity. Every transition between such copies gives an arrow of the common relation, so the persistence assertion also holds at limit stages.

The aligned submodels form a strong increasing chain: for \(j<i\), their underlying sets are included and both are strong in the large model at the start of round \(i\), so coherence applies. Its union \[A=\bigcup_{i<\theta^+}A_i\] belongs to \(K\), has cardinality \(a\), and is a copy of \(C_a\). Any \(\theta\)-tuple of \(A\) is contained in some \(A_i\), since \(\mathop{\mathrm{cf}}(\theta^+)>\theta\). After round \(i\) it cannot reach \(p\) in a large model. At the next aligned small model its small orbit has the same name, and therefore cannot reach \(p\) in the common relation. The inclusion of that small model into \(A\) gives an arrow from this earlier small orbit to its orbit in \(A\). If the latter could reach \(p\), transitivity would contradict the former exclusion. Thus no tuple in \(A\) can have an orbit reaching \(p\).

But \(A\cong C_a\), so the orbit named \(p\) occurs in \(A\); it reaches itself by the identity map. This contradiction proves that the failing categoricity cardinals are bounded. A cardinal above their bound is \(b_K(\theta)\), and the first paragraph gives the claimed reversals, including all shorter lengths. ◻

Proof. The downward LS axiom supplies the submodel, after adding \(\kappa\) many elements to the requested set if necessary. If \(M_0,M_1\le_KN\) are two such submodels, apply LS to \(|M_0|\cup|M_1|\). It gives \(M_2\le_KN\) of size \(\kappa\) containing both. Coherence gives \(M_i\le_KM_2\). The two occurrences of \(a\) therefore have the same class. For a strong embedding \(f:N\to N'\), the image of a witnessing submodel is a strong \(\kappa\)-submodel of \(N'\), so the same observation proves preservation. All these comparisons take place inside a given ambient model; no amalgamation property is used. ◻

Proof. If \(\gamma\ge\kappa\) are categoricity cardinals above the reversal threshold, Lemma 21 associates a \(\kappa\)-class to every \(\gamma\)-class. This gives a projection \(\pi_{\gamma\kappa}\), and these projections compose. They are surjective. Indeed, a \(\kappa\)-model is isomorphic to \(E(I)\) for \(|I|=\kappa\); extend \(I\) to an order of size \(\gamma\) and use the strong order map. Every tuple class in the smaller model then occurs in the larger one. This argument supplies the needed extension without a no-maximal-model assumption.

These projections are eventually all bijective. Otherwise, construct a sequence of categoricity cardinals with more than \(B_\sigma\) successive noninjective projections, and choose one final categoricity cardinal \(\rho\) above the entire sequence. For each noninjective projection, surjectivity supplies a pair of \(\rho\)-classes which agree when projected to the earlier stage and differ when projected to the later stage. Pairs selected at distinct stages are distinct: after a pair has separated it remains separated under every later refinement. This gives more than \(B_\sigma\) pairs from a set of size at most \(B_\sigma\), a contradiction. The construction uses only a set-length sequence of cardinals and choices from sets.

Choose a categoricity cardinal \(c_\sigma\) beyond this stabilization and reversal threshold. The canonical \(c_\sigma\)-class defines the desired diagram on models of size at least \(c_\sigma\). The bijective projections show that its equality can equally be computed at every later categoricity cardinal. If two tuple bounds are used, compare them at a categoricity cardinal above both thresholds. Restriction of strong maps then gives the same restricted equivalence. Atomic formulas and their negations are preserved because strong maps are structure embeddings.

For definiteness, thresholds can be chosen as least cardinals having the stated eventual properties. Choose \(t(\sigma)\) to be the least categoricity cardinal strictly above \(\ell+\sigma\) and above all the thresholds \(c_\tau\) for infinite \(\tau\le\sigma\). This is a nondecreasing definable function. The preceding arguments prove the first three assertions.

For the fourth, first put a realization of \((a,c)\) into a strong \(c_\sigma\)-submodel. If the originally chosen ambient size is smaller than a desired target categoricity size, this categorical submodel can be extended to that size by the order presentation. If the original ambient size is larger, LS gives a submodel of the desired size containing the realization. Thus the joint diagram has a realization in a model of the target categoricity size. Apply the third assertion to the first tuple and the specified tuple in the target. The resulting strong map transports the whole realization as required. ◻

Proof. Existence follows from \(E(I)\) for \(|I|=\zeta\). Let \(M,N\) have size \(\zeta\), and choose countable increasing exhaustions of their underlying sets by sets of size less than \(\zeta\). Start with the prescribed bounded diagram match, or with the empty match. At a forward step, enumerate together the current source tuple and the next part of the exhaustion of \(M\). Its length and the length of the current target tuple are bounded by an infinite \(\sigma<\zeta\). Put the data on each side inside a strong submodel of size \(t(\sigma)<\zeta\). Their current tuples have the same diagram. Proposition 22 gives a strong map of these submodels matching those tuples. Its values on the new entries extend the match, and the enlarged tuples again have equal diagrams. At the next step interchange \(M,N\).

Only finitely many previously chosen bounded tuples are used at each step, so their combined length stays below \(\zeta\). The union of the countable sequence of partial matches is a bijection \(|M|\to|N|\). Every finite tuple and every value of a finitary function occur at some step, where the atomic diagram is preserved. The bijection is therefore a structure isomorphism. ◻

Proof. Present the categoricity model as \(E(H(\delta))\), choosing \(|\delta|\) to be its cardinality and \(\mathop{\mathrm{cf}}(\delta)>\chi\). This is possible at every sufficiently large cardinal, including singular cardinals. Fix term representations of the parameters, and let \(S\subseteq H(\delta)\) be their support set. Its size is at most \(\chi\). Every member of \(S\) is coded by a finite list of ordinals and integer and rational coefficients. The union of its ordinal supports consequently also has size at most \(\chi\).

For one further position, its finite ordinal support has at most \(\chi\) possible order/equality patterns over these old ordinal supports. The discrete coefficients contribute only countably many choices for each finite code. Such a pattern determines all comparisons of the new position with \(S\). For at most \(\sigma\) new positions, include their mutual comparisons, their identifications with old positions, and the term labels. There are at most \(\chi^\sigma=\chi\) choices so far.

To apply Theorem 14, also record which strict slots over the old and new positions are realized in \(H(\delta)\). The old support \(S\) is fixed. A slot over \(S\) not containing a new position is unchanged. At most \(\sigma\) old slots contain new positions, and inside each there are at most \(2^\sigma\) cuts of the new support to test. The new flags therefore have at most \(2^{2^\sigma}\le\chi\) possible values. The full record has at most \(\chi\) possibilities.

The combined list of old and new positions has size at most \(\chi<\mathop{\mathrm{cf}}(\delta)\). Theorem 14 extends equality of full records to an order automorphism fixing \(S\) pointwise. Its induced automorphism of the presentation fixes the parameters and matches the tuples. Thus the number of structure-automorphism orbits is at most the number of records. ◻

Proof. Suppose the original and modified diagrams were different. Let \(\sigma\) bound the two lists, their supports, and the shared positions. Choose \(\chi\ge\ell+2^{2^\sigma}\) with \(\chi^\sigma=\chi\), for instance by taking a sufficiently large power of two.

In each region repeat the pair of blocks along an arbitrary linear order \(L\). If the first family’s block was on the left, use the order \(L\) for the repetitions; if it was on the right, use the reverse of \(L\). Write \(d_i\) for the first-family tuple using the blocks at index \(i\), and \(e_j\) for the second-family tuple using the blocks at index \(j\); retain all the shared positions outside the regions. For \(i<j\), the diagram of \((d_i,e_j)\) is the original one, and for \(i>j\) it is the modified one. Comparisons within either family and across distinct regions do not change.

Let \(\epsilon\) be the least infinite cardinal satisfying \(2^\epsilon>\chi\). The binary tree \(2^{<\epsilon}\) has at most \(\chi\) nodes: for \(\alpha<\epsilon\) each level has size at most \(\chi\), and \(\epsilon\le\chi\). Give it lexicographically ordered divider points, one between the two successor subtrees at each node. Explicitly, encode branch digits by \(-1,1\), and encode the divider at a node \(s\) by the sequence \(s\) followed by \(0\), using \(-1<0<1\) in lexicographic comparison. Adjoin one point for every branch in \(2^\epsilon\). Distinct branch points determine distinct strict cuts over the divider points. Use this as the order \(L\).

The tuples \(e_j\) at the divider indices, together with the fixed shared data, use at most \(\chi\) parameters. If two branch-indexed tuples \(d_i\) were in the same automorphism orbit over these parameters, their diagrams with every divider tuple would agree. A divider between the two branches gives the two different diagrams, a contradiction. Hence there are more than \(\chi\) such orbits. Pad the constructed order to a sufficiently large categoricity size and apply Lemma 25. This is impossible. ◻

Proof. The assertion is immediate if \(C\) is empty or \(U\) is empty. Well-order \(C\), and suppose no such set exists. For every ordinal \(\beta\), the set \(U\cap V_\beta\) fails to generate \(U\) upwards. There is therefore an element of \(U\) which dominates none of its members. Let \(h(\beta)>\beta\) be the least ordinal such that one such witness lies in \(V_{h(\beta)}\). This is a definable ordinal function.

Take an ordinal length \(\lambda\) satisfying the partition relation for pairs, \(|C|\) colors, and an infinite homogeneous set, supplied by Lemma 8. Define increasing ordinals \(\beta_i\), for \(i\le\lambda\), recursively, with \(\beta_{i+1}>h(\beta_i)\) and with limit values above all earlier values. Choice for a set-indexed collection of nonempty subsets of \(V_{\beta_\lambda}\) now selects witnesses \(u_i\) which dominate no member of \(U\cap V_{\beta_i}\), for \(i<\lambda\). For \(i<j\), we have \(u_i\in V_{\beta_j}\), so some coordinate satisfies \(u_i(c)>u_j(c)\). Color the pair \(i<j\) by the first such coordinate in the fixed well-order of \(C\). An infinite homogeneous set yields an infinite strictly decreasing sequence of ordinals in that coordinate. This contradiction proves the claim. The rank bounding above ensures that only ordinary set-sized Choice, not a choice principle for proper classes, was used. ◻

Proof. Amalgamate the two support orders over \(I\), and let \(T\) be the union of the supports of the two added tuples. Its size is at most \(\sigma\). Freeze its order, the labels and supports of the two tuples, and the subset of its positions which belong to \(I\). Up to a relabeling on a fixed set of size at most \(\sigma\), these frozen data range over a set.

For fixed frozen data, each component of \(I\setminus T\) in a strict slot over \(T\) is well-ordered. Record its ordinal length. The set of slots is fixed, so these lengths form an ordinal vector. Restrict attention to the vectors that give valid configurations and for which the two placed comparisons are unequal. This is a definable class: order presentations and diagrams are defined from set codes, and diagrams of any specified set length can be evaluated above their thresholds.

Coordinatewise domination gives an order embedding of the smaller configuration into the larger one, fixing \(T\) and preserving the base positions. Natural diagrams respect these embeddings. Thus a valid smaller unequal configuration remains a witness in any dominating valid configuration. Apply Lemma 27 to this class, obtaining a set of valid witnesses. Equivalently one could apply it to the upward closure and select its generators from valid configurations; no assertion that arbitrary vectors themselves describe well-orders is required.

Bound the sizes of the base orders in this set of witnesses. An embedded witness uses only that bounded number of old positions. All labels on these positions give at most their cardinality plus \(\ell\) elements of \(A\), and the diagrams of the two added tuples with these elements are unequal. Taking a cardinal bound over the set of frozen data gives \(g(\sigma)\). Increasing it to an infinite nondecreasing function causes no change in the assertion. When a witness uses only finitely many positions, “all labels” simply means their evaluated terms; no assertion about membership of a finite-order presentation in \(K\) is needed. ◻

Proof. Fix one term representation per parameter in \(A\). Write \(S_X\subseteq I\) for the supports of \(X\). For one set \(X\), its prescription has a placement. To see this, extend \(I\) to a sufficiently large categoricity size and use Proposition 22 to realize the possible joint diagram over the actual parameter tuple. The realization has term representations in that presentation.

A support profile over \(X\) records the labels for \(d\), its formal support order \(T_0\) of size at most \(\sigma\), and comparisons and coincidences with \(S_X\). A well-order of size at most \(\chi\) has at most \(\chi\) cuts. Hence there are at most \(\chi^\sigma=\chi\) profiles. The positions of \(T_0\) in one strict slot over \(S_X\) form a cluster. Each profile has a continuation over \(I\) which leaves every such cluster intact: insert the cluster at a single cut of \(I\) extending its specified cut over \(S_X\).

Call a hit of a new parameter support on \(T_0\), or the separation of two positions in one cluster by a new parameter support, a new event. For \(X'\supseteq X\), all continuations of a profile with no new event over \(S_{X'}\) have the same natural diagram over \(X'\). Within each old slot, the whole cluster can only change its position across a block of new parameter positions. The slots are disjoint, so Lemma 26 applies simultaneously.

Suppose no placement solves all the prescriptions. Start with any \(X_0\) of size at most \(\chi\). Given \(X_i\), choose for every profile over \(X_i\) a continuation with no new event over all of \(I\). It fails a prescription on some set of at most \(\chi\) parameters. Adjoin one such failing set for each profile to obtain \(X_{i+1}\). At limits take unions, and carry out \(\sigma^+\) stages. Every set constructed, including \(X_* = \bigcup_{i<\sigma^+}X_i\), has size at most \(\chi\), because \(\sigma^+\le\chi\).

Take a placement realizing \(q_{X_*}\). At each stage its profile over \(X_i\) was considered. If it had no new event between \(S_{X_i}\) and \(S_{X_{i+1}}\), the preceding no-event comparison would identify its diagram on the selected failing set with that of the chosen continuation. This contradicts its realization of \(q_{X_*}\). Thus it has a new event at every stage. A support position can be newly hit only once, and a pair can be newly separated only once. There are at most \(\sigma+\sigma^2=\sigma\) such events. They cannot occur at \(\sigma^+\) different stages. ◻

Proof. The displayed bounded diagrams are defined, since their thresholds lie below \(\mu\), and they agree on the parameters with the natural diagrams. For every sufficiently large \(\chi<\mu\) with \(\chi^\sigma=\chi\), Proposition 29 gives a placement realizing the tests of size at most \(\chi\). Such \(\chi\) are cofinal below \(\mu\): use \(\chi=2^\alpha\) for \(\sigma\le\alpha<\mu\), enlarging \(\alpha\) as necessary.

Once \(\chi\ge g(\sigma)\), any two resulting placements have the same full comparison by Proposition 28. Fix one of them. Every bounded test is covered by a larger choice of \(\chi\), whose placement has that same full comparison. The fixed placement consequently realizes every bounded test. The same argument gives uniqueness. A restriction realizes the restricted tests and hence, by uniqueness, is their lift. ◻

Proof. Such levels are unbounded by the countable closure construction following Proposition 23. Categoricity at them has already been proved. Identify a given base with \(A=E(I)\), where \(I\) is a well-order of size \(\mu\). Extend \(I\) to an order \(J\) whose cardinality \(\gamma\) is a categoricity cardinal at least \(t(\mu)\), and let \(G=E(J)\). Thus \(A\) is strongly included in its specified position in \(G\).

We show that every \(\mu\)-sized strong extension \(B\) of \(A\) embeds strongly into \(G\) over \(A\). Choose \(M_n\le_KB\), increasing with union \(B\), with \(\|M_n\|<\mu\). This follows by LS from a countable exhaustion of \(B\), containing the preceding submodel at each step; coherence makes the chain strong. Choose compatible enumerations \(d_n\) of these models, so that each earlier list is a sublist of the next.

Lemma 30 assigns coherent placed comparisons to \((d_n,A)\). Each is realized over \(A\) in \(G\), and the realizations can retain the previous assignments. More explicitly, realize the corresponding term pattern in an order extension of size \(\gamma\). Its parameter tuple \(A\), and then its tuple \((A,d_{n-1})\), have the same diagram as the already assigned ones. Their length is at most \(\mu\), so Proposition 22 at \(\gamma\ge t(\mu)\) supplies the strong map realizing the new list while fixing these previous data.

It remains to verify strongness of the copied small models; atomic agreement by itself would not suffice. Fix \(n\), and bound the length of \(d_n\) by an infinite \(\sigma_n<\mu\). Choose the categoricity cardinal \(\rho=t(\sigma_n)<\mu\). LS puts the original enumeration inside \(B_n'\le_KB\) of size \(\rho\), and the copied enumeration inside \(G_n'\le_KG\) of that size. Coherence gives \(M_n\le_KB_n'\). The copied and original lists have the same bounded diagram; Proposition 22 gives a strong map \(B_n'\to G_n'\) with exactly the prescribed values on \(d_n\). Its restriction shows that the copied \(M_n\) is a strong submodel of \(G\).

The copied models are nested, and coherence makes their inclusions strong. Their union is a strong submodel of \(G\) by the chain and common-upper-bound axioms. It is the image of an embedding of \(B\). Every element of \(A\) eventually occurs in some \(d_n\), and its equality with that parameter is part of the lifted comparison. The embedding therefore fixes \(A\). Performing this construction for \(B_0,B_1\) in the same \(G\) gives an amalgam. LS supplies a strong \(\mu\)-submodel of \(G\) containing both images; coherence makes it a strong amalgam of the required size.

For the second assertion, any identifying amalgam preserves the displayed bounded diagrams, giving necessity. Conversely, Proposition 28 identifies the placed lifts of \(d_0,d_1\) over \(A\). Realize this common lift once in \(G\). On each side start the preceding countable construction with the specified tuple already assigned, and choose every small-model enumeration to contain that tuple. Homogeneity over \(A\) and the old assignments works exactly as above. The two resulting embeddings identify the tuples, and the same LS shrinking applies.

For a singleton, a placement uses one label on a finite support. Relative to the well-order \(I\), each support position is either an old position or lies in one of its \(|I|+1\) cuts. Together with the finitely many mutual comparisons and the label, these data have at most \(\mu\) possibilities. They determine the full natural comparison. The second assertion identifies exactly the types with equal comparison, proving the bound. ◻

Proof. We first prove the directed assertion by induction on the cardinality of an indexing set. A finite directed family has a member containing all its members. A countable directed family has a cofinal increasing sequence, obtained by successively choosing an upper bound for the previous choice and the next enumerated member. The chain assertion gives its union and its common-upper-bound property.

For an uncountable indexing cardinal \(\tau\), fix a binary operation on the indexing set selecting an upper bound for each pair. Write the indexing set as an increasing union of sets of size less than \(\tau\), and close each under this operation. This closure adds only countably many stages and preserves the bound of being smaller than \(\tau\). The sets can be chosen nested, and their union is the whole indexing set. By the inductive assertion each corresponding smaller directed family has an object as its union. That union still has cardinality \(\mu\): it contains a member of cardinality \(\mu\) and is contained in the given total union of cardinality \(\mu\). The common-upper-bound part of the inductive assertion makes these unions a chain of arrows. The chain assertion now gives the total union. Applying the same common-upper-bound clauses to a specified ambient object proves the last assertion, including the mixed-level version.

Fix a well-ordered subset \(J_0\subseteq I\) of size \(\mu\). Let \(\mathcal J\) consist of all well-ordered subsets of \(I\) of size \(\mu\). A union of two well-ordered subsets is well-ordered: in any nonempty subset take the smaller of the minima supplied by its two nonempty intersections. Thus \(\mathcal J\) is directed under inclusion. Every finite subset of \(I\) is contained in a member, namely its union with \(J_0\). The finite-support description of the template identifies \[F(I)=\bigcup_{J\in\mathcal J}F(J).\] The union has cardinality \(\mu\), and the directed assertion applies. For an order embedding \(I\to I'\), first restrict to well-ordered suborders of the source. Their images are well-ordered; if necessary, enlarge each image by a padding subset in the target. The known order arrows and the common-upper-bound assertion give the induced map on the total union as an arrow.

Finally, two occurrences of the same bounded support pattern in orders can be identified by amalgamating the orders over that suborder. Such an amalgamation is obtained cut by cut: retain the common suborder and put the points from each of the two orders in their prescribed cuts, keeping their own orders within each cut. Append a well-order of sufficiently large eligible cardinality to make the amalgam padded. The two order arrows identify the term lists there. Diagram preservation proves their naturalness. ◻

Proof. Put \(\xi=2^\eta\), so that \(\xi^\eta=\xi\) and \(\eta^+\leq\xi\). Starting with an order of size \(\xi\), repeatedly fill every cut specified by disjoint sets \(A<B\) with \(|A|+|B|\leq\eta\), allowing an empty side. At each stage there are at most \(\xi^\eta=\xi\) requests; they can be filled in an order extension of size \(\xi\). Perform \(\eta^+\) stages and take unions at limits. A set of at most \(\eta\) parameters in the final union occurs in one earlier stage, since \(\eta^+\) is regular. Its requested cut is filled at the next stage. The order is dense and without endpoints because requests with at most two parameters were among those filled. To realize an arbitrary added pattern, well-order its at most \(\eta\) new positions and insert them successively. Each insertion asks for a cut over at most \(\eta\) old or previously inserted positions.

For the second assertion, use the lexicographic sum \[I_{\mu,\eta} =\sum_{\alpha<\mu\cdot\eta^+}Q_\eta,\] where the index is ordinal multiplication. Its cardinality is \(\mu\), its index has cofinality \(\eta^+\), and choosing one point in each summand gives a well-ordered subset of cardinality \(\mu\). Here \(|Q_\eta|=2^\eta<\mu\).

Consider a cut \(A<B\) with at most \(\eta\) parameters. If \(B\) is empty, the indices of the summands meeting \(A\) are bounded in \(\mu\cdot\eta^+\), and a later summand supplies a point above \(A\). If \(B\) is nonempty, let \(\beta\) be the least index of a summand meeting \(B\). All points of \(A\) lie in summands of index at most \(\beta\). In the summand at \(\beta\), fill the cut between \(A\cap Q_\eta^{(\beta)}\) and \(B\cap Q_\eta^{(\beta)}\); the first set is allowed to be empty. The resulting point fills the original cut. The same successive-insertion argument realizes added patterns. ◻

Proof. The structural conditions are the AEC axioms, including their common-upper-bound clauses. The presentation and its mixed order arrows are supplied by Theorem 9. Categoricity at the specified levels identifies every model with each presentation of the same size; supports in such a presentation give mixed downward closure as described after Definition 33.

Proposition 22 gives the bounded diagrams, their uniform cardinal bounds, restriction compatibility, and preservation under strong maps. Proposition 23 gives isomorphism at equal bounded diagrams. For saturation, let \(a\) be an actual tuple and let \((b,c)\) witness a possible joint diagram, with \(D(a)=D(b)\). Choose an infinite \(\sigma<\mu\) bounding both lists. The closure requirements provide a categoricity cardinal \(\kappa<\mu\) above \(\sigma\) and the stabilization thresholds for these arities. Put \(a\) in a strong \(\kappa\)-submodel of its actual model. Put \((b,c)\) in a strong \(\kappa\)-submodel of its witness, first embedding the witness into a larger eligible presentation if needed. Stabilization identifies the \(\kappa\)-comparison classes of \(a\) and \(b\), so a strong map from the second submodel to the first takes \(b\) to \(a\). Its image of \(c\) realizes the required joint diagram. Naturality follows from the order arrows and order amalgamation. Images of small strong submodels are strong by the isomorphism argument following Definition 33; taking their increasing unions proves the exhaustion criterion. Finally, imposing the additional closure bounds of Theorem 31 retains each of these already established assertions. Those additional bounds provide the amalgamation and comparison facts needed later; they are not extra axioms of a working scheme. ◻

Proof. Let \(\beta\) be an infinite bound for the length of \(c\), and choose one eligible \(\alpha>|F|+\beta\). The diagram of \(c\) has a witness at \(\alpha\). If its original witness is at a larger level, use saturation at \(\alpha\) with the empty tuple as base. If its witness is at a smaller level, first extend that object to a presentation at a level at least \(\alpha\) using an order arrow. This gives a choice of \(\alpha\) uniform over all diagrams of the specified arity. Choose a well-ordered chart for this new witness and fix representations of \(c\). Let \(J\) be the union of their finite supports, with its inherited well-order. In the presentations \(F(J+H)\) name the terms representing \(c\) on \(J\). Regard this as a template in the variable order \(H\): any term using positions from both parts becomes a label recording its original label and its finitely many fixed positions from \(J\), applied to its remaining positions from \(H\). Terms supported wholly on \(J\) are labels of arity zero. The new collection of labels has cardinality at most \(|F|+|J|+\aleph_0\) and is fixed independently of the level. Order maps on \(H\), extended by the identity on \(J\), induce arrows preserving the names.

Naturality gives the prescribed diagram on the named list in every sufficiently large such presentation. Homogeneity for \(c\) shows that every object with such a named realization is isomorphic to one of these presentations. Define its diagram on a further list \(a\) to be the old diagram on the combined list \((c,a)\). The old package gives exactly restriction compatibility, the uniform bound, preservation, homogeneity, and saturation for these diagrams. The same support construction gives mixed downward closure, now including the named terms. Chain unions and the exhaustion criterion retain the names, so they are inherited.

For the final assertion suppose a sublist enumerates \(M\leq_KV\) in the original witness, which may be at a level larger than \(\alpha\). Embed that original system and the new level-\(\alpha\) witness into objects of a common larger eligible level. Mixed preservation and homogeneity there give an isomorphism matching their named lists. The original copy of \(M\) has strong image in that large vertex. This image is exactly the substructure enumerated inside the embedded level-\(\alpha\) vertex, so coherence makes it strong in that vertex as well. It is a \(K\)-model because its complete atomic enumeration is isomorphic to \(M\). Thus strong naming already holds in the uniformly small witness. Above \(\alpha\), order arrows and the same homogeneity argument preserve it. The argument applies to every named vertex model and specified map. Thus the new presentations satisfy the intended strong naming condition, not just the atomic diagram of the enumeration. ◻

Proof. For the first route, fix an arity bound \(\sigma\). At a sufficiently large eligible cardinal \(\kappa\), arrow comparison on lists of this arity is reflexive and transitive, and reversal makes it symmetric. A list in a larger object can be put into a level-\(\kappa\) subobject. Two choices of that subobject are included in a third by mixed downward closure and coherence. Their arrow classes therefore agree. This defines the level-\(\kappa\) comparison in all larger objects and shows that it is preserved under mixed arrows.

If \(\gamma\geq\kappa\) is another sufficiently large eligible cardinal, there is consequently a projection from the \(\gamma\) comparison classes to the \(\kappa\) comparison classes. This projection is onto: an object at level \(\kappa\) embeds into one at level \(\gamma\) by identifying it with a chart and using an order arrow. The projections compose. Let \(b\) bound the numbers of classes. If strict refinement continued arbitrarily high, recursively choose \(b^+\) many successive strict refinements and then an eligible cardinal above all the chosen levels. At each strict refinement some pair of classes at this final level has equal images before the refinement and unequal images after it. A fixed pair can witness this only once, since unequal images cannot merge in a refinement. There are at most \(b^2=b\) pairs, a contradiction. Thus the comparisons stabilize.

Their stabilized equality is canonical, and comparisons at different arities commute with restriction: raise the cardinal beyond the stabilization thresholds for both arities and restrict an arrow implementing the longer comparison. Atomic diagrams are preserved by arrows. A prescribed bounded extension is realized over an actual list in a sufficiently high same-level object by placing a witness and the actual list into objects of one common eligible size and using the reversible comparison to map the witness list to the actual one. This gives the joint extension as well.

At a receiving level \(\mu\) of countable cofinality, close below \(\mu\) under these thresholds and under choices of a sufficiently large smaller eligible cardinal for each arity. Enumerate each of two objects by countably many nested bounded lists. To extend a match, choose a smaller eligible cardinal containing all the old and newly requested entries and above their stabilization thresholds. Put the data into subobjects at that cardinal and implement the equal stabilized diagrams by an arrow in the desired direction. Alternate the direction of extension and include the next enumeration list on each side. The union is a bijection preserving and reflecting every atomic formula, hence an isomorphism of systems. Starting with a given equal-diagram tuple makes it part of that isomorphism. The same smaller-level construction realizes a possible bounded extension diagram over an actual tuple. Order arrows and order amalgamation give naturality. These arguments use both eligibility of \(\mu\) and the availability of smaller eligible cardinals, as distinguished in Section 5.2.

For the second route, instances of the same well-ordered pattern have the same orbit. Indeed two well-orders amalgamate over a common suborder into a well-order: in each cut of the common well-order concatenate the two remaining well-ordered pieces, then retain the common points between successive cuts. Enlarge to an eligible size if necessary. The induced order arrows and same-level orbit preservation identify the two instances. The assumed independence of orbit comparison from the level therefore defines diagrams on well-ordered patterns. The set of such patterns at a fixed arity gives a uniform bound.

For a mixed arrow from level \(\nu\) to level \(\mu\), include the image of its whole source in a level-\(\nu\) subpresentation of the target. Coherence factors the arrow through that subpresentation. Same-level orbit preservation computes the comparison there, and the assumed agreement of chart comparisons computes the same diagram in the target. This proves mixed preservation. For saturation, take a well-ordered support pattern witnessing the desired joint diagram in a larger object. Its support has cardinality below the receiving level, so it embeds into a well-order of that level. The old subtuple has the diagram of the prescribed actual tuple; an isomorphism at the receiving level carries the new realization over that tuple. The orbit hypothesis itself supplies homogeneity. Naturality on padded orders follows from Lemma 35.

In either route, diagrams on bounded enumerations of small vertex submodels have strong images by homogeneity, with the preliminary order embedding in the mixed-level case. The AEC union axioms give the asserted componentwise exhaustion condition. ◻

Proof. Fix an infinite \(\eta\) at least the cardinality of the template code and of the patterns to be tested. For two set structures \(A,B\) in its language, form the set of all pairs of tuples of the same index set of cardinality at most \(\eta\). Index sets can be taken to be ordinals below \(\eta^+\), reindexing concatenations when necessary. Let \(R_0\) consist of the pairs with the same atomic diagram. Having defined \(R_\alpha\), retain in \(R_{\alpha+1}\) just those pairs \((a,b)\in R_\alpha\) such that every added tuple of cardinality at most \(\eta\) on either side has a matching added tuple on the other side with the extended pair in \(R_\alpha\). At a limit take the intersection of all preceding relations.

This decreasing recursion stabilizes. If its state set has cardinality \(\tau\), there cannot be a strict decrease at every successor stage below \(\tau^+\), since each strict decrease removes a previously unremoved state. Equality at one successor stage gives a fixed point. Write \(R_\infty\) for the stabilized relation. In particular, from a pair in \(R_\infty\) every allowed extension has a matching extension still in \(R_\infty\); quantification over all ranks is not being exchanged with an existential choice without this fixed-point argument. Reflexivity and symmetry follow from the construction. Transitivity follows by composing matches: the composition of two relations having the atomic and extension properties again has those properties, and is contained in the largest such relation \(R_\infty\). This also proves invariance under isomorphisms.

Use orders satisfying Lemma 36, and realize the two indicated patterns in their term structures. Declare \(p\equiv_{F,\eta}q\) when their tuple pair belongs to \(R_\infty\). Every support pattern of size at most \(\eta\) embeds into such an order, by the successive insertion assertion in that lemma.

The definition is independent of the rich orders and of the realizations of an individual pattern. To prove this, relate two term tuples when their representations are carried to each other by an order isomorphism between support sets of size at most \(\eta\). This relation has atomic matching by the definition of the template. An added tuple has at most \(\eta\) new support positions. Order richness extends the support map to these positions on the other side, in either direction. Thus this relation has the extension property and is contained in \(R_\infty\). Replacing an instance of either pattern by another instance and using transitivity proves independence for the comparison of two possibly different patterns.

If \(\eta'\geq\eta\), orders rich for \(\eta'\) are also rich for \(\eta\), and their back-and-forth test with the larger moves implies the test with the smaller moves. Independence of the chosen orders gives \[\equiv_{F,\eta'}\ \subseteq\ \equiv_{F,\eta}\] on patterns in the common domain. Define \(D_F\) to be agreement at every sufficiently large test bound \(\eta\).

Here is both uniform definability and the promised single bound. In defining the test at \(\eta\) it is enough to use rich orders of cardinality \(2^\eta\) on a fixed standard universe, whose existence was proved in Lemma 36. All their order relations, the realizations of the patterns, the associated term structures, and the states of the recursion are sets. The recursion up to the successor cardinal of its state set defines \(R_\infty\) by an ordinary first-order set-theoretic formula. Independence means that one may quantify over the rich orders and realizations in that set, without making a uniform class choice of an order.

For each pair in \(\mathcal P_F(\sigma)^2\) which fails some test, take its least failing infinite cardinal above the fixed input bounds. This is a uniquely defined ordinal when it exists. Replacement collects these witnesses into a set. Choose \(b_F(\sigma)\) above their supremum, above \(\sigma\), and above the template and naming bounds. Monotonicity proves \[p\mathrel{D_F}q \quad\Longleftrightarrow\quad p\equiv_{F,b_F(\sigma)}q, \qquad p,q\in\mathcal P_F(\sigma).\] The same holds at every larger test bound. Taking suprema over smaller arities makes \(b_F\) monotone if desired. Notice that the cardinality of the set of patterns justifies taking the set of separation witnesses; it does not assert an a priori numerical upper bound on their ranks. A code failing the coherence tests may, if a total definition on all set codes is desired, be assigned the discrete comparison and a fixed default bound. This convention has no mathematical role for a coherent template.

We now compare with the working diagrams. First suppose two bounded patterns have equal working diagrams. Fix any test bound \(\eta\). Choose an eligible level large enough for the patterns and \(\eta\), and use a rich padded order of that level from Lemma 36. Lemma 35 makes its term structure an object of the scheme. Naturalness transfers the equal working diagrams to realizations of the two patterns there. The package gives an isomorphism taking one realization to the other. It passes the back-and-forth test at \(\eta\). Independence of rich orders now gives \(p\equiv_{F,\eta}q\). Since \(\eta\) was arbitrary, equal working diagrams imply \(D_F\)-equivalence.

Conversely fix an eligible \(\mu\) as in the statement and two objects of that level with bounded lists whose patterns are \(D_F\)-equivalent. Choose countable nested bounded enumerations exhausting both objects. We construct compatible matches containing these enumerations, maintaining \(D_F\)-equivalence of their term patterns. Suppose the current lists have been matched, and a next bounded list on one side is requested. Let an infinite \(\rho<\mu\) bound the cardinality of the combined old and requested lists. Choose \[b_F(\rho)\leq\eta<\mu.\] This is possible by strict closure. At the same level \(\mu\), form rich padded presentations for this test. Realize the current patterns there. Naturality and homogeneity for the working diagrams give isomorphisms from the current objects to these presentations taking their current lists to the chosen realizations.

Transport the requested list through the first isomorphism. The current pair passes the test at \(\eta\), so the fixed-point extension property supplies a matching list in the other rich presentation. Choose finite-support term representations for the extended lists. Their patterns pass the \(\eta\)-test; because \(\eta\geq b_F(\rho)\), they are \(D_F\)-equivalent. Transport the matching list back to the actual target object. The isomorphisms used in this transport preserve working diagrams, which were already shown to imply \(D_F\)-equivalence. Transitivity therefore gives the required \(D_F\)-equivalence for the extended actual lists, independently of their chosen representations.

Repeat with the sides reversed and with the next lists in the two enumerations. All stages have cardinality below \(\mu\); only their countable union exhausts the objects. Atomic matching ensures that the compatible assignments define a well-defined injective map, and the alternating exhaustion makes it onto every sort. Every atomic instance involves finitely many entries and occurs at one stage, so the resulting bijection is a structural isomorphism. It carries the original list to the other list. The working package therefore identifies their working diagrams, as required. ◻

Proof. Present the parameter object on a well-order. After choosing one term representation of each parameter, its supporting positions form a well-ordered set of size at most \(\chi\). There are at most \(\chi\) slots and positions relative to this set. Labels, comparisons and coincidences for at most \(\sigma\) additional positions therefore have at most \(\chi^\sigma=\chi\) possibilities. Equal profiles give equal natural diagrams. The diagram-isomorphism clause of the working package turns this into the asserted orbit bound over the actual parameters.

Here are the hypotheses needed for the block argument in Lemma 26. We have just proved its parameter orbit bound. Repeating the two blocks along an arbitrary order is permitted after padding: the scheme has the union and common-upper-bound clauses, so Lemma 35 supplies the padded presentations and their order arrows. Naturalness compares the two patterns at a common higher eligible level. If the transposition changed a diagram, the repeated patterns would distinguish cuts by whether the first block preceded or followed a parameter block. A binary tree of least height \(\epsilon\) with \(2^\epsilon>\chi\) has at most \(\chi\) nonterminal nodes and more than \(\chi\) branches. Divider points at those nodes give at most \(\chi\) parameter blocks and more than \(\chi\) different diagrams over them. The preceding orbit bound gives a contradiction. The repetition uses only a set of positions, so a higher eligible level can contain the entire test. This proves the assertion also when there are boundedly many simultaneous transpositions. ◻

Proof. Amalgamate the orders containing the two placements over the parameter order. Freeze the labels of the two tuples, their combined ordered support \(T\), the coincidences with old positions, and the colors. There are set-many such frozen patterns at the prescribed bound. The unfrozen well-ordered parameter positions are described by a vector of ordinal lengths, one coordinate for each strict slot and each prescribed segment. There are set-many coordinates, even when \(T\) itself is not well-ordered. By the monotonicity requirement in Definition 43, a pointwise increase embeds the old layout and its designated terms into the new one. Unequal comparisons remain unequal because diagrams are preserved by the induced arrows.

For a fixed frozen pattern, apply Lemma 27 to the upward closure, among all ordinal vectors, of its valid unequal configurations. It gives a set of generators, which can be chosen from valid unequal configurations. Each generator has a set-sized parameter order. Take a cardinal above the sizes of the terms on all these orders, then above the resulting bounds for all the frozen patterns. An unequal configuration contains one of the generating configurations and is consequently witnessed on at most that many parameters. Increasing the bound monotonically gives \(g\). This is precisely the ordinal-vector proof of Proposition 28; its required ingredients here are natural diagrams, their preservation, and the explicit monotonicity of the layout, all verified above. Taking the same supremum over a set of descriptors proves the last assertion. ◻

Proof. For \(X\subseteq P\), let \(S_X\) be the union of its chosen supports. A profile records the labels of \(v\), its formal ordered support, and all comparisons and coincidences with \(S_X\). If \(|X|\le\chi\), there are at most \(\chi\) profiles. In each strict slot over \(S_X\), all the new positions there form one cluster. A profile has a continuation over the whole old order with no new event: place each cluster intact into a single strict slot of the old order extending its slot over \(S_X\). Order enlargement supplies positions if necessary. A new event on enlarging \(X\) means a new hit of an old position or a separation of two previously unseparated new positions by an old position.

Two continuations with no new event over \(S_Y\), for \(Y\supseteq X\), have the same diagram over \(Y\). Indeed, their differences consist of moving whole clusters past blocks of parameter supports. The regions belong to distinct slots, so the block transpositions in Lemma 42 apply simultaneously.

If simultaneous realization fails, choose \(X_0\) of size at most \(\chi\). For each profile over \(X_i\), choose a no-new-event continuation and one prescribed query where it fails. Adjoin those queries to \(X_i\) to obtain \(X_{i+1}\); at limits take unions. There are at most \(\chi\) profiles, each chosen query has size at most \(\chi\), and \(\sigma^+\le\chi\). Thus every \(X_i\), including \(X_{\sigma^+}\), has size at most \(\chi\). Choose a placement realizing the prescription on \(X_{\sigma^+}\). At every earlier step this placement must have a new event, since otherwise the no-event comparison would transfer the chosen failure to it. There are at most \(\sigma\) possible hits and at most \(\sigma\) pairs of new positions. Each event can occur for the first time only once. This contradicts the \(\sigma^+\) steps.

In a non-well-ordered chart, the number of profiles over \(X_i\) is at most \(2^{|X_i|+\sigma+b}\). Starting with the desired test size, use this as the next cardinal bound and include a failed query of at most that original test size for every profile. The larger sets \(X_i\) have prescriptions because those were supplied on all bounded subsets. More explicitly, start with an infinite \(\beta_0\) above the desired test size and set \(\beta_{i+1}=2^{\beta_i+\sigma+b}\), taking suprema at limits. Require the single bound \(\sup_{i\le\sigma^+}\beta_i\) to be strictly below the level. This is closure under the whole indicated recursion, rather than merely closure under each individual exponentiation. It keeps the final set bounded even though the level has countable cofinality. Its prescription is available by hypothesis, and the identical event count is a contradiction. This is a set recursion depending only on the starting arity and fixed data. ◻

Proof. A single bounded request is possible in a presentation: the parameter diagram is preserved by the arrow, and saturation realizes its desired extension over the actual parameters in a level object. Apply Lemma 45 at \(\chi=c(|v|+\aleph_0,\tau)\), for any desired bounded query size \(\tau\). Two outputs agree on all tests of size at most \(g(|v|+\aleph_0)\), and Proposition 44 identifies their full placed comparisons. For any bounded query, choose \(\tau\) large enough to include it. The unique comparison therefore computes every actual bounded diagram. This argument does not require an amalgamation relation on types. ◻

Proof. Write arrows as inclusions by taking renamed copies. We prove the stronger construction with a prescribed identification of bounded tuples; omit the tuples for ordinary amalgamation. Let the target initially be \(N_0=B_1\). Choose increasing bounded lists \(d_n\) exhausting \(B_0\), starting with \(d_0=v_0\) (or the empty list when no identification is prescribed). In each vertex also choose an increasing countable exhaustion by strong submodels of cardinality less than the level, and include their enumerations in the \(d_n\)’s. Such exhaustions exist by the component LS property, coherence and \(\mathop{\mathrm{cf}}(\mu)=\omega\).

We construct targets \(N_n\) and compatible images of \(d_n\). The invariant is equality of all bounded joint diagrams of \((d_n,A)\) with their original diagrams in \(B_0\). For the prescribed initial tuple this is the hypothesis and Lemma 46; the empty initial tuple is automatic.

Suppose an image of \(d_n\) has been chosen. In a well-ordered chart of \(N_n\), regard \(A\) and this whole image as the parameter set \(P\). For a bounded subset of \(P\), its required joint diagram with \(d_{n+1}\) is read in \(B_0\), interpreting the old image as \(d_n\). This prescription is well-defined on repetitions and coincidences by the invariant. It is locally possible: equality on the old parameters and saturation give a realization in \(N_n\). Choose a test cardinal of the form (1), large enough also for the length of \(d_n\), and apply Lemma 45. The resulting tuple lies in an order enlargement \(N_{n+1}\) and retains the old assignments.

To verify the invariant, use a natural well-ordered chart of the source \(A\). Both the desired tuple and the newly placed tuple have comparisons there by Lemma 46. Their agreement on the chosen tests includes the testing bound for the joint arity, so Proposition 44 makes their comparisons equal. They therefore agree on every bounded query in \(A\). We have not applied uniform layout testing to the possibly unnatural image of \(A\) in the target chart; compact placement alone was used on that image.

Take the union of the countable target chain. Its total size is \(\mu\), so the union and upper-bound clauses of the package give an object and an arrow from \(B_1\). The assignments define a map from \(B_0\) into this union. They match diagrams on increasing lists that exhaust \(B_0\) and include the component strong-submodel exhaustions. The image of each such small submodel is strong: the matching diagram of its enumeration is implemented by an isomorphism between its original containing object and the target object. The arrow criterion of the package consequently makes this map an arrow, including any extra basis condition already checked for the current scheme. The initial tuples have the same image. Necessity of diagram equality follows from preservation in any amalgam.

Amalgamation makes the identification relation transitive: amalgamate two witnesses over their common intervening object. Reflexivity and symmetry follow from identity maps and interchange of the two legs. The equivalence and testing descriptions now follow from the proved criterion and Lemma 46. ◻

Proof. Use the countable exhaustion in the preceding proof, with all source lists and testing thresholds below \(\nu\). Perform the compact placement in a chart of \(N\). The placed tuple, all of \(A\), and the previously assigned list together have cardinality at most \(\nu\), which is bounded at \(\mu\). Saturation at \(\mu\) therefore realizes their whole joint diagram back in the actual \(N\), fixing the existing parameters. Continue there, without enlarging the final target. For component strongness, first place the source object at level \(\mu\) by a presentation arrow. Mixed preservation and an isomorphism of \(\mu\)-objects implementing the matching enumeration show that every small source strong submodel has strong image in \(N\). The exhaustion criterion now gives the arrow.

To interpret a tuple of length less than \(\nu\) over \(A\) inside a larger object, take a \(\nu\)-subobject containing \(A\) and the tuple, using mixed LS. Coherence makes it an extension of \(A\). Mixed preservation identifies its diagrams with those in the larger object. The testing criterion shows independence of the chosen subobject. This also justifies the source-level type comparisons used during the construction. ◻

Proof. By the rich-order and padding constructions of Lemmas 36 and 35, present \(A\) on a padded dense order sufficiently saturated for every support size used below. The presentation is an object of the current scheme; categoricity in the package gives an isomorphism with \(A\). Lemma 46, or its compact-placement proof in the padded chart, places \(p\) correctly at size \(\tau\).

Keep every extra supporting position that belongs to the old chart. Partition the other supporting positions into clusters according to their strict cut over the entire old order. For every pair of distinct cuts choose an old position separating them. Include the shared supporting positions as well. This gives a bounded anchor set of size at most \(\sigma+\aleph_0\). Each unshared cluster now belongs to a different strict slot over the anchors.

In each such anchor slot, choose \(\kappa\) pairwise disjoint convex regions in the old order and, in the \(i\)th region, put a copy of the corresponding cluster with its internal order. The prescribed richness supplies these patterns; its required arity is bounded in terms of \(\sigma+\kappa\). Use the original labels and the unchanged shared positions to obtain \(v_i\in A\).

Choose a query \(Z\) and one finite support for each of its elements. If these supports avoid every region used for the \(i\)th copies, then each copied cluster and the original cluster can differ relative to the query only by passing whole blocks of parameter positions. There are no hits or separations inside a cluster. Their anchor slots are disjoint, so Lemma 42 gives \(D(v_i,Z)=p\mathord\upharpoonright Z\). Every supporting position of \(Z\) belongs to at most one of the regions, and therefore excludes at most one index \(i\). Finitarity of supports gives at most \(|Z|+\aleph_0\) excluded indices. The same set of good indices works for every subtuple of \(v\). Only bounded support patterns, the fixed labels, rich orders at bounded arities, and the compact-placement bounds were used. This proves the uniformity assertions. ◻

Proof. First fix a query bound \(\tau\) and take an approximation sequence \(I=(v_i:i<\kappa)\) in \(A\) with \(\kappa>\tau+\aleph_0\). Given a query \(Z\) in \(B\) of size at most \(\tau\), saturation moves it into \(A\) over the entire sequence: there is \(Z_0\subseteq A\), with the same enumeration, such that \[ D(I,Z)=D(I,Z_0). \tag{3}\] The total length \(|I|+|Z|\) is bounded. For mixed levels it is bounded at the originating level, and the mixed saturation clause applies. Define the answer on \(Z\) to be the majority of \(D(v_i,Z)\), equivalently the answer \(p\mathord\upharpoonright Z_0\). Equation (3) preserves every entry of the sequence, so this definition is independent of the chosen \(Z_0\) and retains the same exception estimate.

If \(I'\) is another sufficiently long approximation sequence, move \(Z\) into \(A\) over \(I\cup I'\). On that moved query both majorities compute the original \(p\). Thus the answers agree. This proof requires saturation over the concatenation of the sequences; it does not require either approximation estimate to hold for a query containing that concatenation. The averaging queries still have size at most \(\tau\). The identical argument compares different query bounds on their common domain. It also proves coherence under restrictions and reindexing of queries.

We next obtain an actual type. Use \(\tau=c(\sigma)\) and \(\kappa=\tau^+\). In a well-ordered chart of \(B\) prescribe the majority answers on every query of size at most \(\tau\). For each single query these are realized by some \(v_i\in A\subseteq B\), since fewer than \(\kappa\) indices are exceptional. Thus they have local placements. Lemma 45 gives a placement realizing all of them in an order enlargement of \(B\). This is an actual tuple in an extension object, and Theorem 47 makes its type unique, since \(\tau\ge g(\sigma)\). This type is \(p^B\). Its restriction to \(A\) equals \(p\) by the same testing criterion.

For a larger desired bounded query size \(\tau'\), repeat with a power closed bound at least \(c(\sigma,\tau')\). The comparison of sequences just proved identifies the resulting type with \(p^B\) on the initial testing threshold and hence everywhere. In a mixed-level use, this additional direct majority evaluation is asserted only when its costs remain below the originating level. The type itself is already actual over \(B\), and its diagrams at larger arities are those of this actual type; no averaging inside a smaller model at unbounded arities is being asserted.

Restriction to a subtuple commutes with every majority evaluation. Choose the threshold large enough for both arities and use testing to obtain equality of types. Isomorphism invariance follows by applying the isomorphism to the sequences and their query diagrams. For transitivity, let \(J\subseteq B\) be a canonical approximation sequence for \(p^B\) at a sufficient fixed threshold, and retain an original sequence \(I\subseteq A\) at that threshold. The latter computes \(p^B\) on queries in \(B\) by the construction. Move a query in \(C\) into \(B\) over \(I\cup J\). The two sequences give the same answer there, because each computes \(p^B\). The first also computes \(p^C\), and the second computes \((p^B)^C\). Testing proves transitivity. All these sequence lengths can be chosen as the uniform bounds in Lemma 50, below the smallest originating level. This proves the mixed-level assertions as well.

Finally, suppose \(J\subseteq B\) has the same whole diagram as a fixed code \(I\subseteq A\) at threshold \(c(\sigma)\). For each query \(Z\) in \(B\) of that size, saturation realizes \(D(J,Z)\) over \(I\) in \(A\). The resulting majority is therefore well-defined, with the same exception estimate. For each query one of the entries of \(J\) realizes the answer in \(B\). Coherence, compact placement and testing give an actual unique type, as in the preceding construction. Moving queries over code sequences shows that an arrow carrying \(J\) into a larger object gives exactly its free lift there. The code length and every threshold used here depend only on \(\sigma\) and the fixed scheme, which proves the final assertion. ◻

Proof. Let \(p=q\mathord\upharpoonright A\) and choose a canonical sequence \(J\subseteq A\) approximating \(p\) at size \(\chi\). For a query \(Z\subseteq B\) of that size, mixed saturation moves it to \(Z_0\) in \(A\) over the whole \(I\cup J\). The total length is less than \(\nu\). The majority from \(I\) on \(Z\) computes \(q\), and on \(Z_0\) computes \(p\). These answers agree by diagram preservation. The majority from \(J\) on \(Z_0\) also computes \(p\), and on \(Z\) computes \(p^B\). Hence \(q\) and \(p^B\) agree on all \(\chi\)-queries. Apply the testing criterion. The same proof works for an arbitrary longer indexed family whenever a bounded subsequence of the displayed length retains the exception estimate. ◻

Proof. Two realizations of \(p\) can be identified over \(A\) by amalgamation. In a common model containing their witnessing extensions, the free lifts of \(q\) agree by stationarity and restriction. A second type-identifying amalgamation identifies the realizations of \(q\). This proves independence of the choices in the definition.

We give the cardinal calculation for symmetry. Fix a bounded query \(Z\) in \(A\), and put \(e=|Z|+|x|+|y|+\aleph_0\). Choose approximation sequences \((a_i:i<\kappa)\) for \(p\) and \((b_j:j<\lambda)\) for \(q\), sufficient for queries of size \(e\), where \[\kappa=e^+,\qquad \lambda=\kappa^+.\] All these cardinals lie below a sufficiently closed level. For the array \(M_{ij}=D(a_i,b_j,Z)\), first realize \(x\) and freely realize \(y\). The resulting answer \(R\) is obtained by first taking the majority in \(i\) and then in \(j\). Except at at most \(e\) columns, the column majority is \(R\), and in each such column at most \(e\) entries differ from \(R\). Reversing the realization order gives an answer \(S\): except at at most \(e\) rows, its row majority is \(S\), with at most \(e\) exceptions in each such row. The bounds concern the size of \((x,Z)\) or \((y,Z)\), not the lengths of the sequences.

There are \(\kappa\) good rows. Their exceptional columns together number at most \(\kappa e=\kappa\). Since \(\lambda>\kappa\), choose a column outside this set and outside the at most \(e\) bad columns. Every good-row entry in that column equals \(S\), whereas all but at most \(e\) entries equal \(R\). As \(\kappa>e\), some entry has both values. Thus \(R=S\). This explains why two equally sized sequences would not suffice for the argument. Testing gives symmetry of the joint types.

For (4), take the two sequences just used in \(A\) and a sequence \(K\subseteq A\) approximating the actual old product. Choose their accuracy at a common sufficient test threshold. Given a query \(Z\) in the enlarged base \(B\), move it into \(A\) over these three whole sequences. Both successive free evaluations over \(B\) are the iterated majority of the same array \(D(a_i,b_j,Z)\). Transitivity permits the original sequence for the second factor to be used after the first factor has been realized. The query movement identifies this array with the old array in \(A\), where it computes \(p\otimes q\). The sequence \(K\) evaluates that old product and computes its free lift on the original query. The answers therefore agree. Testing proves the formula. All the lists fixed during the query movement are bounded, including in the mixed case.

Now realize \(x,y,z\) successively along a chain of free lifts from \(A\). The first two form \(p\otimes q\), and \(z\) is free over a model containing them, so the joint type is \((p\otimes q)\otimes r\). Over a model containing \(x\), the last two have type \(q^B\otimes r^B=(q\otimes r)^B\), by the formula just proved. Thus the same joint type is \(p\otimes(q\otimes r)\). This proves associativity. Projection follows from the projection property of free lifts in each successive realization. Associativity and the binary symmetry permit every permutation of a finite list of factors.

For the final assertion, use symmetry and a type-identifying amalgam to realize the given joint type by first putting \(d\) in a model containing \(B\) and then realizing \(x\) freely over it from \(B\). Since \(x/B\) is itself free from \(A\), transitivity makes this last realization free from \(A\). The tuple \((d,e)\) is in the intervening model, so the definition of product gives the assertion. The amalgam identifies the full original tuple over \(B\), and hence retains its actual joint type over \(A\). ◻

Proof. Pass to a cofinal chain indexed by the regular cardinal \(\gamma=\mathop{\mathrm{cf}}(\delta)\). Choose a sufficient testing size \(\chi\ge c(|v|+\aleph_0)\) below \(\mu\). If \(\gamma\) is larger than the size of an approximation sequence for \(p\) at that threshold, the whole sequence lies in one stage. Its exception estimate is still correct on all queries in \(A\), so Lemma 52, at the same level, applies.

In the other case \(\gamma<\mu\). Choose a regular \(\kappa<\mu\) above \(\gamma,\chi,|v|\) and the needed bounds, and take \(\kappa\) approximations inside \(A\). Every whole approximation tuple belongs to some stage: this uses finiteness, or the hypothesis \(|v|<\gamma\). If every stage contained fewer than \(\kappa\) of the tuples, regularity of \(\kappa\) and \(\gamma<\kappa\) would make their union contain fewer than \(\kappa\) tuples. Thus one stage contains \(\kappa\) of them. Pass to those indices. The exception estimate survives unchanged, and Lemma 52 again identifies \(p\) as the free lift from that stage.

For the final assertion, local character makes \(p\) free from some \(A_i\). Its restriction there is free from \(X\) by hypothesis. Transitivity in Theorem 51 makes \(p\) free from \(X\). ◻

Proof. Build \(S_\alpha\) for \(\alpha<\chi^+\), starting with the required set. At a successor stage, for every \(R\subseteq S_\alpha\) of size at most \(\chi\), and every order, equality and color pattern of at most \(\chi\) further positions over \(R\cup T^*\) that is actually realized in \(J_0\), choose one realizing tuple and adjoin its positions. Use unions at limits. If \(|S_\alpha|\le\kappa\), the number of choices of \(R\) is at most \(\kappa^\chi=\kappa\), and the number of patterns for each \(R\) is at most \(2^\lambda=\kappa\). Each chosen tuple adds at most \(\chi\) positions. Consequently every stage and their union have size at most \(\kappa\).

For \(R\) contained in the final union, regularity of \(\chi^+\) puts all of \(R\) into a single stage. The actual tuple \(Q\) witnesses that its pattern was among the requirements processed at the next stage. Its chosen witness is the required \(Q'\). Equality with elements of \(R\) and \(T^*\) is part of the pattern, so it is preserved literally. This also covers arbitrary enumerations and repetitions in \(Q\). ◻

Proof. We first realize a bounded type \(p(v/A)\) using just one fresh substrip \(V\). Choose a testing threshold \(\chi\ge c(|v|+\aleph_0)\) large enough also for \(|v|\) and the number of labels of \(G\). Take a sequence \(I\) in \(A\) approximating \(p\) at query size \(\chi\). Represent its entries by \(G\)-terms and collect their old supports in \(S_0\subseteq J\). Apply Lemma 55, with the side of \(V\) recorded, to obtain a bounded \(S\subseteq J\). Its closure permits every at-most-\(\chi\) old query pattern to move into \(S\) over any at-most-\(\chi\) subset of \(S\). The approximation supports, which may be larger than \(\chi\), can instead be included as the fixed set \(T^*\) in that Lemma. Thus all of them are fixed during every such movement.

Let \(P_S\) be the set of all \(G\)-terms on \(S\). It is bounded, since \(G\) has a bounded set of finite-support labels. The natural parameter diagram of \(P_S\) is the same in \(A\) and in \(G(S\cup V)\). The latter is a level object because \(|V|=\mu\). Saturation there realizes the desired whole joint diagram of \((v,P_S)\), giving a tuple \(w\) whose supporting positions belong to \(S\cup V\). Only at most \(|v|+\aleph_0\le\chi\) of its supporting positions are old; call them \(R\subseteq S\).

For any query \(Z\) in \(A\) of size at most \(\chi\), move its chosen support tuple into \(S\) over \(R\) and the fixed approximation supports, preserving the side of \(V\). Let \(Z'\) be the resulting term tuple. All comparisons with the new supporting positions of \(w\) in \(V\) are forced by that side. Naturalness therefore gives \[D(w,Z)=D(w,Z'),\qquad D(I,Z)=D(I,Z').\] The majority from \(I\) computes \(p\) on both queries. The chosen realization of \((v,P_S)\) gives \(D(w,Z')=p\mathord\upharpoonright Z'\). It follows that \(D(w,Z)=p\mathord\upharpoonright Z\). Testing of actual types, using a natural \(F\)-chart of \(A\) if \(G\) differs from \(F\), proves \(\mathop{\mathrm{tp}}(w/A)=p\). Naturality of \(G\) was used only for the displayed support movements; the testing and saturation are those already proved in \(\mathcal C\).

Now let \(B\ge A\) be arbitrary and choose increasing bounded lists \(d_n\) exhausting it, including countable strong-submodel exhaustions in every vertex. Use the first substrip to realize the type of \(d_0\) over \(A\). At subsequent step \(n\), the target base consists of \(A\) and the whole previously used substrips. Suppose \(d_n\) has already been assigned there with its correct type over \(A\). Theorem 47 amalgamates \(B\) with this target base over \(A\), identifying that entire assigned tuple. In this amalgam, \(d_{n+1}\) has an actual bounded type over the target base. Apply the one-substrip construction to the next fresh substrip. Since its type includes equality with the already assigned coordinates, the new assignment extends the previous one. The final union of the assignments lands in \(A^+\). The arrow criterion applies to the included strong-submodel exhaustions, so it is an arrow \(B\to A^+\) over \(A\). ◻

Proof. Present \(A\) by \(F\) on a well-order consisting of \(\mu\) disjoint convex blocks \(J_i\), each of cardinality \(\mu\) and itself containing countably many convex substrips of that size. The whole order still has cardinality \(\mu\), and the working package identifies its presentation with \(A\). Let \(A_i\) be the presentation on the complement of \(J_i\). It is a level subobject of \(A\). Proposition 56, with \(J_i\) as the inserted strip, embeds \(B\) into \(A\) over \(A_i\); call the arrow \(r_i\). Choose one finite supporting set for \(a\). It meets only finitely many \(J_i\). For every other index, \(a\in A_i\) and \(r_i(a)=a\). ◻

Proof. Coherence makes \(r_i\mathord\upharpoonright U':U'\to A'\) an arrow: its image and \(A'\) are subobjects of \(A\), and its image is contained in \(A'\). Put \(\sigma=|d|+\aleph_0\), choose \(\chi\ge c(\sigma)\) below \(\nu\), and choose \(\chi^+\le\kappa<\nu\). Retain any \(\kappa\) indices and form \(I=(r_i(d))\) on them. This is a bounded concatenated list in \(A'\).

For a query \(Z\subseteq A\) of size at most \(\chi\), at most \(|Z|+\aleph_0\) indices fail to fix every element of \(Z\). At every other index, arrow preservation gives \[D(r_i(d),Z)=D(r_i(d),r_i(Z))=D(d,Z).\] Thus \(I\) has the required majority estimate for the actual type over \(A\). On queries in \(A'\) the same identity is a comparison at level \(\nu\), using the restricted arrows. Mixed preservation identifies it with the larger-level identity.

Apply Lemma 52 to \(A'\le A\). Its restriction type is precisely \(\mathop{\mathrm{tp}}(d/A';U')\), by Corollary 48. The conclusion is therefore the stated free lifting of the actual type, including tuples that span a chosen resolution of \(U'\). ◻

Proof. For the first assertion, write \(c=(c_0,c_1)\) and let \(Z\) isolate \(q\). Suppose \((u',c'_0)\) has the prescribed marginal on \(u\) and the same diagram as \((u,c_0)\) over \(Z\). In a model containing \(A,u',c'_0\), bounded saturation extends this diagram by a tuple \(c'_1\) so that \[D(u',c'_0,c'_1,Z)=D(u,c_0,c_1,Z).\] Isolation identifies the full type over \(A\), and its projection identifies \(\mathop{\mathrm{tp}}(u',c'_0/A)\).

For the second assertion, fix an isolating fragment \(Z\). It is enough to compare the actual joint type over \(B\) with \(q^{\mathrm{fr}}_B\) on the uniform testing arity for \((u,c)\). Enlarge that arity to include \(Z\) and choose approximation lists in \(A\) for both \(q\) and \(p=\mathop{\mathrm{tp}}(u/A)\), long enough to evaluate all the comparisons just specified. Let \(t\) be a test tuple from \(B\) at this enlarged arity. Bounded saturation moves \(t\) to a tuple \(t'\) in \(A\), preserving its diagram over \(Z\) and both approximation lists.

Choose a realization \(u_0\) of \(p\) over \(A\). The free evaluation of \(p\) gives \[D(u,t,Z)=D(u_0,t',Z).\] Saturation over the bounded list \((u_0,t',Z)\) supplies \(c_0\) such that \[D(u_0,c_0,t',Z)=D(u,c,t,Z).\] In particular \((u_0,c_0)\) agrees with \(q\) on \(Z\) and has marginal \(p\). Isolation gives \(\mathop{\mathrm{tp}}(u_0,c_0/A)=q\). Consequently the actual answer to the query \(t\) is the answer that \(q\) gives to \(t'\). Because the query was moved over the approximation list for \(q\), that is also the free evaluation of \(q\) on \(t\). The testing theorem identifies the types over \(B\).

Now let a competing type over \(B\) have the same marginal on \(u\) and agree with the displayed type on \(Z\). Its restriction to \(A\) is \(q\). The argument just given identifies it with \(q^{\mathrm{fr}}_B\), proving isolation there. In the mixed-level case, perform these comparisons at the uniform test bound below the source level. Mixed realization supplies the required sections, and the same argument applies to those diagrams. ◻

Proof. Choose an infinite \(\chi\) large enough for the testing theorem at arity \(\sigma\), for the approximation lists for \(q\) and its marginal \(p\), and for the finitely many joint comparisons made below. These choices are uniform in \(\sigma\). Increasing \(\chi\) if necessary, all the supports in the chosen approximation lists have cardinality at most \(\chi\).

Present \(A=F(I)\) on a well-order of the level cardinality \(\mu\). We may choose \(I\) to have more than \(\sigma\) disjoint consecutive blocks, each of order type and cardinality \(\mu\): this is still a well-order of cardinality \(\mu\), and all such presentations are objects at this level. Let \(J_0\) consist of the supports of the approximation lists, together with an initial segment of order type \(\chi^+\) in every candidate block. Its size has a bound depending only on \(\sigma\). Let \(Z_0\) be the set of all term values on \(J_0\). Since the label set is fixed, the same is true of \(|Z_0|\).

If \(Z_0\) isolates \(q\), we have the first alternative. Suppose it does not. Choose \(q^1\ne q^0=q\) with the same marginal \(p\) and the same diagram on \(Z_0\). By Lemma 45, give both types placements over the displayed presentation of \(A\), and amalgamate their support orders over \(I\). The combined new support has cardinality at most \(\sigma\). Each new support position either hits the interior of one candidate block or determines an interior cut of at most one such block. We can therefore choose a candidate block \(J\) whose interior contains neither a hit nor a cut of either placement.

Set \(A_*=F(J_0\cup J)\leq A\). This object has cardinality \(\mu\). The restrictions of \(q^0\) and \(q^1\) to \(A_*\) are equal. To check this, take a test at the fixed sufficient arity. Move every position of the test lying in \(J\) into the initial \(\chi^+\) part of \(J\), preserving the order and equality pattern of the test. This can be done above any positions of that initial part which need to remain in the pattern: fewer than \(\chi^+\) positions have been specified. Leave the positions outside \(J\) unchanged. No position of either candidate separates the interior of \(J\), so the move preserves the natural diagram with either candidate. The moved query uses only \(J_0\) and therefore has the same answer for \(q^0\) and \(q^1\). The testing theorem proves equality over \(A_*\).

The approximation lists for \(q^0\) and \(p\) lie in \(A_*\). Their majority evaluations show that \(q^0\) and \(p\) over \(A\) are free from \(A_*\). Also, an isomorphism \(f:A_*\simeq A\) may be chosen to fix those bounded lists, by bounded diagram homogeneity. The transport assertion for free types then gives \[f\bigl(q^0\mathbin{\upharpoonright}A_*\bigr)=q.\] Transport the inclusion \(A_*\leq A\) along \(f\), viewing its larger object as an extension \(B\) of the original base \(A\). Transport \(q^1\) as well. Its restriction is \(q\) because the two restrictions to \(A_*\) agree. Its marginal is the free lift of \(p\). Its joint type is not free, since the unique free lift before transport was \(q^0\), distinct from \(q^1\). This is the second alternative.

Choose \(h(\sigma)\) to bound the size of \(Z_0\) for these uniform choices. Lemma 60 excludes the second alternative when \(q\) is isolated, even if an initially given isolating fragment was larger. This proves both exclusivity and the asserted uniform bound. ◻

Proof. Choose increasing bounded lists \(c_n\), \(n<\omega\), exhausting \(Y\); include \(b\), the prescribed initial data, and exhaustions of every vertex by smaller strong submodels. Suppose the image of \(c_n\) has already been chosen with the correct full type over \(X\). Let \(Z_{n+1}\subseteq X\) isolate \(\mathop{\mathrm{tp}}(b,c_{n+1}/X)\). The old image and the source list have the same diagram over \(Z_{n+1}\). Saturation in \(N\) extends this bounded match to \((b,c_{n+1},Z_{n+1})\). Relative isolation makes its full type over \(X\) correct. Taking the union gives a map on all of \(Y\) fixing \(X\): whenever an entry of \(X\) occurs in a list, its equality with the corresponding parameter is part of its full type. The strong-submodel exhaustions and the map criterion in the working package show that this map is an arrow. This proves the first assertion, also into a larger target because every saturation request is bounded at the source level.

For the second assertion, perform the same construction alternately on the two sides, at each step including the next list in the chosen exhaustion on the side to be covered. Both objects have isolation for the enlarged bounded list. The construction therefore continues in both directions and its union is an onto structural isomorphism.

For the third assertion, use symmetry and the definition of product to choose a model \(W\geq X\) containing \(x\) over which \(b\) is free from \(X\). Type-identifying amalgamation brings \(W\) and the actual coupling into a common extension, identifying \(x\) and \(b\) over \(X\). For every bounded \(c\) in \(Y\), Lemma 60 says that \((b,c)/W\) is free from \(X\). Hence \(x\) and \((b,c)\) have product over \(X\). Symmetry and projection give the free evaluation of \(x\) on every bounded test \(c\) from \(Y\). The testing theorem identifies \(\mathop{\mathrm{tp}}(x/Y)\) with the free lift of \(\mathop{\mathrm{tp}}(x/X)\). ◻

Proof. By Proposition 61, choose a large-base isolating fragment \(W\subseteq B\) with \[|W|\leq h(|u,c|+\aleph_0)<\nu.\] Let \(w\) enumerate \(W\). The type \(\mathop{\mathrm{tp}}(w/A)\) is a small-level type, computed by taking a level-\(\nu\) section containing \(A\) and \(w\). Choose a sufficiently long bounded approximation list \((w_i)_{i<\tau}\) for this type inside \(A\), where \(\tau<\nu\). Enlarge its testing bound to include the arities of \(w\) and \((u,c)\) and choose \(\tau\) larger than the two exception bounds that will occur below. Put \[Z=\bigcup_{i<\tau}\mathop{\mathrm{ran}}(w_i)\subseteq A.\] This is a bounded fragment.

Let \(q'_A\) have the same marginal on \(u\) as \(q_A\) and agree with it over \(Z\). Lift \(q'_A\) freely to \(B\). The marginal on \(u\) then agrees with the marginal of \(q_B\). In either free coupling, symmetry identifies the joint diagram with \(w\) by the majority evaluation of \(\mathop{\mathrm{tp}}(w/A)\) against the candidate tuple. Thus all but the prescribed bounded number of \(i<\tau\) give the diagram of that candidate with \(w\). Choose one index outside the two exception sets. The candidates agree on \(w_i\), because \(w_i\) lies in \(Z\), so their free lifts agree on \(w\). Isolation of \(q_B\) identifies the free lifts, and restriction identifies \(q'_A\) with \(q_A\). Every approximation and comparison here has size below \(\nu\); no approximation to the whole of \(B\) is used. ◻

Proof. We prove the more general statement. Fix a bounded approximation list \(I_p\) in \(X\) which determines \(p\) at a sufficient testing arity. Choose a much larger eligible level \(\kappa\) and a cardinal \(\rho\) such that \[\lambda<\rho=\rho^\lambda, \qquad \rho^+<\kappa.\] Require \(\rho\) to dominate the approximation and small-hull costs at arity \(\lambda\), and choose \(\kappa\) after those set-sized bounds. Such choices exist: first choose a sufficiently large power \(2^\xi\) with \(\xi\geq\lambda\) for \(\rho\), and then choose an eligible \(\kappa\) above \(\rho^+\) and all remaining bounds. Extend \(X\) by a presentation arrow to a level-\(\kappa\) object \(X_0\), and choose \(Y_0\geq X_0\) containing a realization \(b\) of the free lift of \(p\).

We construct continuous pairs \[X_i\leq Y_i\qquad(i\leq\rho^+)\] at level \(\kappa\), with a single fixed \(b\) in all the upper objects. The invariant on the marked marginal is \[ \mathop{\mathrm{tp}}(b/X_i)=\mathop{\mathrm{tp}}(b/X_0)^{\mathrm{fr}}_{X_i}. \tag{5}\] For \(i<\rho^+\), we also keep increasing continuous sets \[R_i\subseteq X_i,\qquad S_i\subseteq Y_i,\qquad R_i\subseteq S_i,\qquad |R_i|,|S_i|\leq\rho,\] with \(I_p\subseteq R_i\) and \(b\subseteq S_i\). They are bookkeeping sets, not additional structure on the objects.

Here are the two closure requirements at a stage \(i\) with \(\mathop{\mathrm{cf}}(i)>\lambda\).

1. Any specified at-most-\(\lambda\) sets of base and top parameters from \(R_i,S_i\) are contained in a pair \(A\leq V\) of level-\(\lambda\) subobjects of \(X_i\leq Y_i\), with \(A\subseteq R_i\) and \(V\subseteq S_i\).

2. Every tuple \(d\) of length at most \(\lambda\) from \(S_i\) has a sequence of at least \(\lambda\) copies inside \(R_i\) computing its actual type over \(X_i\) on all tests of size less than \(\lambda\). For every subtuple and each such parameter test \(Z\), all but at most \(|Z|+\aleph_0\) of the copies give its joint \(D\)-diagram.

We explain how to arrange the requirements; in particular, they do not amount to assuming a small saturated submodel. At successor stages, process all at-most-\(\lambda\) lists in the current parameter sets. There are at most \(\rho^\lambda=\rho\) of them. Mixed Löwenheim–Skolem supplies the requested level-\(\lambda\) pairs. Lemma 50 supplies copies of each top list in the current base, at the test sizes below \(\lambda\) and with the displayed exception estimate. Their total number of coordinates is at most \(\rho\). Close the sets under these operations for \(\lambda^+\) steps; the size is still \(\rho\). If new elements are added later, repeat these successor closures. At a limit \(i\) of cofinality greater than \(\lambda\), every requested list was contained at an earlier stage. Local character applied to that list, whose length is at most \(\lambda<\mathop{\mathrm{cf}}(i)\), says that its actual type over \(X_i\) is free from some earlier stage. Approximations placed in a later intervening successor base still compute it over \(X_i\) by the free-extension theorem. Their copies lie in \(R_i\). The same cofinality argument places every small-hull request in an earlier closure. This proves both requirements at the indicated limits.

At any such stage, if some list \(d\) of length at most \(\lambda\) from \(S_i\) makes \(\mathop{\mathrm{tp}}(b,d/X_i)\) nonisolated relative to \(b\), apply Proposition 61. It gives a same-level extension of \(X_i\) in which this joint type has a nonfree extension while the \(b\)-marginal remains free. By type-identifying amalgamation, extend \(Y_i\) into a common \(Y_{i+1}\), identifying the old \((b,d)\) with that realization. The new base is the extension just chosen. Transitivity preserves (5). At other stages use compatible extensions and the bookkeeping closures. At limits use the working scheme’s unions; Definition 65 preserves the marginal invariant. All these unions have size \(\kappa\), since \(\rho^+<\kappa\).

This process must reach an indicated stage at which every list in the second closure requirement is isolated jointly with \(b\). Suppose not, and choose a failing list \(d_i\) at every stage with \(\mathop{\mathrm{cf}}(i)>\lambda\). The set of these stages is stationary in the regular cardinal \(\rho^+\). Indeed, in any closed unbounded subset of \(\rho^+\) take a continuous increasing sequence of length \(\lambda^+\) and its supremum; the supremum is still below \(\rho^+\), is in the closed set, and has cofinality \(\lambda^+\).

Because \(S_i\) is continuous and \(|d_i|\leq\lambda<\mathop{\mathrm{cf}}(i)\), there is \(j(i)<i\) with \(d_i\subseteq S_{j(i)}\). Fodor’s pressing-down argument (Fodor 1956) makes \(j(i)\) constant on a stationary subset. For completeness, if every fiber of a regressive map on a stationary subset of a regular cardinal were nonstationary, choose a closed unbounded set avoiding each fiber. Their diagonal intersection is closed unbounded and gives a contradiction at a point of the stationary set. The diagonal intersection is unbounded by taking an increasing countable sequence whose next point is in all the clubs indexed below the previous point; the needed intersections of fewer than the regular cardinal many clubs are closed unbounded, by interleaving their choices and taking a limit. Thus this application uses only set-indexed choices in ZFC.

There are at most \(\rho^\lambda=\rho\) possible lists in the resulting fixed \(S_j\). Partitioning the stationary subset into these \(\rho\) possibilities retains a stationary piece: otherwise the intersection of \(\rho<\rho^+\) clubs avoiding the pieces is a contradiction. Consequently one fixed list \(d\) witnesses nonfree extensions at stationarily many stages. In the final union, the tuple \((b,d)\) has length at most \(\lambda<\rho^+\). Local character makes its type free from some \(X_j\). Its restrictions at every later successor are then free from their preceding base, contradicting the chosen stationarily many nonfree extensions.

Fix a stage \(i\) at which all the required lists are isolated. We next shrink, and this step must preserve freeness for the tuples on which isolation will be transferred. Construct increasing pairs \[A_\alpha\leq U_\alpha\qquad(\alpha<\theta^+)\] of level-\(\lambda\) subobjects inside \(R_i,S_i\). Keep \(I_p\) in every base and \(b\) in every top. At successor stage \(\alpha+1\), take a tuple enumerating \(U_\alpha\). By the second closure requirement it has \(\lambda\) approximation copies in \(R_i\). Include every coordinate of these copies in \(A_{\alpha+1}\), and include \(A_\alpha,U_\alpha\) in the next pair, using the first closure requirement. The requests have cardinality \(\lambda\). At proper limits take unions; the upper bound clause into \(X_i,Y_i\) keeps them strong there. Finally put \[A=\bigcup_{\alpha<\theta^+}A_\alpha, \qquad U=\bigcup_{\alpha<\theta^+}U_\alpha.\] Because \(\lambda\) is strong limit and \(\theta<\lambda\), we have \(\theta^+<\lambda\). Both unions are level-\(\lambda\) objects, and the common upper bound clause gives \(A\leq U\).

Let \(c\) have length at most \(\theta\) in \(U\). Regularity of \(\theta^+\) puts \((b,c)\) inside some \(U_\alpha\). The next base contains \(\lambda\) copies of its type over \(X_i\), with the exception estimates above. For any fixed sufficient testing arity below \(\lambda\), select a bounded subsequence longer than that arity’s exception bound. These copies are inside \(A\) and compute the actual large-base type. The majority characterization of free extension now says that \[\mathop{\mathrm{tp}}(b,c/X_i)=\mathop{\mathrm{tp}}(b,c/A)^{\mathrm{fr}}_{X_i}.\] Explicitly, move a large-base query into \(A\) over the selected copies and over canonical approximations for the small type. Choose an index outside the exception sets for the query and its moved copy. The actual answer therefore equals the small free evaluation. The testing theorem identifies the whole type. The bounds needed for this argument are below \(\lambda\), since \(|b,c|\leq\theta\).

The large type is isolated by the choice of \(i\). Its uniform fragment has size at most \(h(|b,c|+\aleph_0)<\lambda\), so Lemma 64 gives isolation over \(A\). Finally, \(I_p\) still determines the marginal on \(b\): it did so at \(X_0\), the matrix preserved its free lift, and the same approximation answers hold on restriction to \(A\). Bounded diagram homogeneity gives an isomorphism \(A\simeq X\) carrying these anchors to themselves. Transport of approximation evaluations carries \(\mathop{\mathrm{tp}}(b/A)\) to \(p\). Renaming \(U\) along this isomorphism gives the asserted extension of the original \(X\). ◻

Proof. Write \(\nu\) for the desired level and fix sufficient bounded anchors \(I_p\subseteq X\) for the input marginal. Choose a much larger eligible \(\lambda>\nu\) and lift the type to a level-\(\lambda\) base by a presentation arrow. Apply Proposition 66 at level \(\lambda\) with \(\theta=\nu\). We obtain a pair \(A\leq U\) of level \(\lambda\) such that every tuple of length at most \(\nu\) in \(U\), jointly with \(b\), has isolation relative to \(b\) over \(A\). The original anchors may be retained in \(A\) throughout that construction.

Choose \(\nu\) distinct indices from the family in Corollary 57, and write the corresponding approximate retractions as \[r_j:U\longrightarrow A\qquad(j<\nu)\] such that each \(a\in A\) is fixed by all but finitely many of them. Use mixed Löwenheim–Skolem to choose level-\(\nu\) subobjects \(A'\leq U'\) of \(A\leq U\) which contain \(I_p,b\) in their indicated places and satisfy \[ r_j[U']\subseteq A'\qquad(j<\nu). \tag{6}\] Here is the closure construction. Start with level-\(\nu\) sections containing the desired entries. From the current top of size \(\nu\), adjoin to the next base all its images under the \(\nu\) selected maps; there are at most \(\nu\cdot\nu=\nu\) coordinates. Enlarge the next top to contain that base and the old top. Iterate countably many times and take unions. Same-level chain closure and the common upper bound clause into \(A,U\) give the pair and (6).

Fix any bounded tuple \(d\) in \(U'\). The tuple \((b,d)\) is still bounded at \(\nu\). The maps in (6) place all its images in \(A'\). For a test \(Z\subseteq A\), all but at most \(|Z|+\aleph_0\) of the maps fix \(Z\) pointwise, and hence for all those indices \[D(r_j(b,d),Z)=D(b,d,Z).\] At a fixed testing arity below \(\nu\), choose a bounded subsequence of indices longer than the exception bound. Lemma 58 gives \[\mathop{\mathrm{tp}}(b,d/A)=\mathop{\mathrm{tp}}(b,d/A')^{\mathrm{fr}}_A.\] The type on the left is isolated, by the length-\(\nu\) assertion at level \(\lambda\). Its uniform fragment bound for the actual arity \(|b,d|<\nu\) is below \(\nu\). Downward transfer gives isolation of \(\mathop{\mathrm{tp}}(b,d/A')\) relative to \(b\).

This argument applies separately to every bounded \(d\subseteq U'\); it makes no assumption that \(d\) lies in one stage of the countable construction. Thus \(U'\) is all-dominated over \(A'+b\). The retained anchors and bounded diagram homogeneity identify its marginal with the original \(p\) by an isomorphism \(A'\simeq X\). Transport gives the required object over \(X\). Its embedding into an actual ambient is Proposition 63. ◻

Proof. Induct on the stage. At a successor \(i+1\), the finite tuple \((x,b_i)\) has product with every finite selection of earlier marks, by the finite product rules. The induction hypothesis applied to this tuple says that its joint type over \(M_i\) is free from \(A\). Products lift freely by Proposition 53; hence \(x\) and \(b_i\) still have product over \(M_i\). Proposition 63, applied to the all-dominated increment \(M_{i+1}\), makes \(x/M_{i+1}\) free from \(M_i\). Transitivity makes it free from \(A\).

At a limit \(j\), local character for the finite tuple \(x\) gives a proper stage \(i<j\) from which \(x/M_j\) is free. The induction hypothesis and transitivity give freeness from \(A\). All types are computed in the actual coupled ambient, so this argument asserts continuity of the specified realization, not merely existence of some independent realization at the limit. ◻

Proof. For the first assertion, maintain a common ambient containing the original list and the already constructed witnessing chain. At stage \(i\), finite domination makes the actual \(b_i\) free over \(M_i\) from \(A\): its products with finite selections of previous marks are still the original ones, since arrows preserve types. Theorem 67 supplies an all-dominated realization over \(M_i+b_i\). Primeness embeds it into a compatible actual ambient over this tuple; alternatively, type-identifying amalgamation supplies such an ambient while retaining the original list. At limits take the coherent unions. Finite domination continues to apply, and the chain has the stipulated total size.

For uniqueness, let \(M_i^0,M_i^1\) be the two witnessing chains. Build common objects \(N_i\) and coherent arrows from \(M_i^0,M_i^1\) into \(N_i\), agreeing on \(A\) and identifying all marks already processed. At a successor, take the free lift over \(N_i\) of the next common marginal type over \(A\), with realization \(c\). Its restriction to either image of \(M_i^r\) is the prescribed type of \(b_i^r\), by transitivity. Amalgamate the next stage \(M_{i+1}^0\) with this realization over its old stage, identifying \(b_i^0\) with \(c\). Then amalgamate \(M_{i+1}^1\) in the same way, identifying its mark with the same \(c\). The first amalgamation preserves the type of \(c\) over the other old-stage image, so the second identification is legitimate. Retain the old common object throughout. At limits, coherent unions give the required arrows. The final common ambient identifies every mark. Only bounded individual marginal types were used in a single step, which proves the stated version for bounded individual tuples as well. ◻

Proof. Lemma 70 supplies witnesses for any actual list with the specified finite products and identifies their whole types. The finite projections of a free lift are the free lifts of the finite projections, by Proposition 53. They are therefore the required products of the lifted marginal types. Applying witnessed uniqueness at the receiving base proves the first assertion, including its mixed-level interpretation.

For continuity, take the actual coupled chain in Definition 65. Each finite sublist of the fixed mark is a finite tuple. Its actual free evaluations at the proper stages persist at the union by local character and transitivity. These finite data are precisely the finite data of the free lift of the original whole marginal. By the first assertion they determine its whole type at the union. This proves the second assertion without applying finite-tuple local character directly to the possibly long mark.

We may now apply the general forms of Proposition 66 and Theorem 67. To check the additional arity conditions, choose the auxiliary \(\theta\) at least \(|b|\). The parameter-set scheduling then handles \((b,d)\) at length at most \(\lambda\), and the final stationary contradiction uses length \(\lambda<\rho^+\). At limits of the matrix construction, the continuity just proved preserves the fixed marked marginal. All approximation and isolation bounds are evaluated at the actual bounded joint arities. The all-length descent uses the same retractions on the concatenations \((b,d)\), which remain bounded at the desired level. Thus all hypotheses of the two existence results hold. Primeness gives the assertion about the actual ambient. ◻

Proof. The samples and their language. Let \(F\) be the template of \(\mathcal C\). At arbitrarily high closed input levels choose a pair \[X=F(J)\leq Y,\qquad Y\cong F(Z),\] with \(Y\) all-dominated over \(X+b\). Choose the presentations sufficiently rich for any prescribed set-sized order-saturation bound. We may take \(J,Z\), and a further order \(W\), to be padded dense orders. Padding means that the order has a well-ordered subset of its own cardinality. In addition, \(W\) has many disjoint convex substrips, each of the level size. Proposition 56, in its presentation-invariant form, puts \(Y\) over \(X\) into \[L=F(J+W).\] All these choices concern the already working scheme \(\mathcal C\).

Expand a sample by sorts for the orders and charts, chart evaluation maps, the inclusions, and the mark. For each element of a chart choose a representing label and its finite list of positions. Representation tags record the label arity; coordinate functions have default values outside their arity. Include a sort of retraction indices and an evaluation function for a family \[r_i:Y\longrightarrow X\] from Corollary 57. Distinct indices are retained as distinct indices, even if two of their maps happen to be equal.

Finally include finitary LS witness functions for the underlying \(K\)-vertices. For each finite list in a vertex choose a small strong submodel containing it and the models already chosen for its proper sublists, and enumerate that model. Coherence gives strong inclusions between these small models. Perform this in all the finitely many vertex occurrences, including the required inclusion data. In the term closure of any generating set, these enumerated small submodels form a directed cover of each vertex intersection: every finite tuple has its witness model there, and a witness for a combined tuple contains the earlier witnesses. Thus the intersection is strong by the directed-union axioms. Designated entries keep the necessary sorts nonempty.

This is one fixed set-sized finitary expansion. It names neither the diagram table nor all the elements of a high sample. Its number of terms has a bound in the old template language and the fixed input data.

Homogeneous finite hulls. In each sample take a long ordinal-indexed sequence bundling an increasing sequence in each order sort and a sequence of distinct retraction indices. Color a finite index set by the complete labelled atomic diagram, with negations and equalities, of its term hull and the inclusions among the hulls of its subsets. The palette has a fixed set bound. The finite-arity extraction used in Theorem 9 chooses compatible colors at all finite arities while retaining arbitrarily large homogeneous samples. Retain at the same time arbitrarily high prescribed order-saturation bounds. Treat the requested homogeneous size and the requested order saturation as one cardinal demand. If each possible next color had a bound on the demands it could meet, the supremum of those set-many bounds would contradict the availability of samples. Thus a single next color retains unbounded demands. Thinning the horizontal sequence does not change the saturation of its ambient chart orders.

Let \(H\) be a well-order of a sufficiently closed input size \(\lambda\), and evaluate the extracted term data on \(H\). Write the resulting chart orders as \(J_H,W_H,Z_H\), and the underlying objects as \(X_H,Y_H,L_H\). The evaluation and representation functions give both directions of generation: \[X_H=F(J_H),\qquad Y_H\cong F(Z_H),\qquad L_H=F(J_H+W_H).\] Representation equalities concern fixed finite tuples of terms and therefore hold in actual homogeneous samples. The increasing distinguished sequences pad the chart orders. Extending the old template to padded orders uses only the underlying scheme’s chain and directed-union properties.

The vertex LS witnesses prove \[X_H\longrightarrow Y_H\longrightarrow L_H\] componentwise strong over \(X_H\to L_H\). They also prove this for maps induced by order embeddings of \(H\), including mixed sizes. Each witness model is an isomorphic copy of its sample model, and the full component map is a directed union of these strong maps. Since arrows of \(\mathcal C\) are componentwise, these are underlying arrows. All-domination remains to be proved.

Bounded horizontal arity. Fix a bounded list \(u=(b,c)\) from \(Y_H\) such that each individual entry has a term representation using at most \(q\) horizontal indices, for one common finite \(q\). This is a bound per entry: the union of the supports of the whole bounded list may be infinite. Term depths need not be bounded. Coordinate functions and representations preserve finite support. Thus the positions representing \(u\) in \(J_H+W_H\) use a fixed finite number of indices per position. The positions representing \(r_i(u)\) in \(J_H\), for the \(\lambda\) distinguished retraction indices, require only the additional index \(i\). Comparing two such positions requires at most twice a fixed finite arity.

Take an actual sample homogeneous at these arities, with a horizontal index set containing an order copy of \(H\). The specified positions match those representing an actual tuple \(u_*\in Y\) and its images under the corresponding actual retractions. Choose the sample with order saturation above \(\lambda\). Extend the partial matches to embeddings of the entire orders \(J_H,W_H\) into the respective sample orders. In a recursion of at most \(\lambda\) steps, each next position specifies an order pattern over at most \(\lambda\) earlier positions, and sample order saturation realizes it. The initial partial maps are order embeddings by the recorded comparisons. We are not extending a map of the entire expanded term hull.

The host-order embedding identifies \(u\) with \(u_*\) and embeds \(X_H\) into \(X\). The mixed stationary prescription first shows that the mark in \(Y_H\) realizes \(p_{X_H}\). We next prove the stronger assertion needed for isolation: \[ \mathop{\mathrm{tp}}(u_*/X)\text{ is the free extension of }\mathop{\mathrm{tp}}(u/X_H). \tag{7}\] The images of \(u_*\) under the \(\lambda\) selected actual retractions belong to the embedded \(X_H\), because their representing positions were included in the partial matching. Choose a test bound \(\chi<\lambda\) above the costs for the arity of \(u\), and retain a set of \(\kappa\) selected retractions with \(\chi+\aleph_0<\kappa<\lambda\). Their images of \(u_*\) form a bounded list in \(X_H\). For each \(Z\subseteq X\) with \(|Z|\leq\chi\), all but at most \(|Z|+\aleph_0\) of these retractions fix \(Z\) pointwise. At every other index, diagram preservation identifies the diagram of its image of \(u_*\) with \(Z\) with the diagram of \(u_*\) with \(Z\). Thus this image list computes the actual type over \(X\) with the majority estimate of Lemma 52. That Lemma gives (7). Only images of the tested tuple have been placed in \(X_H\); closure of the entire small upper object under these retractions is neither claimed nor needed here.

The actual sample pair is all-dominated. Apply Lemma 64 to (7); its fragment bound is below \(\lambda\) by closure. It follows that \(\mathop{\mathrm{tp}}(b,c/X_H)\) is isolated relative to \(b\).

Removing the arity restriction. Let \(V\) be all-dominated over \(X_H+b'\), with \(b'\) of the prescribed type. We construct an arrow \[Y_H\longrightarrow V\] over \(X_H\), taking \(b\) to \(b'\). Choose nested bounded lists exhausting \(Y_H\) in countably many steps. They may be chosen so that at each step every entry uses at most a fixed finite number of horizontal indices: increase a cardinal bound cofinally to \(\lambda\) and the finite index-arity bound at the same time. Every term has finite arity. Include also full enumerations of small vertex witness models for finite index sets in the corresponding bounded part of \(H\). Their enumerated entries still have uniformly finite horizontal arity per entry, independently of term depth.

At each step the whole new list, the preceding list, and \(b\) satisfy the isolation conclusion already proved. The constructive primeness argument of Proposition 63 realizes the new list over the previous assignment and \(X_H\). Its isolating fragment together with the preceding list is bounded; underlying saturation supplies the realization. Isolation gives equality of the full types over \(X_H\). The included vertex witness models give strongness of the union map. Every bounded tuple of its image in \(V\) has isolated joint type with the mark. Consequently every bounded tuple of \(Y_H\), with no arity restriction, has this property. Thus \(Y_H\) is all-dominated.

The remaining pre-closure properties. Any marked pair at the level has a base isomorphic to \(X_H\), and Lemma 73 extends this to a pair isomorphism. The same Lemma gives orbit preservation and mixed reflection. For a set of at most \(\nu\) entries in a larger pair, take its horizontal supports and a well-ordered subpresentation of size \(\nu\) containing them. Its value is a marked pair by the individual template assertion just proved; coherence gives mixed downward Löwenheim–Skolem.

Naturalness on well-orders follows by putting any fixed bounded patterns into a common well-order enlargement and using orbit preservation. Mixed reflection makes these comparisons independent of the eligible level. Here are the remaining diagram details, without assuming the union clause in Definition 33. Define comparison of bounded term patterns by their pair isomorphism orbits at any eligible level. The preservation and reflection just proved make this independent of the level. At each fixed arity, the labels and order patterns belong to a fixed set, giving a uniform orbit bound. A mixed arrow factors, by mixed downward Löwenheim–Skolem and coherence, through a subpresentation of the target at its source level. Same-level orbit preservation in this factor and the level-independent pattern comparison give mixed diagram preservation. For saturation, represent a possible joint diagram in a larger well-ordered pair presentation. Its support has size below the receiving level, so that well-ordered support pattern embeds in a well-order at the receiving level. Evaluating \(F^b\) there realizes the joint diagram. The old subtuple has the orbit of the prescribed actual old tuple, so an isomorphism of the pairs carries the new realization over that tuple. An exhaustive diagram match is componentwise strong by its small vertex enumerations and respects the inclusions and mark, so it is a pair arrow. No union-object assertion for \(\mathcal C^b\) was used. ◻

Proof. Present \((A,U,b)\) as \(F^b(H)\) on a well-order of size \(\nu\). Given a questioned bounded tuple from \(C\), include it over \(A\) in a level-\(\nu\) subobject \(V\leq C\). Append a universal strip to \(H\), retaining size \(\nu\), to obtain \(H'\). The base presentation of the pair template is a natural term presentation into the already working scheme \(\mathcal C\). The presentation-invariant universal-strip result embeds \(V\) over \(A\) into \(A_{H'}\). Corollary 48 then embeds \(A_{H'}\) into \(C\) over this copy of \(V\).

The joint bounded diagrams of \(U\) and \(A_{H'}\) inside \(T\) are the diagrams of the natural layout \[ U_H\cup A_{H'} \quad\hbox{inside }U_{H'}. \tag{8}\] Indeed, each bounded tuple of \(U\), together with \(b\), is isolated over \(A\), whereas the marginal of \(b\) over \(A_{H'}\) is the prescribed free extension. Lemma 60 determines its joint type. The argument applies both to (8) and to the specified image inside \(T'\). It includes equalities between the two parts of the layout; an additional actual overlap is not ignored.

For a bounded candidate tuple in either ambient, each bounded test over the layout has a local realization in \(U_{H'}\), by mixed diagram saturation in \(\mathcal C\). Apply Lemma 45 to lift its comparisons to a placed comparison over (8). The layout has two well-ordered horizontal segments with designated term parts. Proposition 44 gives a bound depending on the candidate arity and the fixed template, not on \(H,H'\) or \(V\).

If the two candidates disagree on the questioned test, their placed comparisons disagree and yield a witness within that bound. Its second-part parameters lie in \(A_{H'}\), already embedded into \(C\); its first-part parameters lie in the original \(U\). This is the required small witness. Close \(\nu\) under the testing and placement costs for this fixed layout.

All padded-order repetitions here concern the horizontal top presentation as a functor into \(\mathcal C\). Its extension to padded orders uses chain closure of \(\mathcal C\), not of \(\mathcal C^b\). ◻

Proof. Fix a level \(\mu\) closed under the bounds of Lemma 75, with cofinally many smaller levels at which Lemma 74 and the required underlying results hold. We do not require pair-chain closure at the smaller levels.

Write the chain, replacing arrows by inclusions, as \[(C_i,T_i,b)\quad(i<\alpha),\] and its component unions as \(C,T\). The underlying scheme gives \(C\leq T\) and its union maps. The actual marginal of the finite mark over \(C\) is \(p_C\): the marginals at proper stages are the prescribed free extensions, and Proposition 54 gives stationary continuity for this finite tuple.

Induct on the chain length. The shorter-length assertion allows intermediate limit unions to be inserted. Restricting cofinally, we may consider a continuous chain indexed by a regular cardinal \(\delta\). If a bounded tuple \(d\in T\) is contained in some \(T_i\), its type with \(b\) is isolated over \(C_i\); Lemma 60 gives isolation over \(C\).

Suppose \(d\) is not contained in a proper stage. Its entries occur at cofinally many indices, so \[\delta\leq |d|<\mu.\] Choose an eligible \(\nu<\mu\) strictly above \(|d|+\delta+\aleph_0\), closed under the arity, isolation, approximation, and two-part testing bounds to be used. Small pair objects below will come from Lemma 74 or from explicit descent; pair-chain closure at \(\nu\) is not an induction hypothesis. Choose \[B\geq C \quad\hbox{all-dominated over }C+b', \qquad b'\models p_C .\]

It suffices to find an image \(d'\) in \(B\) with \(\mathop{\mathrm{tp}}(b,d/C)=\mathop{\mathrm{tp}}(b',d'/C)\), because the type on the right is isolated relative to \(b'\). We obtain this image by building small pairs inside the given chain and compatible maps from their upper objects into \(B\). The maps must preserve types over the entire union base \(C\), including for tuples that span a limit of the small pairs.

Specifically, we construct continuous systems of underlying level-\(\nu\) objects \(A_i\leq U_i\) inside \(C_i\leq T_i\), for \(i<\delta\), and compatible arrows \(f_i:U_i\to B\), satisfying:

1. \(b\in U_i\), \(f_i(b)=b'\), and \(f_i\) fixes \(A_i\);

2. \((A_i,U_i,b)\) is a marked pair;

3. for every tuple \(u\) from \(U_i\) of length \(<\nu\), \[ \mathop{\mathrm{tp}}(b,u/C) =\mathop{\mathrm{tp}}(b',f_i(u)/C); \tag{9}\]

4. every entry of \(d\) is eventually included.

Equation (9) is computed in the actual underlying ambients \(T,B\).

Retractions prepared for the limits. For every nonzero limit \(j\leq\delta\), put \(C_\delta=C\), and choose in advance families of \(\nu\) approximate retractions \[ r^j_\xi:T\to C_j,\qquad s^j_\xi:B\to C_j \quad(\xi<\nu). \tag{10}\] They exist in the underlying scheme since \(C_j\leq T,B\); each old parameter of \(C_j\) is fixed outside a finite set of indices in each family. At a limit we require \[ r^j_\xi[U_j]\ \cup\ s^j_\xi[f_j[U_j]]\ \subseteq A_j \quad(\xi<\nu). \tag{11}\]

We describe the scheduling. Once an entry \(x\) and its image \(f_i(x)\) have been chosen at stage \(i<j\), each value in (10) belongs to \(C_j\), hence to some \(C_k\) with \(k<j\) by continuity. Assign its inclusion in the small base to a successor stage \(k'\) with \(i<k'<j\) and \(k\leq k'\). Such a stage exists because \(j\) is a limit. A value is never requested before it is available. New entries and images create at most \(\nu\cdot\nu\cdot|\delta|=\nu\) requests at a stage. The union of the requests assigned to any one stage still has size at most \(\nu\): there are \(<\nu\) stages, each of size \(\nu\). Underlying mixed downward Löwenheim–Skolem can therefore include all of them. This also schedules \(j=\delta\), whose families were chosen in advance.

Small objects at a nonlimit stage. At an initial or successor stage \(i\), include the preceding small base in the new base and the preceding small top in the new top, the requests now due, and the designated entries of \(d\) available in \(T_i\). Choose \(\nu\) approximate retractions \(T_i\to C_i\). Alternate for \(\omega\) steps the following operations: choose a level-\(\nu\) subobject of \(C_i\) containing the current base, all due base entries, and all the chosen retraction images of the current top; then choose a level-\(\nu\) subobject of \(T_i\) containing that base, the current top, and required top entries. Each request has size at most \(\nu\). Underlying coherence gives increasing arrows and the base-to-top arrows. Take underlying unions to obtain \(A_i\leq U_i\).

The marginal of \(b\) over \(A_i\) is \(p_{A_i}\), by restriction of the mixed prescription from \(C_i\). Lemma 58 says that every \(<\nu\) tuple from \(U_i\), jointly with \(b\), has actual type over \(C_i\) freely extended from \(A_i\). Its type over \(C_i\) is isolated relative to \(b\), since the given large pair is all-dominated. The uniform fragment bounds are below \(\nu\). Lemma 64 proves that \((A_i,U_i,b)\) is a small marked pair. Only underlying unions were used in obtaining it.

Extending the map at a nonlimit stage. Let \(U^-,A^-,f^-\) be the preceding small top, base, and map, when present. The old map fixes every element of \(U^-\cap C\), not just \(A^-\): apply (9) with that element as a parameter. Thus fixing \(A_i\) is compatible with the old map on their overlap.

Enumerate \(U_i\) by nested bounded lists in countably many steps, including the mark and whole smaller strong vertex submodels. Place these lists in \(B\), retaining the old map, and require equality on all joint tests of size \(<\nu\) from \(U^-\) and \(C\). For a current source list \(v\), let \(\chi_0<\nu\) be the bound of Lemma 75. With no preceding stage, use whole-base testing instead.

For every old test \(u\) from \(U^-\) of length at most \(\chi_0\), the tuple \((b,u,v)\) lies in \(T_i\). Its type over \(C_i\) is isolated, and its actual mark marginal over \(C\) is free. Lemma 60 gives an isolated type over \(C\). Choose an isolating fragment \[Z_u\subseteq C,\qquad |Z_u|\leq h(|b,u,v|)<\nu .\] Include the empty old test. The union of the fragments has size at most \(\nu^{\chi_0}\cdot h(|b|+\chi_0+|v|)\). This may exceed \(\nu\), but it is less than \(\mu\), since \(\mu\) is strong limit and \(\nu<\mu\).

The placement parameters are \(f^-[U^-]\), the fragments, \(b'\), previous assignments in the current exhaustion, and the required fixed entries of \(A_i\). Their total size is \(<\mu\). Choose a test size \(\chi<\nu\) large enough for \(\chi_0\), the current list, the fragment bounds, all relevant equalities, and the compact-placement costs. Specify joint diagrams on all parameter tests of size at most \(\chi\), using the actual source diagrams.

Every such simultaneous local request is possible in \(B\). A query of size at most \(\chi\) may meet many of the fragments \(Z_u\), but all those entries together form one tuple from \(C\) of size at most \(\chi\). Combine that tuple, its old entries from \(U^-\), fixed base entries, and previous assignments into one parameter list. For the first placement, (9) matches its old entries over \(C\); if there is no old stage, the prescribed mark types give the initial match. At later placement steps, the maintained joint comparisons give the match also with previous assigned entries. The combined list has size \(<\nu\). Underlying saturation in \(B\) realizes the diagram of the new source list over these parameters.

The compact-placement cost depends on the current tuple arity, \(\chi_0\), the uniform fragment bound, and the fixed labels, rather than on the size of the entire union of fragments. For an infinite \(\sigma<\nu\) bounding the current tuple arity, choose \(\chi<\nu\) above these costs with \(\chi^\sigma=\chi\). Each parameter subset of size at most \(\chi\) then has at most \(\chi\) support profiles. The hit-and-separation construction tests only a final parameter set of size at most \(\chi\). Apply Lemma 45 to the coherent local requests in a well-ordered presentation of \(B\). It gives a placement in an order enlargement. The whole parameter set has size \(<\mu\), so underlying saturation realizes its joint diagram with that placement back inside \(B\). In particular the realization agrees on every \(Z_u\) and all previously imposed equalities. Its mark marginal over \(C\) is \(p_C\). Isolation gives the correct whole type over \(C\) for \((b,u,v)\) when \(|u|\leq\chi_0\). Lemma 75 upgrades this to all joint tests of size \(<\nu\). Continue.

The union is an underlying arrow \(f_i:U_i\to B\), by the included strong vertex enumerations. It fixes \(A_i\) and takes \(b\) to \(b'\). A \(<\nu\) tuple of \(U_i\) might span this countable exhaustion. For such a tuple, the completed arrow gives the correct small type over \(A_i\). The small pair is all-dominated, and both actual mark marginals over \(C\) are the prescribed free extensions. Mixed Lemma 60 identifies their types over \(C\). This proves (9) for every \(<\nu\) tuple.

Proper limit stages. For a nonzero limit \(j<\delta\), take underlying unions \[A_j=\bigcup_{i<j}A_i,\qquad U_j=\bigcup_{i<j}U_i,\qquad f_j=\bigcup_{i<j}f_i .\] They are underlying objects and an underlying arrow by the chain and mixed upper-bound clauses of \(\mathcal C\). Their size is \(\nu\), since \(|j|<\nu\). Scheduling gives (11). For every \(<\nu\) tuple of \(U_j\), apply Lemma 58 on each side: its actual type over \(C_j\) is the free extension of its type over the common \(A_j\). These small types agree because \(f_j\) fixes \(A_j\).

The given large pair \((C_j,T_j,b)\) is all-dominated. Downward isolation transfer proves all-domination over \(A_j+b\), without small-pair chain closure. The equality over \(C_j\), isolation there, and prescribed free mark marginals over \(C\) then give equality over \(C\) by Lemma 60. All proper-stage invariants are established.

The final limit. Take underlying unions \(A_\delta,U_\delta,f_\delta\). The families prepared for \(j=\delta\), condition (11), and Lemma 58 give equality of the actual types over \(C\) from their common type over \(A_\delta\). No isolation assertion for the final source pair has been used. In particular, \[\mathop{\mathrm{tp}}(b,d/C) =\mathop{\mathrm{tp}}(b',f_\delta(d)/C),\] since \(|d|<\nu\) and all its entries were included. The right-hand type is isolated by all-domination of \(B\); hence the left-hand type is isolated relative to \(b\). This covers every bounded tuple not already contained in a proper stage, and proves all-domination of \(T\) over \(C+b\).

The union maps are componentwise strong by the underlying scheme. If all stages lie in a common marked pair, the underlying upper-bound clause gives a componentwise strong union map preserving the data and mark. That is precisely a pair arrow. The argument includes a larger eligible common upper bound. ◻

Proof. Lemma 73 gives the isomorphism test, orbit preservation, and mixed reflection. Lemma 74 gives individual template values and their mixed arrows, mixed downward Löwenheim–Skolem, natural bounded diagrams and saturation, and the exhaustive-list arrow criterion. Lemma 76 supplies the missing union-object and upper-bound assertions. Composition and coherence are componentwise.

The extraction added only finitary chart, representation, retraction, and LS-witness symbols with a fixed set bound. Further bounds were testing and placement costs for the old template and the fixed two-part layout of the new template, isolation and approximation costs, and a refinement permitting cofinally many smaller template-valid levels. These are fixed-parameter operations in the closure bookkeeping. No step requires small-pair chain closure before it is proved. ◻

Proof. First consider surjectivity at a level \(\mu\). Present \(X=F(I)\) on a well-order, and let \(p\) be a projected type over \(PX\). For a bounded list \(a\) of parameters from \(PX\), saturation in \(\mathcal D\) realizes the prescribed joint diagram of \((v,a)\) in \(PX\) itself. Such a realization has term representations in the retained sorts of \(F(I)\). Thus every one of the simultaneous local requests used in compact placement has an actual placement in the chart of \(X\).

Here we prescribe projected diagrams only; diagrams involving the forgotten sorts have yet to be chosen. The proof of Lemma 45 applies to this form of request as well. To verify this explicitly, fix a sufficiently large bounded cardinal \(\chi=\chi^{|v|+\aleph_0}\), larger than the label and testing bounds. A profile records the labels of \(v\), its ordered supports, and their comparisons with the chosen representations of the projected parameters under consideration. There are at most \(\chi\) profiles over at most \(\chi\) parameters. If a continuation of a profile fails a prescribed projected diagram, record a witnessing projected test and add it to the next parameter set. The comparison of continuations with no new event uses equality of natural \(\mathcal C\)-diagrams on retained sorts; the hypothesis on \(P\) then gives equality of the requested \(\mathcal D\)-diagrams. Consequently the same new-hit or new-separation argument as in Lemma 45 rules out failure at every step. The local possibility used at the final step is the simultaneous request on the entire final bounded parameter set, which is realizable in \(PX\) by saturation.

The resulting placement in an enlargement of \(I\) satisfies the projected requests up to \(\chi\). Taking \(\chi\) beyond the testing bound in \(\mathcal D\) makes its projected type equal to \(p\). The placement itself defines a \(\mathcal C\)-type over all of \(X\), which proves surjectivity. In particular, no diagram on a forgotten parameter was assumed to have been prescribed in advance.

Next let \(q=\mathop{\mathrm{tp}}_{\mathcal C}(v/X)\). Its approximation lists from Lemma 50 consist of tuples in the same retained sorts as \(v\). A query whose parameters lie in the projection sorts can be moved over such an approximation list using the working package. The projection comparison identifies precisely the equality tests used in this computation. The majority answer and its exception estimate therefore compute the projected free lift. Increasing the approximation length or the test arity gives the same answers by the compatibility part of the approximation construction. Thus free lifts project to free lifts. This reasoning uses bounds below the originating level and consequently applies also to mixed arrows. Projecting the witnessing chain of a free product now gives its claimed projected witnessing chain.

For injectivity, suppose \(q_0\ne q_1\) have the same projection. Choose a bounded tuple \(f\) from \(X\) witnessing their inequality: the diagrams of \((v,f)\) for the two types have distinct values \(\delta_0\) and \(\delta_1\). Choose a bounded infinite \(\chi\) such that \[\chi^{|f|+\aleph_0}=\chi,\] and such that \(\chi\) bounds \(|v|\) and the label and orbit-counting costs. All constructions below fit below \(\mu\): in particular \(2^\chi<\mu\), and a tuple of \(\chi\) many copies of \(v\) remains bounded at \(\mu\).

For each \(\eta\in{}^\chi 2\), construct a genuine witnessed free sequence \((v_i^\eta:i<\chi)\) over \(X\) with successive marginal \(q_{\eta(i)}\). Successor steps use free extension and amalgamation; limit steps use the chain axiom. The uniqueness of whole types of witnessed chains in Lemma 70 applies also to these bounded tuple entries. Their projected marginal types are all the same, so their projected sequences have the same whole type over \(PX\). In particular their parameter-free projected diagrams agree. By the hypothesis on \(P\), their whole \(\mathcal C\)-diagrams agree as well.

Fix one such sequence \(a=(a_i:i<\chi)\) in a level-\(\mu\) object. Bounded diagram homogeneity gives, for every \(\eta\), an isomorphism from the object containing \(v^\eta\) onto this fixed object, carrying \(v_i^\eta\) to \(a_i\) for every \(i\). Write \(f_\eta\) for the image of \(f\). Preservation of diagrams gives \[D_{\mathcal C}(a_i,f_\eta)=\delta_{\eta(i)}.\] If \(\eta\ne\eta'\), a coordinate where they differ shows that \(f_\eta\) and \(f_{\eta'}\) have different orbits over the entries of \(a\). There would be \(2^\chi\) such orbits of \(|f|\)-tuples over at most \(\chi\) parameters. Lemma 42 bounds their number by \(\chi\), a contradiction.

Restriction and transport commute with projection directly. Surjectivity and injectivity, together with the free-lift calculation, give all the stated compatibilities. In particular a projected extension of a type is free exactly when its corresponding full extension is free: the free full extension has the required projection, and injectivity makes it the only possible full lift. ◻

Proof. Identify the given base with its image. Choose nested bounded lists \(d_i\) exhausting \(Z\) for \(i<\omega\). In each vertex include enumerations of increasing smaller strong submodels exhausting that vertex. We construct extensions \(X\to X_i\) and assignments of \(d_i\) into \(PX_i\) that extend the previous assignments and have the correct type over \(PX\).

Suppose the assignment of \(d_i\) is given. Amalgamation in \(\mathcal D\), with identification of the already matching tuple, puts \(Z\) and \(PX_i\) in a common extension, agreeing on \(PX\) and on \(d_i\). The type there of \(d_{i+1}\) over \(PX_i\) lifts by Proposition 78 to a type over \(X_i\). Realize it in a \(\mathcal C\)-extension \(X_{i+1}\). The part corresponding to \(d_i\) is already a tuple of parameters from \(PX_i\), so its equality diagram forces the new assignment to extend the old one. At the first step use the same argument with the empty tuple.

Take the union of the \(X_i\). The assigned lists match all their bounded diagrams, and the included vertex submodel enumerations give componentwise strongness by the working-package map criterion. Thus their union is the required arrow from \(Z\). ◻

Proof. We induct on the number of axes. At depth zero the working package and the prescription \(r\) are the given ones. Suppose the assertion is known for \(\mathcal C_n\). By the exact type correspondence for the root projection, \(r\) determines a unique type over every \(\mathcal C_n\)-object. Projection commutes with free lifting, so this prescription is stationary, including under mixed arrows. Theorem 77 therefore supplies the working scheme \(\mathcal C_{n+1}=(\mathcal C_n)^b\).

First forget its last axis. The result is its lower object \(X\). If two bounded tuples in the lower objects have equal \(\mathcal C_n\)-diagrams, a lower-object isomorphism matches them. It transports the prescribed type of \(b\), and hence extends to an isomorphism of the marked pairs by Lemma 73. This proves diagram reflection; preservation follows by restriction. Objects and arrows plainly project to their lower objects and arrows.

Next apply an earlier projection \(P:\mathcal C_n\to\mathcal C_k\) to both layers of \((X\le Y,b)\). The marginal of \(b\) over \(PX\) is the required type, by Proposition 78. We must verify all-domination of \(PY\) over \(PX+b\). Suppose it fails for a bounded tuple \(a\) from \(PY\). The nonisolation alternative of Proposition 61 gives an extension of \[\mathop{\mathrm{tp}}_{\mathcal C_k}(b,a/PX)\] to an enlarged parameter object \(V\ge PX\) that is nonfree, although its \(b\)-marginal is free. By Corollary 79, put \(V\) inside the projection of an extension \(X'\) of \(X\). Freely extend the chosen joint type to \(PX'\). It remains nonfree from \(PX\), since otherwise its restriction to \(V\) would have been free. Its \(b\)-marginal remains free from \(PX\) by transitivity.

Lift this type to \(X'\) by the exact type correspondence. Its restriction to \(X\) is the original type of \((b,a)\), because their projections agree and the correspondence is injective. Its \(b\)-marginal is the free lift of the original one, again by injectivity and compatibility with free lifting. Its joint type is nonfree: a free joint type would project to a free one. This contradicts the relative isolation of \(\mathop{\mathrm{tp}}_{\mathcal C_n}(b,a/X)\) and Lemma 60. The projected pair is thus all-dominated as required. Componentwise projection of an arrow preserves the prescribed mark and gives an arrow of these pairs.

It remains to reflect pair diagrams. Suppose bounded retained tuples in two projected pairs have equal diagrams. The projected pair isomorphism test gives an isomorphism of their projected bases transporting their types jointly with \(b\); any indicated base entries are included in this match. Choose in the first base sufficiently long approximation lists for this joint type, at arities exceeding the full and projected testing bounds. Their entries are in retained sorts. Carry these lists, together with the indicated base entries, by the projected base isomorphism. The inductive reflection hypothesis and bounded homogeneity give an isomorphism of the full bases making precisely these bounded matches.

The transported approximation lists compute the same projected joint type over the second projected base. Exact type correspondence therefore says that the full base isomorphism transports the entire joint type with \(b\). The full pair isomorphism test now extends it to an isomorphism of marked pairs matching the original tuple. Preservation is immediate from projection of an isomorphism. The same calculation uses free lifting and the mixed preservation and reflection in Lemma 73 when comparing eligible levels; all the tuple and approximation bounds are below the smaller one. Composing elementary axis deletions proves the assertion for every \(P_s\). This completes the finite induction. ◻

Proof of Lemma 82 and Theorem 83. We prove the two assertions together by induction on \(n\). For \(n=0\) the diagram assertion is empty, and joint embedding gives completion. At a positive dimension, after proving the diagram assertion we shall derive completion by a placement argument. Thus only lower-dimensional completion will be used in proving the next diagram assertion.

For \(n=1\), its only proper projection is its base. Theorem 80 identifies the full-scheme diagrams on that base with its projected diagrams. The given base arrow preserves the latter, proving the assertion.

Let \(n=m+1\) with \(m\ge1\), and write the source and target as \[(X^-\le Y^-,b^-),\qquad (X^+\le Y^+,b^+)\] over \(\mathcal C_m\). A boundary map gives a full base arrow \(e:X^-\to X^+\) and a boundary map \(h:\partial Y^-\to\partial Y^+\) agreeing with \(e\) on \(\partial X^-\); the upper faces also specify \(h(b^-)=b^+\). Let \(v\) be a bounded tuple from \(\partial Y^-\), enlarged to include \(b^-\). We first claim that its type over \(X^-\) in \(\mathcal C_m\) equals the restriction along \(e\) of the type of \(h(v)\).

Suppose instead that a bounded tuple \(f\) from \(X^-\) witnesses a difference. Put \[\delta_0=D_{\mathcal C_m}(f,v),\qquad \delta_1=D_{\mathcal C_m}(e(f),h(v)), \qquad \delta_0\ne\delta_1.\] Choose an infinite bounded \(\chi\) satisfying \(\chi^{|f|+\aleph_0}=\chi\), bounding \(|v|\) and all the label and orbit-counting costs. Let \(\epsilon\) be the least cardinal with \(2^\epsilon>\chi\). Cantor’s Theorem gives \(\epsilon\le\chi\), and minimality gives \(2^{|i|}\le\chi\) for every \(i<\epsilon\). Consequently \[\left|{}^{<\epsilon}2\right|\le\chi, \qquad 2^\epsilon\le 2^\chi<\mu,\] where \(\mu\) is the common level. Every accumulator and branch world below will have size \(\mu\), and the total number of amalgamations remains below \(\mu\).

We construct branch worlds \(W_s\in\mathcal C_m\) for \(s\in{}^{\le\epsilon}2\), carrying tuples \(f_s\), with coherent full arrows along each branch. Their proper boundaries have compatible arrows \[q_s:\partial W_s\longrightarrow\partial A\] into an increasing common accumulator \(A\in\mathcal C_m\). The accumulator may be enlarged at each operation; existing boundary arrows are always composed with its enlargement arrow. The invariant requires coherence of these boundary arrows with the branch arrows. It does not require full maps of all the branch worlds into the accumulator to be retained.

Start with \(W_\varnothing=X^-\), its tuple \(f\), and the identity boundary map into \(A=X^-\). At a node \(s\), diagram preservation along the branch shows that \(D(f_s)=D(f)\). Bounded homogeneity supplies an isomorphism \[k_s:X^-\overset{\cong}{\longrightarrow}W_s, \qquad k_s(f)=f_s.\] There is no coherence requirement on the choices of \(k_s\). Choose the minus child to be a copy of \(Y^-\) attached over \(W_s\) by \(k_s^{-1}\), and the plus child to be a copy of \(Y^+\) attached by \(e k_s^{-1}\). These choices give the full branch arrows. In each child, \(f\) denotes the image of \(f_s\); the corresponding upper boundary lists have diagrams \(\delta_0\) and \(\delta_1\) with it. Transporting \(h\) gives a boundary arrow \[h_s:\partial W_{s0}\longrightarrow\partial W_{s1}\] over \(\partial W_s\), matching the two copies of \(v\).

Apply the already proved completion theorem in dimension \(m\) to \(q_s\). After enlarging the accumulator, this gives a full map \(W_s\to A_0\) extending \(q_s\). Ordinary amalgamation in \(\mathcal C_m\) then puts the plus child in an enlargement \(A_1\) over this full map. Let \(G_1:W_{s1}\to A_1\) be the resulting arrow. Retain its boundary restriction as \(q_{s1}\), and define \[q_{s0}=q_{s1}h_s.\] Both restrict to the preceding \(q_s\), after enlargement, and the two boundary copies of \(v\) have one common image \(v_s\) in \(A_1\). The temporary full maps to \(A_0\) and \(A_1\) are no longer part of the invariant. In particular the minus child has not been required to send its copy of \(f\) to the temporary image of \(f_s\) in the accumulator.

Process the nodes of each level successively. At a limit height take the union of the worlds along each branch and the union of the accumulators constructed so far. Their sizes are still \(\mu\). The boundary arrows into the union accumulator exist by the chain and common-upper-bound clauses in every proper projection. Full branch arrows and the carried tuples also pass to the unions. This establishes the invariant through height \(\epsilon\).

At that height, apply lower-dimensional completion to each leaf boundary map, successively enlarging the accumulator. This supplies a full map of each \(W_\eta\), for \(\eta\in{}^\epsilon2\), extending its retained boundary map. There are fewer than \(\mu\) leaves, so the final union is still at level \(\mu\). If two leaves first differ after a node \(s\), their images of \(f\) have diagrams \(\delta_0\) and \(\delta_1\) over the common tuple \(v_s\). Indeed the corresponding copy of \(v\) was in that child’s boundary, remained there along that branch, and its boundary image was never changed except by composition with an accumulator arrow. Thus the final images of \(f\) occupy more than \(\chi\) orbits over the entries of \((v_s:s\in{}^{<\epsilon}2)\). This parameter list has size at most \(\chi\). The orbit bound of Lemma 42 gives the contradiction. The claimed equality of types of \(v\) follows.

To pass from this type equality to the full pair diagrams, retain an arbitrary bounded tuple \(a\) from the lower face \(X^-\). The marginal of \(b^+\) over \(X^+\) is the prescribed free lift from \(e(X^-)\). Relative isolation of the source type of \((b^-,v)\) and Lemma 60 therefore identify the actual type of \((b^+,h(v))\) over \(X^+\) with the free lift of that source type.

Choose sufficiently long bounded approximation lists in \(X^-\) computing the source type. Their images under \(e\) compute its free lift over \(X^+\) by Theorem 51. Base homogeneity gives an isomorphism \(X^-\cong X^+\) matching \(a\) and these lists with their images under \(e\), since \(e\) preserves their joint bounded diagram. The transport assertion for the approximation lists says that this isomorphism carries the whole source type to the type of \((b^+,h(v))\). Lemma 73 now extends it to an isomorphism of the marked pairs matching \((a,v)\) with \((e(a),h(v))\). Every bounded boundary list is of this form. Thus its full \(\mathcal C_n\)-diagram is preserved, including cross-face equalities.

We finish the induction by deriving completion from this diagram equality. Present the source \(J\) on a well-order. Its boundary union is a natural collection of the designated term sorts in that presentation. Choose nested bounded lists \(d_i\) exhausting \(J\), including increasing strong submodel enumerations in every vertex. We construct extensions \(K_i\) of \(K\) and compatible assignments of \(d_i\) into \(K_i\) satisfying \[D_J(d_i,u)=D_{K_i}(d_i',h(u)) \quad\text{for every bounded boundary list }u. \tag{C}\] Here and subsequently \(h\) is composed with the current extension arrow. At the start the assertion for the empty list is exactly the boundary diagram equality just proved.

For the next list prescribe the source joint diagrams on the parameter set consisting of the boundary images and the previous assignment. Each bounded local request, including the whole previous assigned list, is possible by saturation: the parameter diagram agrees by \((\mathrm C)\). This also checks repetitions and equalities between old entries and boundary entries, so the requests define one coherent prescription. Apply compact placement in a well-ordered chart of \(K_i\), keeping these previous entries fixed. Work at one bounded cardinal large enough for the profile count, the new tuple, and the testing bound for the source boundary layout with the previous tuple included. The resulting placement lies in a level-\(\mu\) extension \(K_{i+1}\).

To check \((\mathrm C)\) beyond that initial testing cardinal, pull the candidate diagrams back along \(h\) to the natural boundary layout of \(J\). Their local possibility there follows from the boundary diagram equality and saturation. Lemma 45 compactifies these requests over this source layout, and Proposition 44 says that agreement at the chosen testing bound determines all bounded comparisons. The actual images of the boundary inside \(K_i\) have not been assumed to form a natural layout. All uses of that hypothesis are on the source layout after pullback.

Continue through \(\omega\) steps and take the union of the \(K_i\). The working-package criterion, with the included strong submodel enumerations, makes the union assignment an arrow \(J\to K^*\). Whenever a boundary entry is first included in \(d_i\), its equality test against that boundary entry forces its assigned image to be \(h\) of that entry. The union arrow therefore extends the entire boundary map. The map from \(K\) is the chain inclusion. This proves completion and closes the induction. ◻

Proof. The assertion is immediate for the empty boundary. Suppose it fails otherwise. Choose a bounded infinite \(\chi\) with \(\chi^{|z|+\aleph_0}=\chi\), bounding \(\sigma\) and the orbit-counting and label costs. Let \(\epsilon\) be the least cardinal with \(2^\epsilon>\chi\). Choose a smaller eligible level \(\nu\) such that \[|z|+\sigma+2^\chi<\nu<\mu,\] where \(\mu\) is the level of \(J\), with all required testing bounds below \(\nu\) and with Theorem 83 available at \(\nu\). The further closure requirement on the level of \(J\) ensures this choice. It is a finite refinement for this fixed \(n\).

Fix a well-ordered presentation \(J=F_n(I)\). Construct continuous subpresentations \(J_i\) of size \(\nu\) for \(i\le\epsilon\), beginning with \(z\) in \(J_0\). At step \(i\), the boundary of \(J_i\) is a bounded parameter set in \(J\). By the assumed failure, a boundary automorphism \(\alpha_i\) of \(J\) fixes it pointwise and changes the value of the function at some tuple \(u_i\) of length at most \(\sigma\). Thus \[D_J(z,u_i)\ne D_J(z,\alpha_i(u_i)). \tag{S}\] We choose \(J_{i+1}\) containing both tests so that \(\alpha_i\) restricts to an automorphism of its boundary.

Here is the support closure for this choice. Begin with the positions for \(J_i\), \(z\), \(u_i\), and \(\alpha_i(u_i)\), padding to size \(\nu\). For every element of every proper projected subpresentation currently generated, add positions for its image and its inverse image under the corresponding face map of \(\alpha_i\). There are finitely many faces and \(\nu\) elements in their union, and each representation uses finitely many positions. Repeat this operation countably many times. The resulting position set still has size \(\nu\). Every element generated at its union appeared at a finite stage, so both its image and inverse image are generated in the union. Hence all restricted face maps are onto and remain compatible with the specified inclusions. They give the asserted boundary automorphism of \(J_{i+1}\). At a limit use the union of the position sets. Mixed diagram preservation transfers \((\mathrm S)\) to \(J_{i+1}\), since \(|z|+\sigma<\nu\).

Now build a binary tree of boundary embeddings \[q_s:\partial J_i\longrightarrow\partial A, \qquad s\in{}^i2,\] where \(A\) is an increasing accumulator of size \(\nu\). Start with \(A=J_0\) and the identity map on \(\partial J_0\). At a successor node first apply completion to \(q_s\) on \(J_i\) and then amalgamate \(J_{i+1}\) over that full copy of \(J_i\). This yields an arrow \(G_s:J_{i+1}\to A'\) whose boundary extends \(q_s\). Define the two next boundary embeddings by \[q_{s0}=\partial G_s, \qquad q_{s1}=(\partial G_s)\alpha_i^{-1}.\] They restrict to the same old \(q_s\), because \(\alpha_i\) fixes \(\partial J_i\) pointwise. The common parameter test \(G_s(u_i)\) is the image of \(u_i\) on branch \(s0\) and of \(\alpha_i(u_i)\) on branch \(s1\). Only these boundary embeddings are retained for later steps; the full map \(G_s\) is temporary.

At limits the continuity of the \(J_i\) and the common-upper-bound clauses give the boundary maps into the union accumulator. At height \(\epsilon\), complete the boundary maps to full maps of \(J_\epsilon\), one leaf at a time. The full maps at the leaves carry \(z\). If two leaves first separate at \(s\in{}^i2\), their images of \(z\) have the two distinct diagrams from \((\mathrm S)\) over the one retained test \(G_s(u_i)\). This follows from preservation by their final full maps and from coherence of their boundary maps with the chosen maps at the split.

There are at most \(\chi\) nonterminal nodes, hence at most \(\chi\) parameters in all the splitting tests. There are \(2^\epsilon>\chi\) distinguishable leaf images of \(z\). All leaf completions and all unions remain at level \(\nu\), since \(2^\chi<\nu\). Lemma 42 again contradicts this number of orbits over the tests. Thus the bounded fixing list \(a\) exists. ◻

Proof. We build a back-and-forth sequence of matches \(a\mapsto a'\) of bounded tuples, maintaining \[D_J(a,u)=D_K(a',h(u)) \quad\text{for every bounded boundary tuple }u. \tag{BF}\] For the empty tuple this is Lemma 82. Suppose that a match satisfying \((\mathrm{BF})\) has been chosen, and let \(z\) be any bounded enlargement of \(a\) in \(J\).

Take a bounded infinite \(\sigma\) at least the uniform testing bound for a tuple of length \(|z|\) over the natural boundary layout of a \(\mathcal C_n\)-object. Choose fixing data \(c\) for \(z,\sigma\) in \(\partial J\) by Lemma 84. The maintained equality with the particular boundary list \(c\) gives \[D_J(a,c)=D_K(a',h(c)).\] Working-package homogeneity supplies a full isomorphism \(H:J\cong K\) carrying \(a\) to \(a'\) and \(c\) to \(h(c)\). Put \(\alpha=(\partial H)^{-1}h\). This is a boundary automorphism of \(J\) fixing \(c\) pointwise. Therefore, for every boundary tuple \(u\) of length at most \(\sigma\), \[\begin{split} D_K(H(z),h(u)) &=D_J(z,\alpha(u))\\ &=D_J(z,u). \end{split} \tag{BT}\]

We justify explicitly the passage from these tests to all bounded boundary tests. By Theorem 83, embed \(J\) into a same-level extension \(K^*\) of \(K\) by an arrow \(j\) extending \(h\). Both \(j(z)\) and \(H(z)\) are now tuples in \(K^*\), and \((\mathrm{BT})\) says that their diagrams agree over boundary tests from \(K\) of size at most \(\sigma\). The boundary of \(K\), in a well-ordered chart of \(K\), is a natural collection of term sorts. The types of these two tuples over \(K\) have order placements by the one-dimensional calculus. Proposition 44 restricted to this natural boundary layout therefore gives equality over every bounded boundary test. Preservation by \(j\) then shows \[D_K(H(z),h(u))=D_J(z,u)\] for all bounded \(u\). Thus \(z\mapsto H(z)\) extends the previous match and satisfies \((\mathrm{BF})\).

Apply this extension step alternately to \(J,K\) with \(h\), and to \(K,J\) with \(h^{-1}\). Their level has countable cofinality, so countably many bounded enlargements can exhaust both systems. In each vertex choose increasing smaller strong submodels whose enumerations are included in these tuples. The union assignment is onto in every component and is an arrow by the working-package map criterion; the reverse construction gives its inverse arrow. If an entry lies on the boundary, its equality test with that boundary entry in \((\mathrm{BF})\) forces its image to be exactly the image under \(h\). The resulting isomorphism therefore extends all of \(h\), as required. ◻

Proof. First suppose that a coupling contains a model \(D\) over \(M_0\) and \(S\) but omits \(x\). The type of \(x\) over \(D\) is a nonalgebraic extension of \(p_0\). By Proposition 87 it is the free lift of \(p_0\). Restricting its parameters to \(S\) shows, by Proposition 53, that \(x\) has product type with \(S\) over \(M_0\).

Conversely suppose that \(S,x\) has product type. Use Theorem 67 to obtain a model all-dominated over \(M_0+S\), and amalgamate it with the actual finite configuration, identifying the copy of \(S\). The domination conclusion of Proposition 63 makes \(x\) free over this model from \(M_0\). It is outside the model by Lemma 86. The same amalgamation can retain any further specified finite entries of the original configuration. This is a coupling witnessing that \(S\) does not force \(x\). ◻

Proof. Choose a maximal independent subset \(S\) of a finite \(F\). Every \(y\in F\setminus S\) fails to independently extend \(S\), so Lemma 89 says that every model containing \(S\) in the actual configuration must contain all of \(F\). A point that fails to independently extend \(S\) is therefore forced by \(F\). If \(x\) independently extends \(S\), the avoiding dominated model from Lemma 89 can be adjoined while retaining \(F,x\). It contains \(F\) by the preceding observation and omits \(x\). Thus \(F\) does not force \(x\). This proves the first assertion and its independence of the choice of \(S\).

Define closure on arbitrary subsets by taking the union of closures of finite subsets. Extensivity and monotonicity hold directly from the containment test. To verify idempotence on finite configurations, suppose that finitely many \(y_j\) are in \(\mathop{\mathrm{cl}}_M(F)\) and that \(x\) independently extends a maximal independent \(S\subseteq F\). The avoiding model over \(S\) can be coupled with the whole finite configuration \(F,(y_j),x\). It contains \(F\) and every \(y_j\), because all these points are forced by \(S\), and it omits \(x\). Hence the \(y_j\) cannot force \(x\). Finite character now yields idempotence for all subsets.

For exchange, it suffices by finite character to take finite \(F\) and points \(x,y\) with \[y\in\mathop{\mathrm{cl}}_M(F\cup\{x\})\setminus\mathop{\mathrm{cl}}_M(F).\] If \(x\in\mathop{\mathrm{cl}}_M(F)\), idempotence would imply \(y\in\mathop{\mathrm{cl}}_M(F)\), so \(x\notin\mathop{\mathrm{cl}}_M(F)\). Let \(S\) be a maximal independent subset of \(F\). Then \(S,x\) and \(S,y\) are independent. Since every member of \(F\) is already forced by \(S\), the set \(S\cup\{x\}\) is maximal independent in \(F\cup\{x\}\). The displayed membership says that \(S,x,y\) is dependent. Permutation invariance of products makes \(S,y,x\) dependent as well. Applying the first assertion with \(S\cup\{y\}\) gives \(x\in\mathop{\mathrm{cl}}_M(F\cup\{y\})\). This is exchange.

Preservation and reflection follow from the invariant finite-type definition and the containment test. For relative closedness, take finite \(F\subseteq P(A)\) and \(x\in\mathop{\mathrm{cl}}_M(F)\). Choose \(D\leq_KA\) of size \(\lambda_0\) containing \(M_0\cup F\), and then choose a section of \(M\) containing \(D\cup\{x\}\). Forced containment gives \(x\in D\subseteq A\). The finite closure of \(F\) lies in this same \(D\), proving the finite cardinal bound. There are \(|F|\) finite subsets of an infinite \(F\), so finite character proves the displayed bound.

For completeness, a maximal independent subset of a set can be constructed by well-ordering it and retaining a point precisely when it is outside the span of the points retained earlier. Finite character makes the resulting set independent, and maximality makes it spanning. If an independent set is spanned by a finite set of \(n\) points, it has at most \(n\) points: successively insert its points into a spanning list, using exchange to remove one of the original points whenever a new independent point is inserted. After \(n\) insertions no further independent point is in the span. This also proves equality of finite basis sizes.

For infinite bases \(H,J\) of the same closed set, choose for each \(j\in J\) a finite support \(S_j\subseteq H\). Then \(\mathop{\mathrm{cl}}(J)\subseteq\mathop{\mathrm{cl}}(\bigcup_{j\in J}S_j)\). Independence of \(H\) implies \(H\subseteq\bigcup_{j\in J}S_j\), because a member of \(H\) cannot belong to the span of the other members. Hence \(|H|\leq|J|\); interchanging the bases gives the reverse inequality. The finite argument excludes the possibility of one basis finite and the other infinite. Finally, for a closed \(C\), the operator \(U\mapsto\mathop{\mathrm{cl}}(C\cup U)\setminus C\) on \(P(M)\setminus C\) satisfies the same closure and exchange axioms. Finite character follows by discarding all but the finitely many entries of \(U\) in a dependence witness. Applying the preceding constructions to this operator gives relative bases and their finite supports. ◻

Proof. The enumeration is a bounded tuple at \(\mu\). Bounded-diagram homogeneity in Proposition 23 carries it between any two instances of \(\Delta\) by an isomorphism of the entire models. The pointed version of the working package follows by reserving its supporting positions and including the enumeration in every relevant diagram, as in Proposition 38.

Existence of \(p^B\) is mixed free extension of \(p_0\), and Lemma 86 gives nonalgebraicity. To prove uniqueness, take two nonalgebraic extensions over \(B\). A distinguishing test for singleton types may be chosen with a fixed bound below \(\lambda_0\). For any such parameter set \(Z\subseteq B\), choose \(M_0\leq_KA\leq_KB\) of size \(\lambda_0\) containing \(Z\). Both types restrict to nonalgebraic extensions of \(p_0\) over \(A\) and are equal there by Proposition 87. Their diagrams on \(Z\) are consequently equal. The bounded testing theorem gives equality over \(B\). Uniqueness and transitivity of free extension prove the assertion for pointed arrows.

All distinguished data here already belong to the parameter model. An amalgam over that model fixes them, and an identification of types over that model respects them. Thus adding them as constants does not change this type computation. ◻

Proof. A product can be witnessed by successive free realizations in models containing all preceding entries. Each realization is outside that model by Lemma 86. Its point set is relatively closed, so the realization is outside the geometric span of \(P(B)\) and the earlier entries. This proves one implication.

For the converse let \(x\) be a finite list independent over \(P(B)\). Fix a parameter test \(Z\subseteq B\) large enough to be used in the uniform comparison of the type of \(x\) over \(B\), but with \(|Z|<\lambda_0\). Choose a regular infinite \(\theta<\lambda_0\) with \(|Z|<\theta\). We may and do choose \(\lambda_0\) closed enough that the comparisons and local-character bounds used here fit below it.

Inside \(B\) choose lists \(x_i\), \(i<\theta\), so that every \(D^K(x_i,Z)\) equals \(D^K(x,Z)\) and all the \(x_i\) together are independent over \(M_0\). To make the successor choice, include in the bounded match the entire enumeration of \(M_0\), \(Z\), and all earlier copies. The original \(x\), being independent over \(P(B)\), is independent from those earlier copies. Saturation realizes its joint diagram inside \(B\). Diagram equality is witnessed by an isomorphism, so it preserves every finite independence comparison over \(M_0\). The total parameters at every choice are bounded at the level of \(B\).

Take a strong section \(N\leq_KB\) of size \(\lambda_0\) containing \(M_0\), \(Z\), and all the copies. Their finite sublists have product type over \(M_0\). The independent-list and finite-domination conclusions of Theorem 71 give a continuous witness chain \((A_i:i\leq\theta)\) inside \(N\), starting at \(M_0\), in which \(x_i\) is free over \(A_i\) from \(M_0\) and is included in \(A_{i+1}\). One may keep the chain inside \(N\): at each step primeness embeds the required all-dominated increment into \(N\) over its already placed base and the specified next list. At limits finite domination keeps the next finite list free, and unions remain strong in \(N\).

Since \(\mathop{\mathrm{cf}}(\theta)>|Z|\), local character applies to \(\mathop{\mathrm{tp}}(Z/A_\theta)\). It is free from some \(A_i\). For a later \(j<\theta\), its restriction to \(A_{j+1}\) is free over \(A_j\), so \(Z\) and \(x_j\) have product over \(A_j\). The type of \(x_j\) over \(A_j\) is free from \(M_0\). The base-change identity in Proposition 53 therefore says that \(x_j\) has product with \(Z\) over \(M_0\). In particular \(D^K(x_j,Z)\) is determined by \(p_0\) and \(\mathop{\mathrm{tp}}(Z/M_0)\).

A known product of the \(p^B\) has this same joint diagram with \(Z\): products of free lifts are free lifts of products, and one may restrict the resulting type to \(M_0\) together with \(Z\). Since \(D^K(x,Z)=D^K(x_j,Z)\), the two candidate types over \(B\) agree on every test of the uniform comparison size. Bounded testing makes their full types equal. This proves the converse. ◻

Proof. Fix a sufficiently large uniform testing arity \(\tau\) for singleton types, including the bound needed to apply compact placement to those tests. The approximation construction for Theorem 51 gives a list \(c=(c_i:i<\beta')\) of approximations in \(A\) that computes \(r\) by majority on all these tests. Its length and all ancillary approximation data can be bounded by one cardinal \(\beta\), independently of the level. Choose the length larger than the exception bound for the tests; increase \(\beta\) also to include the fixed point data. The prescription is the value attained by all but the permitted number of entries in \(D^K(c_i,z)\), for each test \(z\) of arity at most \(\tau\).

Freely lift the actual \(r\) to arbitrarily large eligible models containing \(A\). Query matching over the fixed approximation list shows that these lifts compute exactly the same majority prescription. They are nonalgebraic by Lemma 86. For another sufficiently closed pointed \(B\) with the same named diagram, embed \(B\) into such a larger instance, respecting the names. This is possible by bounded-diagram homogeneity and mixed placement. Restrict the lifted type to that copy of \(B\). It is nonalgebraic, since its realization is outside the larger parameter model, and query matching makes its bounded answers the prescribed ones.

Any two types having these answers are equal by the singleton comparison bound. Thus the construction is independent of the larger instance and the chosen embedding. A free lift along an arrow preserving the names has the same prescribed answers: the approximation evaluation is transported by matching each query over the named list inside the old base. Uniqueness therefore identifies it with the prescribed receiving type. At \(A\) the answers are those of \(r\) by the choice of \(c\).

The list lengths have a fixed set bound. Their stabilized diagrams, the fixed testing arity, and the majority rule range over a set of descriptors. Only descriptors realized at arbitrarily high eligible single-model levels are needed; the preceding construction proves that the descriptor extracted from an actual \(r\) has this property. The named diagram itself can be witnessed at one fixed eligible level large enough for arity \(\beta\), by saturation for diagrams from larger levels. Proposition 38 therefore applies with a lower threshold depending on \(\beta\) and the original working scheme, rather than on \(\|A\|\). In particular, extracting the names from a model of size \(\lambda\) does not require moving above \(\lambda\) in order to use the pointed working scheme at that level. ◻

Proof. Take the set of anchored descriptors from Lemma 93. Choose \(\lambda\) at a common level for all finite marked constructions for these descriptors, using Theorem 119. Require also all the relevant single-model and pointed bounds, and \(\lambda>\lambda_0+\beta\). This is a choice uniform in the possible descriptor. In particular the choice does not depend on a pair that might later be assumed to exist.

Suppose toward a contradiction that \(A<_KB\) is such a pair, and choose \(a\in B\setminus A\). Apply Lemma 93 to \(r=\mathop{\mathrm{tp}}(a/A)\) and name its list \(c\). We work in the pointed scheme also naming this list, with its fixed joint diagram. Write \(\mathcal C_n\) for its \(n\)-fold marked iteration with the root prescription \(r\), as in Theorem 80.

Every one-step all-dominated increment of this scheme has no new \(P\)-points. Indeed, pointed categoricity carries its base, including the named list \(c\), onto \(A\). Transporting the witness \(A<_KB\) back gives an extension with a realization of the required \(r\) and unchanged \(P\). Primeness embeds the all-dominated increment into that extension over its base and mark. Since strong maps preserve and reflect \(P\) and fix the base, the increment has exactly the base points.

It follows by induction that the \(P\)-points in the top of every \(\mathcal C_n\) object are precisely those in its root. For the induction step, its lower and upper layers are \(\mathcal C_{n-1}\) objects and hence each has the points of its own root. Projection onto the new axis is a valid one-step marked increment by Theorem 80. The two roots therefore have the same points, proving the assertion for the entire object.

We next construct coherent finite systems. For each \(n<\omega\) choose an object \(J_n\in\mathcal C_n\). For every \(s\subseteq\{1,\dots,n\}\) choose an isomorphism \[e_{n,s}:J_{|s|}\longrightarrow P_sJ_n\] such that these maps commute with all further face projections, using the increasing identifications of finite index sets. Here the full face map is the identity. To make these choices, induct first on \(n\) and then on the size of a proper subset \(s\). For a proper subset \(u\) of the axes of \(J_{|s|}\), let \(t\) be the corresponding subset of \(s\). The boundary map for \(e_{n,s}\) on this face is \(e_{n,t}e_{|s|,u}^{-1}\), with the indicated index identifications. The already chosen maps make these boundary prescriptions compatible. Theorem 85 extends them to the desired isomorphism. At dimension zero it is simply pointed categoricity. This constructs every \(e_{n,s}\) with the asserted commutation.

For the finite subsets \(s\) of any ordinal \(I\), take a tagged copy of the top vertex of \(J_{|s|}\). If \(s\subseteq t\), use the top component of \(e_{|t|,u}\) followed by the inclusion of that face into the top, where \(u\) records the positions of \(s\) in the increasing list of \(t\). The preceding commutation gives a directed system of strong maps. All its roots are copies of the same actual \(J_0\), and no vertex has more \(P\)-points than that root.

The marks corresponding to different indices of \(I\) are distinct in this directed system. It suffices to inspect a two-axis object. Its new mark lies in the root of its upper one-axis layer, whereas the old mark is the nonalgebraic mark of that layer and is outside its root. Face isomorphisms preserve the marks, so the distinction persists under all transition maps.

Take \(I\) of cardinality \(\mu>\lambda\), where \(\mu\) is a sufficiently closed single-model pointed level. The ordinary directed colimit in the AEC exists: a coherent diagram of injective maps is realized as a diagram of inclusions in its direct limit, and the directed-union axioms apply. There are \(\mu\) finite subsets of \(I\), each contributing at most \(\lambda\) elements, and there are \(\mu\) distinct marks. Thus the colimit \(N\) has size exactly \(\mu\). Every element of \(N\) comes from one finite vertex. Preservation and reflection of \(P\) give \[P(N)=P(J_0),\qquad |P(N)|\leq\lambda.\] The enumeration of its distinguished \(M_0\) retains the fixed stabilized diagram \(\Delta\) under the strong colimit embeddings.

On the other hand, there is a pointed model of size \(\mu\) with more than \(\lambda\) points. Start with any pointed model of that size. Successively realize a nonalgebraic free extension of \(p_0\) outside the current model, for \(\lambda^+\) steps. The receiving models and their unions may all be kept of size \(\mu\). The new realizations are distinct and belong to \(P\), so the union has at least \(\lambda^+\) points. Pointed categoricity at \(\mu\) would make this model isomorphic to \(N\) over \(M_0\), a contradiction.

Only the stationary prescription \(r\) was lifted to higher levels. The assumed witness with unchanged \(P\) was used solely at \(\lambda\). The large colimit used the full AEC directed-union axioms, rather than a same-level closure assertion for a marked scheme. ◻

Proof. Suppose that \(a\in B\setminus A\) and \(P(A)=P(B)\). Construct increasing strong submodels \(A_i\leq_KA\) and \(B_i\leq_KB\) of size \(\lambda\), for \(i<\omega\), all containing the distinguished copy of \(M_0\), so that \[A_i\leq_KB_i,\qquad a\in B_i,\qquad P(B_i)\subseteq A_{i+1}.\] For the successor choice, \(P(B_i)\) has size at most \(\lambda\) and is contained in \(A\), so the Löwenheim–Skolem axiom places it, together with \(A_i\), in the next \(A_{i+1}\). Choose \(B_{i+1}\) to contain \(A_{i+1}\cup B_i\cup\{a\}\). Coherence makes all the required inclusions strong. The two unions \(A_\omega\leq_K B_\omega\) have size \(\lambda\). The point diagram restricts correctly to them, and \[P(B_\omega)=\bigcup_{i<\omega}P(B_i) \subseteq A_\omega.\] Thus their point sets are equal, while \(a\in B_\omega\setminus A_\omega\). This contradicts Theorem 94.

Now let \(\|M\|=\kappa>\lambda\). If \(|P(M)|<\kappa\), choose a strong submodel containing \(M_0\cup P(M)\) of size at most \(|P(M)|+\lambda_0\). Enlarge it inside \(M\), if necessary, to a strong submodel of size at least \(\lambda\) and still less than \(\kappa\). It has the same \(P\) as \(M\), contrary to the assertion just proved. Hence \(|P(M)|=\kappa\). If \(H\) is a basis of \(P(M)\), the closure bound gives \[\kappa=|P(M)|=|\mathop{\mathrm{cl}}_M(H)|\leq |H|+\lambda_0.\] Since \(\kappa>\lambda\geq\lambda_0\), it follows that \(|H|=\kappa\). The final assertions were established in Theorem 90 independently of eligibility. ◻

Proof. The union assertion follows by induction on the axes. Unions of old labels are old. If a union involves \(s\cup\{k\}\) with \(s\in Q\), its old part is an active label containing \(s\), and therefore belongs to \(Q\). This also handles the union of two labels containing \(k\). Restriction to a set of axes replaces \(L\) and \(Q\), at every retained step, by their restrictions. The restricted \(Q\) is upward closed in the restricted \(L\). Steps on discarded axes make no contribution. This proves the restriction assertion.

The displayed union is an active label, since the family is finite and contains \(\varnothing\). The collections of active labels below \(t\) and below \(a_L(t)\) agree. Equation (12) therefore gives equality of their \(P\)-sets. The inclusion \(X_{a_L(t)}\leq_KX_t\) and Corollary 95 give equality of the models. ◻

Proof. Fix a witnessing partition \((H_s:s\in L)\), and enumerate \(L\) in an order extending inclusion. For active \(s\), \[D_s(X)=\mathop{\mathrm{cl}}\left(\bigcup_{u\in L,\ u\subsetneq s}H_u\right).\] When the piece at \(s\) is replaced, previously processed labels not below \(s\) are independent, together with the original piece at \(s\), over this lower span: they are parts of a single independent set. Replacing \(H_s\) by any basis of the same flat over its lower span preserves both independence and the span of the union. Explicitly, let \(C\) be the current pieces below \(s\). Then \(\mathop{\mathrm{cl}}(C\cup B_s)=\mathop{\mathrm{cl}}(C\cup H_s)=P(X_s)\), and \(C\cup B_s\) is independent. The remaining current pieces were independent over \(\mathop{\mathrm{cl}}(C\cup H_s)\), since the full current partition was independent. They remain independent over the equal flat \(\mathop{\mathrm{cl}}(C\cup B_s)\). Thus the new full partition is independent and has the same span. Applying this replacement at the finitely many active labels gives the first assertion and Equation (12) for the new partition.

If pieces extend along an embedding, any finite independence calculation in a vertex over its lower span is the same calculation using the corresponding pieces in the larger independent set. Relative independence is therefore preserved.

Conversely, let \((B_s)\) be an arbitrary witnessing partition of the domain, viewed as a subsystem of \(Y\). Preservation implies that \(B_s\) is independent over \(D_s(Y)\). Extend it to a relative basis \(B_s\cup C_s\) of \(P(Y_s)\) over \(D_s(Y)\). The first assertion, applied to \(Y\), says that these choices assemble into a witnessing partition of \(Y\). This proves both the equivalence and the final assertion. ◻

Proof. Composition follows from the relative independence criterion. For coherence, suppose \(X\subseteq Y\), and both embed by arrows in \(Z\). Independence over \(D_t(X)\) implies independence over \(D_t(Z)\), and hence over its subset \(D_t(Y)\). Componentwise coherence is the AEC coherence axiom.

For a continuous chain, extend witnessing pieces successively using Lemma 99, and take their unions at limit stages. Every finite independent sublist and every finite dependence witness occurs at a stage. The resulting union pieces are independent and span every vertex of the componentwise union. Each contains \(\mu\) elements from the first stage and has size at most \(\mu\), so all pieces still have size \(\mu\). For a chain which is not initially continuous, insert its earlier unions: the preceding construction applies recursively, and the common-upper-bound argument in the next paragraph supplies its connecting arrows.

If each stage maps by an arrow into \(Z\), a finite tuple independent over the lower span of the union is independent over the lower span at any stage containing it. Its image is independent over \(D_t(Z)\). The componentwise AEC common-upper-bound axiom supplies the strong maps, so the union map is an arrow. This argument also permits a larger level for \(Z\).

On restricting to axes \(B\subseteq A\), retain the pieces whose labels are contained in \(B\). They are a basis of \(P(X_B)\) and satisfy the required span identities. For a retained vertex all its proper subsets are still retained; its relative independence test is therefore exactly the old test.

Finally let \(Z\) have shape \(L'\), and put \(X_s=Z_s\) and \(Y_s=Z_{s\cup\{k\}}\). A partition for \(Y\) is obtained by combining \(H_s\) with \(H_{s\cup\{k\}}\) when \(s\in Q\), and using \(H_s\) alone otherwise. These choices extend the pieces of \(X\), and their complements have the asserted sizes. Conversely, extend pieces of \(X\) to pieces of \(Y\) along such an arrow, give the old pieces labels \(s\) and their complements labels \(s\cup\{k\}\), and use \(X\) and \(Y\) as the two layers. The span identities give a system of shape \(L'\). Inactive vertices cause no exception, by Lemma 97. ◻

Proof. Let \(I_s\) be the indicated suborder and set \(X_s=E(I_s)\), using the literal embeddings supplied by Theorem 9. All \(I_s\) have size \(\mu\), since they contain all buffers. The models have size \(\mu\) and are strongly included according to their labels. The initial order was chosen to contain the supports of the fixed enumeration of \(M_0\). Its unchanged term pattern carries the same pointed model in every vertex, and coherence gives the required strong inclusion of \(M_0\).

Choose a relative basis \(H_s\) of \(P(X_s)\) over the union of its proper lower \(P\)-sets for every active \(s\). We first prove that the indexed family of these choices is independent; this also proves that the pieces are disjoint. Suppose there is a finite circuit of labeled entries, allowing a two-entry equality dependence when two differently labeled entries coincide. Choose a maximal label \(s\) represented among its entries. Retain the finite term supports of all entries with label \(s\), and indeed retain every support position in a tile available at \(s\). In each unavailable tile replace all support positions by distinct positions in its preceding buffer, beyond all the finitely many retained positions in that buffer. Such positions exist because the buffer has no greatest point and is dense. No retained position lies in that unavailable tile. Consequently this replacement preserves the order and equality pattern of all circuit supports and fixes the whole initial pointed order.

The labels and this order pattern preserve the pointed finite geometry comparisons. One can formulate this either using the natural \(K\)-diagrams or by taking the term model on the fixed initial order and the finite supports and applying its two pointed strong embeddings into the original presentation. In the latter formulation Theorem 90 preserves and reflects the independence relation.

An entry with label \(t\ne s\) in the circuit has no label properly containing \(s\), by maximality. Thus \(s\nsubseteq t\). After the replacement its term uses only common buffers, initial data, and tiles with labels contained in \(s\cap t\). Its image belongs to \(P(X_{s\cap t})\subseteq D_s(X)\). The entries with label \(s\) have not moved. The preserved circuit makes a sublist of \(H_s\) dependent over \(D_s(X)\), a contradiction. The union is therefore independent. It spans every vertex by induction on the labels: its relative basis spans that vertex over lower vertices, which have already been spanned. If a vertex is inactive, the order retained there is exactly the order retained at its largest active subset. This proves the decomposition without first assuming the system axioms.

We give the fresh-skeleton observation needed for the rank assertion. If \(J\subseteq I\) and \(i\in I\setminus J\), the skeleton entry at \(i\) does not belong to \(E(J)\). Otherwise it equals a labeled term on a finite tuple of positions from \(J\). Enlarge the order by a second position \(i'\) having the same order pattern as \(i\) relative to that finite tuple. Literal pattern preservation would make both distinguished skeleton entries equal to that term. This contradicts their required distinctness. The enlargement need only duplicate the cut relative to the finite tuple, not the cut relative to all of \(J\).

For an active \(t\), omit \(T_t\) from \(I_t\). The resulting order still has size \(\mu\), contains the pointed data and all proper lower vertices, and presents a strong submodel. Enumerate \(\mu\) points of \(T_t\) and adjoin them one at a time. The fresh-skeleton observation makes each successor inclusion proper. All these models have size \(\mu\), because the buffers were retained. By Corollary 95, each successor adds a point of \(P\). Choose one such point at each successor. Relative closedness of \(P\) in strong submodels makes these choices independent over the initial omitted-tile model. There are \(\mu\) choices, so the rank over the proper lower vertices is at least \(\mu\). It is at most \(\mu\) by the size of \(X_t\). This proves the first assertion, including the root case \(t=\varnothing\).

Next consider componentwise order embeddings into enlarged tiles and buffers, identifying the source with its image. Suppose a finite tuple \(a\) in \(P(X_s)\), independent over \(D_s(X)\), becomes dependent over \(D_s(Y)\). Dependence has a finite witness consisting of points from proper lower vertices of \(Y\). Fix the finitely many old positions supporting \(a\). Move every other position needed for the witness into its corresponding old tile or buffer, preserving its order relative to the fixed positions. Density and absence of endpoints of the old order suffice for each finite pattern; it is not necessary that the old order be dense in the enlarged order. The initial pointed order remains fixed. Each witness remains in its designated proper lower vertex, now in \(X\), and its finite dependence diagram is preserved. This contradicts independence of \(a\) over \(D_s(X)\). Lemma 99 therefore gives an arrow. The proof did not require equal source and target sizes.

To obtain simultaneous gains, enlarge all tiles with \(\mu\) fresh points and, if desired, enlarge the buffers. For a particular active \(t\), begin the strict-growth argument over the order containing the old \(t\)-tile, all enlarged proper-lower tiles, all enlarged buffers, and the initial data. This base contains \(X_t\) and all proper lower vertices of \(Y\). Adjoining the fresh points of the \(t\)-tile yields \(\mu\) independent points over that larger base. Hence the complementary rank at \(t\) is \(\mu\). The preceding arrow assertion allows any old pieces to extend, and Lemma 99 combines the relative choices into one partition. This proves the simultaneous assertion.

Finally a lexicographic sum, indexed by a linear order of size \(\mu\), of dense endpoint-free orders of size \(\mu\) is still dense and endpoint-free and has size \(\mu\). Its summands are the desired convex substrips. In particular, for a presentation indexed by a well-order \(H\), one can use \(H\times\mathbb Q\) and reserve intervals of \(H\) of order type and cardinality \(\mu\). Taking \(H\) of order type \(\mu\cdot\mu\) supplies \(\mu\) disjoint such intervals. Additional summands or strips do not change any of the preceding arguments. Underlying \(K\)-diagrams remain natural because the entire system was obtained by designated term subcollections of the single template \(E\). ◻

Proof. The structural conditions are Lemma 100. Proposition 101 supplies term presentations and mixed presentation arrows before categoricity. By the assumed categoricity, every object at an input level is isomorphic to its presentation.

We check the extra relative-basis condition throughout the reversal argument. In each tile and buffer use the order \(H(\delta)\) from Theorem 14. For a tuple of length \(\theta\), record its term labels, the fixed initial positions it uses, and, separately in each of the finitely many variable orders, the order and realized-cut record of its support positions. If \(\theta<\mathop{\mathrm{cf}}(\delta)\), equal records are carried to one another by order automorphisms of the respective tiles and buffers. Their product fixes the initial data and induces an automorphism of the whole system. The set of possible records has a bound depending only on \(\theta\), the finite shape, and the template. Hence the system orbits at that arity have a uniform set bound.

Number these orbits and record the arrows between them, together with the partial map from support records to orbit names. This is again a bounded palette. If reversal fails unboundedly often, choose repeated profiles at eligible levels \(a<\mu\) exactly as in Theorem 20, with \(a^\theta\leq\mu\) and the required large cofinalities for the orders. Apply the ordinal-position shrinking of Proposition 18 simultaneously to the finitely many tiles and buffers. Given at most \(a\) parameters in the large system, the resulting small presentation contains them, has size \(a\) in every tile and buffer, and computes the support records of all its \(\theta\)-tuples correctly. Its inclusion is an actual arrow by Proposition 101. Thus it is an aligned small geometric system, not merely a componentwise subsystem.

For completeness, the contradiction uses two orbit names \(p,r\) with \(p\to r\) and \(r\not\to p\). Repeatedly choose aligned small copies, each containing the previous one, and process their at most \(a^\theta\) tuples in the large level. Whenever a tuple can still be sent to \(p\), send it onward to \(r\). From that point it cannot reach \(p\). Coherence makes the successive small copies a chain of arrows. After \(\theta^+\) rounds every \(\theta\)-tuple of their union occurred at a proper round. Both unions exist by Lemma 100: the small union has total size \(a\), and the large construction has total size \(\mu\). Alignment says that none of the tuples of the small union can reach \(p\). Categoricity of that union at \(a\) says that its orbit \(p\) is realized, a contradiction. This proves eventual reversal at each fixed arity.

Mixed Löwenheim–Skolem closure also has the required form. In a presentation, close the supports of a prescribed small set under finitely many intermediate and exterior positions in every tile and buffer, repeat countably many times, and pad each order to the chosen smaller eligible size. The resulting dense endpoint-free suborders give a small presentation containing the set. The initial pointed order is retained in full. Its inclusion is an arrow by Proposition 101. Transport through a presentation of an arbitrary large object gives mixed containment; coherence supplies comparisons between such subobjects.

We now apply the first route of Proposition 39. Its structural hypothesis is Lemma 100; its presentation and mixed downward-closure hypotheses are Proposition 101 and the preceding paragraph. Categoricity is the input assumption, and the required arity-by-arity reversal and uniform orbit bounds were proved above. Thus the proposition applies to the actual system arrows, including their relative-basis condition.

In particular, the canonical comparison at a smaller input level is computed in a small geometric subobject. Two such sections are contained in a common small section by mixed downward closure, and coherence gives its arrows, so the comparison is well defined. The projections between comparisons at two input levels are onto because the smaller system is a tiled presentation and extends by the mixed order arrows of Proposition 101. The bounded palette therefore stabilizes, exactly as in the first route of Proposition 39.

Choose receiving levels which remain eligible, are strictly closed under the resulting arity bounds, and have sufficiently large smaller input levels below them for every bounded request. These are the closure refinements described in Section 5.2, supplied simultaneously in Theorem 119; closure under the next input level is not being used to infer eligibility by itself. At such a level, countable alternating matching in smaller input-level sections gives actual system isomorphisms on equal bounded diagrams, and realizes possible bounded joint diagrams over their given subtuples. Thus diagrams, homogeneity, and saturation have the system interpretation required here, rather than merely their componentwise \(K\) interpretation. Order embeddings and order amalgamation make the diagrams natural on term tuples, so Proposition 40 also applies.

It remains to check the additional exhaustion condition, which Proposition 39 explicitly leaves as a separate obligation. A finite tuple independent modulo the proper lower vertices stays so when its target diagram agrees with a tuple placed along an actual presentation arrow: the comparison is realized by a system isomorphism, and such an isomorphism preserves relative independence. Every tuple in an exhaustive sequence is handled at a stage containing it. The finite relative-independence criterion in Lemma 99 then supplies the additional arrow condition. Componentwise strongness is the conclusion of the same proposition’s exhaustion argument. This completes the working-package verification.

All refinements used here are the bounds for the original reversal, alignment, diagram stabilization, and saturation arguments, applied to finitely many orders and the fixed initial data. None introduces an amalgamation assumption on the original AEC; the amalgamation used below is the conclusion of the working package and Theorem 47. ◻

Proof. We prove the two assertions in order, by the number of axes. On no axes, the first assertion is exactly the assertion that a prescribed isomorphism of the root models is an isomorphism of the systems. Existence of such a root isomorphism, hence categoricity of the zero-axis scheme, is Proposition 91.

Suppose the second assertion is known for all shapes on fewer axes. For a shape with last-axis description \(L'\), apply the first assertion for \(L\) to its lower layers and then the second assertion for \(L\) to its upper layers. The pieces added at labels in \(Q\) are exactly the pieces bearing labels \(s\cup\{k\}\) in \(L'\). Prescribe their given bijections, and prescribe the empty maps at the other labels. This produces the desired isomorphism of the two-layer systems by Lemma 100. If an auxiliary root basis has been chosen, replace the target root basis by its image under the prescribed root isomorphism; Lemma 99 permits that replacement without changing any prescribed nonroot piece. Thus the first assertion at the next number of axes follows from the preceding second assertion.

It remains to prove the second assertion for a fixed shape \(L\) whose first assertion has now been established. Refine the levels using Proposition 102. All the one-dimensional calculus and dominated-hull results are then available for \(\mathcal G_L\). The rest of the proof is given in four claims.

For each active \(s\), let \(p_s^X\) denote the unique fresh singleton type given by the claim. Such types exist by the rich extensions of Proposition 101 and categoricity. Their realizations lie outside the base vertex, so they are nonalgebraic.

We now know the types of fresh coordinate lists and have all-dominated hulls over them. To extend a partially prescribed basis map, we also need to cover an arbitrary bounded tuple using only boundedly many new coordinates. The next claim provides this size control, including when the target basis has already been chosen.

We finish the second assertion of the theorem. Identify the two bases with \(X\), and keep the prescribed bijections of all complementary pieces. Choose countable exhaustions of the two targets by bounded lists; these exist because the eligible level \(\mu\) has cofinality \(\omega\) and there are only finitely many vertex sorts. Construct alternating isomorphisms between subextensions of the two targets. Initially use \(\mathop{\mathrm{id}}_X\). Maintain the invariant that the complementary pieces in each current subextension are subsets of the specified target pieces, and that the current isomorphism agrees with their prescribed bijections.

At a forth step, apply Claim 107 over the current subextension on the first side to include the next bounded list and to use only remaining specified coordinates. Its new complementary list is bounded. The corresponding coordinates on the second side are jointly fresh over its current subextension. Claim 108, transported by the current isomorphism, embeds the enlarged subextension into the second target over that isomorphism and realizes their prescribed matching. Its image is the next subextension there. The span identities show that its complementary pieces are exactly the specified images of the new pieces, so the invariant is preserved. A back step applies the same construction with the roles interchanged.

The union of these countably many coherent isomorphisms covers both targets, since every list in both exhaustions is eventually included. It is therefore a system isomorphism over \(X\). It realizes all prescribed basis bijections: every basis element is eventually in the domain, and the invariant determines its image. This proves the second assertion, with no lower bound on complementary cardinalities.

The induction is complete. At each fixed finite number of axes there are only finitely many active-label families. Taking the maximum of their finitely many bounds gives the stated uniformity. Simultaneous closure through all finite numbers of axes is addressed separately in Theorem 119. ◻

Proof. We specify the set recursion and the formulas used in it. The small-model code for \(K\) defines membership and strong substructure by the directed union formulas in 6. These are fixed formulas with a set parameter. They are therefore available in all the following set constructions.

Proof. Presentation arrows across levels are supplied by the construction of the templates: the vertex term-hull LS witnesses give componentwise strongness in the marked application, and the tile specialization of 101 gives the additional basis condition in the geometric application. Coherence is componentwise coherence, with the finite independence test for geometric arrows. Once a componentwise union is an object, its arrows and its common-upper-bound property, including into a larger object, follow from the AEC chain axioms and, for geometry, finite character of independence.

Suppose an object \(X\) at \(\nu\in S\) maps to an object \(Y\) at a larger \(\mu\in S\). Present \(Y\) on a well-order. The image of \(X\) uses at most \(\nu\) positions: each of its \(\nu\) entries has finite term support, and there are finitely many vertices. Include these positions in a well-ordered subpresentation of cardinality \(\nu\), also including the fixed named positions. Coherence gives an arrow from \(X\) to this subpresentation. This is mixed LS.

For a tuple bounded at \(\nu\), the latter arrow preserves its orbit by the same-level adequacy condition. The chart clause identifies that orbit with \(D_F\). Inclusion of the subpresentation in the large chart leaves the labeled support pattern unchanged, so the same \(D_F\) test computes the diagram in \(Y\). This proves preservation along arbitrary mixed arrows. A bounded well-ordered pattern from a larger chart can also be placed in an order of size \(\nu\). When its old tuple has the same diagram as a specified tuple in a \(\nu\)-object, the same-level chart clause gives an isomorphism matching those tuples. Transporting the enlargement through that isomorphism proves the required mixed-level bounded saturation.

Root prescriptions pass along mixed arrows because the approximation lists give the same majority comparisons there. To compare the full system types after projection, apply the type correspondence at the receiving level to those equal root marginals. Finally, the criterion for maps obtained by exhausting bounded tuples is componentwise the strong-submodel criterion of the working package. In the geometric case its additional condition is a finite independence comparison, preserved by the matched system diagrams. These arguments verify the mixed clauses without inserting them as new proper-class parameters in the unary adequacy formula. ◻

Proof. Here is the register; its descriptions specify first-order tests, rather than codes for formulas of increasing depth.

Proof. Given any starting ordinal, choose strictly increasing infinite cardinals \((\kappa_n)_{n<\omega}\) above it with \[\kappa_{n+1}> \max\bigl(2^{\kappa_n}, \sup\{\Phi(\alpha):\alpha<\kappa_n\}\bigr).\] The supremum \(\kappa\) of this sequence is a cardinal of cofinality \(\omega\). For every cardinal \(\lambda<\kappa\), some \(\kappa_n\) exceeds \(\lambda\), and then \(2^\lambda\le2^{\kappa_n}<\kappa\). For every \(\alpha<\kappa\), the same choice gives \(\Phi(\alpha)<\kappa_{n+1}<\kappa\). Thus \(\kappa\in G_0\). If instead the \(\kappa_n\) are an increasing sequence in \(G_0\), their supremum is again a countable-cofinality strong limit cardinal and is strictly \(\Phi\)-closed by these same two tests. This proves the two assertions for \(G_0\).

Suppose they hold for \(G_j\). Above any starting ordinal choose a strictly increasing countable sequence in \(G_j\). Its supremum belongs to \(G_j\) by closure and to \(\mathop{\mathrm{Lim}}(G_j)\) because the sequence is cofinal there. This proves unboundedness of \(G_{j+1}\). A countable increasing sequence in \(G_{j+1}\) has its supremum in \(G_j\), and its own members witness that this supremum belongs to \(\mathop{\mathrm{Lim}}(G_j)\). Hence \(G_{j+1}\) has the asserted closure as well.

Choose \(\lambda_n\in G_n\), strictly increasing and above an arbitrary prescribed ordinal. For each fixed \(j\), its tail lies in \(G_j\) because the classes are nested. The supremum belongs to \(G_j\) by its countable closure. It consequently belongs to \(G_\omega\), proving unboundedness.

For absorption, maintain that the current eligible class contains a particular \(G_k\). A request value on inputs below a member \(\mu\in G_k\) is less than \(\Phi(\alpha)\) for a suitable \(\alpha<\mu\), and hence less than \(\mu\). Thus a bound-closure refinement retains all of \(G_k\). A constant threshold is included as a request with input \(0\) and has the same property. If the next refinement demands cofinally many members of the current class below the new level, retain \(G_{k+1}\): its members are limit points of \(G_k\) and thus of the current class. If several earlier eligible classes are mentioned, the maintained index can first be increased to the maximum of their finitely many indices. Induction through the finite refinement list proves the claim, with \(m\) bounded by its number of limit-point refinements. ◻

Proof. Use the fixed register and \(\Phi\) just constructed. The initial single-model results hold on \(G_0\) after the initial requirements have been included. Suppose the assertions required as input to a finite induction step hold throughout \(G_j\). Take \(S\) to be the class defined by their unary adequacy formula, with the current descriptor. It contains \(G_j\). Lemma 116 supplies the mixed conditions for that step. Lemma 117 identifies its bound requests and gives the existence of each relevant witness at its place in the proof. Lemma 118 then retains some \(G_{j'}\), with \(j'<\omega\), through all its refinements.

When a marked step extracts a new template, its code lies in the fixed descriptor set by Proposition 115. The remaining requests with that code as parameter were already majorized by \(\Phi\). Thus making the choice introduces no new closure function or cutoff. For a given finite shape, the finitely many previously required lower shapes can first be brought to one \(G_j\) by taking the largest of their indices. The same observation applies to the finite projection lists in the marked argument. The two ordinary finite inductions therefore give, for each finite descriptor, all its required conclusions on \(G_j\) for some finite \(j\).

In the marked application only root codes consistent at arbitrarily large eligible single-model levels are used. A code obtained from an actual pair at a sufficiently closed starting cardinal has that property: freely lift its type with the named approximation data to arbitrarily large single-model levels. The majority rule is preserved there, and restriction from such a level gives the same stationary prescription at every sufficiently closed smaller single-model level with that named pattern. This is the prescription argument in Lemma [geom:root-prescription], prior to the use of the finite marked systems. It requires no persistence of a no-growth statement about \(P\) at larger levels. The fixed code set and majorant include every such possible input code, so the common-level construction can precede the choice of the actual pair.

Every member of \(G_\omega\) belongs to \(G_j\) for every finite \(j\). It consequently satisfies the conclusion for every finite descriptor used in the application, although the index \(j\) and the selected template may depend on that descriptor. Lemma 118 makes \(G_\omega\) unbounded, so choose a member above the desired thresholds. All constructions in this argument are ordinary set recursions, Separation, Replacement, and finite induction with uniform formulas. This completes the simultaneous closure justification in ZFC. ◻