Proof. Each \(=^*\)-class is countable: its members are obtained by changing the values of one sequence on finitely many integers. If \(\kappa=|S|\), choice therefore gives \[2^{\aleph_0}\le\kappa\cdot\aleph_0.\] The quotient cannot be countable, since then \(2^\omega\) would be countable. Infinite cardinal multiplication and the reverse inequality \(\kappa\le2^{\aleph_0}\) now give \(|S|=2^{\aleph_0}\).

For each \(k\), there are at most \(2^{\aleph_0}\) choices for each of \(E\) and \(R\). By CH, \[\delta^{\aleph_0} =(2^{\aleph_0})^{\aleph_0} =2^{\aleph_0},\] so there are at most continuum many choices for \(\rho\) as well. It follows that \[\left|\coprod_{k\ge1}\mathfrak D_k\right| \le\aleph_0\cdot2^{\aleph_0}=|S|.\] An injection from this disjoint union into \(S\) gives the stated maps. ◻

Proof. Write \(\mathcal D_J=(E_J,R_J,\rho_J)\). The equality \(\mathcal D_J=\mathcal D_{[k]}\restriction J\) gives, for labels \(a,b\in\mathcal L_{|J|}\), \[aE_Jb\ \Longleftrightarrow\ \ell_J(a)E_{[k]}\ell_J(b).\] The forward implication makes the quotient map well-defined, and the reverse implication makes it injective. The analogous equivalence for \(R\) proves preservation and reflection of the quotient relation; equality of the restricted tag functions proves preservation of tags. The maps on labels compose by their definition, so the induced quotient maps do also. ◻

Proof. Fix \(p\in B\). If the final segment above \(p\) has a countable cofinal subset, its cardinality is countable: it is covered by countably many bounded intervals with one endpoint \(p\), together with their endpoints. Otherwise one can recursively choose a strictly increasing sequence \((b_\alpha:\alpha<\omega_1)\) above \(p\). At each stage there are only countably many earlier choices, so the assumption that no countable set is cofinal provides a point above all of them. This sequence must be cofinal above \(p\). A point above the whole sequence would enclose uncountably many \(b_\alpha\)’s in a bounded interval, contrary to local countability. The final segment is therefore covered by at most \(\aleph_1\) countable bounded intervals and their endpoints. It has size at most \(\aleph_1\). The same argument in the reversed order applies below \(p\), proving the claim. ◻

Proof. The right-hand side is a lower bound, since \(I,B,G_*\) are sorts and \(G_*\) is countably infinite. For the upper bound put \(\kappa=\max(|I|,|B|,\aleph_0)\). There are at most \(\kappa\) finite injective tuples over \(I\). The order \(B\) is infinite, so \(|G(B)|=|B|\); hence every row fiber has size \(|B|\), and every column fiber has size \(|G_*|=\aleph_0\). There are at most \(\kappa\) row fibers, indexed by \(\mathcal T(I)\times\omega\), and at most \(\kappa\) column fibers, indexed by \(\mathcal T(I)\times B\). All the carriers together consequently have size at most \(\kappa\). ◻

Proof. Two column representatives differ by a translator \(v\in G_*\). Equation (5) changes their binary sequences only at the finitely many indices in \(v\), so their classes modulo \(=^*\) agree.

For a fixed tuple \(t\), write \(z'_{t,n}=z_{t,n}+u_{t,n}\), with \(u_{t,n}\in G(B)\). Put \[D_t=\bigcup_{n<\omega}\mathop{\mathrm{supp}}(u_{t,n}).\] Each support is finite, so \(D_t\) is countable. At every \(b\notin D_t\), all coordinates of the two bit sequences are identical when computed with the same column representative. The full test for a tuple of length \(k\) involves just its \(2^k-1\) nonempty subsequences. Outside the union of their sets \(D_{t\restriction J}\), all its input colors agree, proving the test assertion.

In the last assertion, the translators between two old representatives belong to \(G(B)^{M_0}\). Their supports in \(M_1\) are still subsets of \(B^{M_0}\), by basic inclusion. At any \(b\) outside \(B^{M_0}\), Equation (5) therefore leaves every individual bit unchanged. This proves the stronger assertion. ◻

Proof. Replace \(I\) and \(B\) by disjoint copies and transport the array indices along these identifications. Use separate disjoint copies for the two group sorts as well. Take tagged, disjoint copies of the appropriate groups for all the fibers. Denote the row points by \((t,n,u)\) for \(u\in[B]^{<\omega}\), and the column points by \((t,b,v)\) for \(v\in[\omega]^{<\omega}\); the tags distinguish the carrier types. Use the regular translation actions and put \[ e((t,n,u),(t,b,v)) = a_{t,b}(n)+\boldsymbol 1_{b\in u} +\boldsymbol 1_{n\in v}\pmod2. \tag{9}\] Set bits between different tuples to zero, and equip the carriers with exactly the specified projections and other relations. Translation by symmetric difference gives (5). The zero row representatives and a zero column representative give the sequence \(a_{t,b}\), as required. Finally, when \(B\) is countable, each set \(E_t(\mathbf z)\subseteq B\) is countable automatically. ◻

Proof. All the basic conditions are preserved by a \(\tau\)-isomorphism, so the isomorphic image of a basic structure is basic. Now consider an isomorphism of basic structures. It preserves the carrier predicates, every row number \(n\), all tuple-coordinate projections, the fixed labels of \(G_*\), the order, supports, actions, and bits. Transporting a row-choice system along it thus preserves the color at each corresponding base point. Countable bad sets are transported to countable bad sets. This proves invariance of the object condition. Convexity, fixed \(G_*\), and equality of old supports are likewise preserved under an isomorphism of a pair of structures. Applying the same color calculation at each new base point proves invariance of the strong relation. In particular, if \(f:N\cong N'\) and \(M\le_K N\), then \(f[M]\le_K N'\).

Reflexivity follows because equality is a basic inclusion and the additional condition has an empty set of new base points. Antisymmetry follows from induced substructure inclusion. To prove transitivity, suppose \(M_0\le_K M_1\le_K M_2\). Basic inclusions compose. Fix a tuple \(t\) from \(I^{M_0}\), a point \(b\in B^{M_2}\setminus B^{M_0}\), and row representatives in \(M_0\) for \(t\) and its nonempty subsequences. If \(b\in B^{M_1}\setminus B^{M_0}\), choose its column representatives in \(M_1\). The bits against these old rows are unchanged in \(M_2\), by induced substructure, and the tests hold by \(M_0\le_K M_1\). If \(b\notin B^{M_1}\), the selected rows in \(M_0\) are also allowable old representatives for \(M_1\le_K M_2\); this latter inclusion supplies the tests. Hence \(M_0\le_K M_2\).

For coherence, suppose that \(M_0\) is an induced \(\tau\)-substructure of \(M_1\), and that both are strong substructures of \(M_2\). Their \(G_*\) sorts both equal that of \(M_2\). Convexity of \(B^{M_0}\) in \(B^{M_2}\) implies its convexity in \(B^{M_1}\). For \(u\in G(B)^{M_0}\), its support in \(M_2\) is exactly its support in \(M_0\); restricting incidence to \(M_1\) gives the same support there. Thus \(M_0\preccurlyeq_{\mathrm b}M_1\). For a tuple from \(I^{M_0}\) and \(b\in B^{M_1}\setminus B^{M_0}\), compute colors using rows in \(M_0\) and columns in \(M_1\). They are the same colors computed in \(M_2\), where \(M_0\le_K M_2\) makes the full test pass. Therefore \(M_0\le_K M_1\). ◻

Proof. Every finite collection of family members has a common upper member, by induction from directedness. In particular, relations agree on overlapping domains: two members embed as induced substructures of a common member. Their union therefore gives a well-defined relational structure \(U\).

The basic data in the union. The carrier predicates still partition the union domain, and every finite tuple in \(I^U\) lies in one member. That member supplies a nonempty row fiber for the tuple at every \(n<\omega\). A tuple together with a base point \(b\) is also contained in a common member, which supplies the required column fiber. Projection graphs remain single-valued and total by the same finite-parameter argument.

The sorts \(G_*^{M_i}\) are all the same set: for any two indices, a common upper member has \(G_*\) equal to both. Their labels and group structures agree. Every \(u\in G(B)^U\) originates in a member. It has exactly its old support in the union, since a common upper member with any other proposed incident point cannot add to that support. Thus its support is finite. Conversely, every finite subset of \(B^U\) lies in a member and is coded there. Uniqueness of its code can be checked in a common member containing any two proposed codes. The support map in \(U\) is consequently a bijection onto \([B^U]^{<\omega}\).

All arguments and values needed for a group operation or an action lie in a common member. This proves semantic totality and uniqueness in the union, as well as the group laws and fiber preservation. For two row points in the same union fiber, a common member containing both supplies their unique translator; the same argument applies to column points. Freeness is also checked in a common member. The fibers are therefore torsors for the required groups. Equation (5) follows by putting its finitely many arguments in a common member. No relations outside the prescribed types can appear in the union.

The base order is linear, dense, and without endpoints, since these assertions for finitely many points have witnesses in a containing member. More precisely, if \(a,c\in B^{M_i}\) and \(a<b<c\) in \(B^U\), choose a member containing \(b\) and then a common upper member with \(M_i\). Convexity in that member gives \(b\in B^{M_i}\). Hence \(B^{M_i}\) is convex in \(B^U\). A bounded interval in the union is exactly the corresponding interval in any member containing its endpoints, and so is countable. These arguments show that \(U\) is basic and that \(M_i\preccurlyeq_{\mathrm b}U\) for all \(i\).

The object condition. Fix \(t\in\mathcal T(I^U)\), and choose one member \(M_i\) containing its entries. Every row of \(t\) and of its nonempty subsequences is nonempty already in \(M_i\). Choose all their row representatives in this one member, for every \(n<\omega\). Over \(B^{M_i}\) their full test has a countable exception set, by the object condition for \(M_i\). These same colors can be calculated in \(U\) with columns from \(M_i\), so the old exception bound remains valid.

For \(b\in B^U\setminus B^{M_i}\), choose a member containing \(b\), followed by a common upper member with \(M_i\). The strong inclusion of \(M_i\) into that common member makes the full test pass at \(b\) using the selected rows. The same row and column points compute the same colors in \(U\). Thus the test fails only on the original countable set in \(B^{M_i}\).

The convenient choices just made may depend on \(t\). To check the definition with a single global row-choice system in \(U\), compare that system with these choices for \(t\) and its finitely many nonempty subsequences. Lemma 11 adds at most a countable set of possible differences. For each \(t\), its bad set is therefore countable also for the global system. Hence \(U\) is an object.

Strongness of the members. Fix \(i\), a tuple from \(I^{M_i}\), and \(b\in B^U\setminus B^{M_i}\). The same common-upper-member calculation, using rows from \(M_i\), supplies the full test at \(b\). Together with the verified basic inclusion this gives \(M_i\le_K U\).

A common upper bound. Suppose now that every \(M_i\le_K N\). The union is an induced substructure of \(N\), because each finite relation instance can be checked in a member containing its entries. Its \(G_*\) sort equals \(G_*^N\), and every union group element has its original support in \(N\). For two points of \(B^U\), choose a member containing both; convexity of that member in \(N\) forces every intervening point of \(B^N\) into that member and hence into \(B^U\). Thus \(U\preccurlyeq_{\mathrm b}N\).

Fix \(t\in\mathcal T(I^U)\) and \(b\in B^N\setminus B^U\). Choose a member \(M_i\) containing \(t\), and choose all the rows required for \(t\) and its subsequences inside \(M_i\). Because \(b\notin B^{M_i}\), the assumption \(M_i\le_K N\) supplies the full test at \(b\). Those representatives are also in \(U\) and are eligible for its strong-inclusion test into \(N\). Canonicality outside \(B^U\), from Lemma 11, makes this one choice sufficient. Hence \(U\le_K N\). ◻

Proof. If necessary add one point to make \(D\) nonempty. Set \(T_0=D\). Given \(T_m\), for each \(x\in T_m\) choose points \(x^-<x<x^+\) in \(B\), and adjoin them to form \(T_{m+1}\). Put \(T=\bigcup_{m<\omega}T_m\). Then \(T\ne\varnothing\), \(|T|\le\kappa\), and \(T\) has no endpoints. Let \[B_0=\{b\in B:\text{there exist }x,y\in T \text{ with }x\le b\le y\}.\] This is the convex hull of \(T\). It is a union of at most \(\kappa^2=\kappa\) closed bounded intervals, each countable after adjoining its endpoints. Thus \(|B_0|\le\kappa\). Convexity and density of \(B\) make \(B_0\) dense. If \(b\in B_0\) lies between \(x,y\in T\), choose points of \(T\) below \(x\) and above \(y\). They give points of \(B_0\) on both sides of \(b\), so \(B_0\) has no endpoints. ◻

Proof. Put \(\kappa=|A|+\aleph_0\). Choose a nonempty \(I_0\subseteq I^M\) of size at most \(\kappa\) containing \(A\cap I^M\) and every tuple-coordinate projection of every row or column element of \(A\). There are at most \(\kappa\) tuples in \(\mathcal T(I_0)\). For each of them, and for each \(n<\omega\), choose a representative \(z_{t,n}\in Z^M_{t,n}\). When computing the bad sets \(E_t\) for \(t\in\mathcal T(I_0)\), always use this same system of choices for all its subtuples. The object condition in \(M\), or an extension of these choices to a full row-choice system in \(M\), shows that each such \(E_t\) is countable.

Collect a subset \(D\subseteq B^M\) consisting of:

1. all points of \(A\cap B^M\), and all base-point projections of column elements of \(A\);

2. \(\mathop{\mathrm{supp}}(u)\) for every \(u\in A\cap G(B)^M\);

3. for every requested row point \(z\in A\cap Z^M_{t,n}\), the support of the unique \(u\in G(B)^M\) satisfying \(z=z_{t,n}+u\);

4. all the sets \(E_t\), for \(t\in\mathcal T(I_0)\).

In (ii)–(iv) the listed sets are included by taking their union. The first three clauses contribute at most \(\kappa\) points, since supports and projections are finite for each requested element. The last clause contributes at most \(\kappa\cdot\aleph_0=\kappa\) points. Therefore \(|D|\le\kappa\).

Apply Lemma 16 to obtain a nonempty convex dense \(B_0\subseteq B^M\) without endpoints, containing \(D\), of size at most \(\kappa\). Let \[H=\{u\in G(B)^M:\mathop{\mathrm{supp}}^M(u)\subseteq B_0\}.\] This is exactly the subgroup coding \([B_0]^{<\omega}\). Define \(N\) by retaining \(I_0,B_0,H\), and the whole group \(G_*^M\), together with the fibers \[\begin{align*} Z^N_{t,n}&=\{z_{t,n}+u:u\in H\} &&(t\in\mathcal T(I_0),\ n<\omega),\\ W^N_{t,b}&=W^M_{t,b} &&(t\in\mathcal T(I_0),\ b\in B_0), \end{align*}\] and all relations restricted from \(M\).

Each displayed row orbit is a nonempty \(H\)-torsor. Each retained column is the whole old \(G_*^M\)-torsor and remains one. The projections land in the retained sorts, the group operations and actions are total there, and Equation (5) restricts to these groups and fibers. Thus \(N\) is basic and \(N\preccurlyeq_{\mathrm b}M\).

The choices \(z_{t,n}\) are present in \(N\): they are obtained by the zero translator. At every \(b\in B_0\), they compute precisely the same colors in \(N\) and \(M\), using the retained whole column fibers. The bad set in \(N\) for any \(t\in\mathcal T(I_0)\) is therefore \(E_t\cap B_0\), which is countable. Hence \(N\) is an object. For \(b\in B^M\setminus B_0\), all these full tests pass because \(E_t\subseteq D \subseteq B_0\). The same chosen rows are eligible old representatives from \(N\). This proves the strong condition, so \(N\le_K M\).

It remains to verify containment of the requested data. The choices of \(I_0\) and \(B_0\) retain requested index and base points and all needed projections. A requested group element belongs to \(H\) by clause (ii). A requested row point belongs to its retained orbit by clause (iii). A requested column point belongs to a retained whole column fiber by clause (i) and the choice of \(I_0\). All requested elements of \(G_*^M\) are present because that entire group was retained. These are all possible carrier types, so \(A\subseteq |N|\). Finally Lemma 10 gives \[\|N\|=\max(|I_0|,|B_0|,\aleph_0) \le\kappa,\] as required. ◻

Proof. The language and its semantic structures were specified after Definition 7. Lemma 14 proves isomorphism invariance, substructure, the partial-order properties, and coherence. Lemma 15 proves the directed union and smoothness assertions, in particular the required chain axioms. Lemma 17 proves the downward bound \(\aleph_0\). Since the language is countable and \(\mathop{\mathrm{LS}}(K)\) is by definition infinite, its least possible value is \(\aleph_0\), which is therefore the value attained here. ◻

Proof. For each \(\alpha<\eta=\delta^+\), fix an injection \(j_\alpha:\alpha\longrightarrow\delta\). These form a set-sized family of choices. Define the functions by transfinite recursion, putting \[ f_\alpha(\beta) = \sup\{f_\gamma(\beta)+1: \gamma<\alpha,\ j_\alpha(\gamma)<\beta\}, \qquad \sup\varnothing=0. \tag{10}\] For each \(\beta<\omega_1\), the set of indices in this supremum is countable, because \(j_\alpha\) is injective and \(\beta\) is a countable ordinal. Regularity of \(\omega_1\) implies that the supremum is below \(\delta\). Thus the recursion defines a function into \(\delta\) at every stage \(\alpha<\eta\).

If \(\gamma<\alpha\) and \(\beta>j_\alpha(\gamma)\), the term \(f_\gamma(\beta)+1\) occurs in (10). Hence \[f_\gamma(\beta)<f_\alpha(\beta), \qquad E_{\gamma,\alpha}\subseteq j_\alpha(\gamma)+1.\] The latter ordinal is countable, proving the assertion. ◻

Proof. The set \(V_\omega\) of hereditarily finite sets is countably infinite, giving the assertion at \(\gamma=0\). At a successor stage, \[|V_{\omega+(\gamma+1)}| =|\mathcal P(V_{\omega+\gamma})| =2^{\beth_\gamma} =\beth_{\gamma+1}.\] If \(\gamma\) is a nonzero limit ordinal, continuity of ordinal addition and of the cumulative hierarchy gives \[V_{\omega+\gamma} =\bigcup_{\zeta<\gamma} V_{\omega+\zeta}.\] The inductive hypothesis gives a lower bound of \(\sup_{\zeta<\gamma}\beth_\zeta=\beth_\gamma\) for the cardinality of this union. It also gives the upper bound \(|\gamma|\cdot\beth_\gamma\). Strict increase of the beth sequence implies \(|\gamma|\leq\beth_\gamma\): the map \(\zeta\mapsto\beth_\zeta\), for \(\zeta<\gamma\), is an injection into the ordinal \(\beth_\gamma\). The upper bound is therefore \(\beth_\gamma\), completing the induction.

Since \(\omega+\omega_2=\omega_2\), the first conclusion follows. The rank assertion is the defining property of membership in \(V_\eta\). ◻

Proof. Fix a well-order of the set \(D\). For distinct \(a,b\in D\), let \(w(a,b)\) be the first element of \(a\triangle b\) in this well-order. This witness exists by set extensionality and belongs to \(D\), since \(D=V_\eta\) is transitive.

If \(A\subseteq D\) is nonempty and countable, define \[A_0=A,\qquad A_{n+1}=A_n\cup \{w(a,b):a,b\in A_n,\ a\ne b\}, \qquad C(A)=\bigcup_{n<\omega}A_n.\] Every \(A_n\), and hence \(C(A)\), is countable. Any two distinct elements of \(C(A)\) lie together in some \(A_n\); their chosen witness lies in \(A_{n+1}\). Thus membership on \(C(A)\) is extensional.

Recursively on the finite cardinality of \(X\), set \[D_X=C\left( X\cup \bigcup_{\varnothing\ne Y\subsetneq X}D_Y \right).\] The seed is nonempty and countable, because there are only finitely many proper subsets of \(X\). This proves (i) and (iii) and directly gives (ii) for proper inclusions; equality gives the remaining case.

Each \(D_X\) is nonempty and at most countable, so it admits a surjection from \(\omega\), allowing repetitions when it is finite. For \(X=\{x\}\), choose one whose initial entry is \(x\). All these choices are indexed by a set, and the axiom of choice supplies the family of surjections. ◻

Proof. Surjectivity of \(q_t\), together with (13), identifies the quotient bijectively with \(D_X\). Equation (14) identifies its relation with membership on \(D_X\), which is extensional. The tags in (15) depend only on the image under \(q_t\), so both the relation and the tags respect the equality relation.

For (i), list \(J\) increasingly as \(\{j_1<\cdots<j_m\}\). A label \((A,i)\) of the subtuple \(t\restriction J=(x_{j_1},\ldots,x_{j_m})\) corresponds to \((\{j_a:a\in A\},i)\) in the original tuple. Both labels denote the same entry \[d_{\{x_{j_a}:a\in A\}}(i).\] Their equality relations, membership relations, and tags therefore agree exactly. This proof applies to every ordered tuple; the enumeration \(d_Y\) was fixed for the underlying set \(Y\).

For the full diagram in (ii), suppose \(\beta\notin F_X\). Every membership edge \(y\in x\) with \(x,y\in D_X\) then satisfies \[f_{\mathop{\mathrm{rank}}(y)}(\beta)<f_{\mathop{\mathrm{rank}}(x)}(\beta)\] by (11). This is precisely the strict tag inequality required for that edge. Finally, \(q_t(\{j\},0)=x_j\), so the distinguished singleton labels are pairwise inequivalent. All validity conditions now hold.

For a subtuple with underlying set \(Y=X_J\), its quotient is \(D_Y\), whose membership relation is extensional by its own construction. In addition, \(\beta\notin F_Y\) follows from (12). The same argument proves the validity of this subtuple diagram. Combined with (i), these are exactly the conditions of the full subsequence test. ◻

Proof. The construction above and Lemma 20 give \(M_{\mathrm u}\in K\) with \[|I^{M_{\mathrm u}}|=|V_\eta|=\beth_\eta, \qquad |B^{M_{\mathrm u}}|=\aleph_1.\] Lemma 10 gives total cardinality \(\kappa=\beth_\eta\).

For \(M_{\mathrm c}\), take an index set of cardinality \(\kappa\), base order \(B=\mathbb Q\), and constant zero sequences \(a_{t,b}\). Lemma 13 supplies a basic structure and makes the object condition automatic because \(B\) is countable. Hence \(M_{\mathrm c}\in K\), and Lemma 10 gives \(\|M_{\mathrm c}\|=\kappa\).

An isomorphism preserves the unary predicate for the order sort. It therefore cannot identify \(M_{\mathrm u}\), whose order sort is uncountable, with \(M_{\mathrm c}\), whose order sort is countable. ◻

Proof. Define \(F\) recursively in increasing order of the tag \(\alpha<\delta\). At tag \(\alpha\), all predecessors have smaller tags, so their images have already been defined; the displayed formula then defines the images of all elements with tag \(\alpha\). These are sets, since \(Q\) is a set. Transfinite recursion and Replacement give a function on \(Q\).

We prove the stated bound by induction on \(\alpha=\rho(x)\). If \(yRx\) and \(\beta=\rho(y)\), the induction hypothesis gives \[F(y)\in V_{\beta+1}\subseteq V_\alpha, \qquad \beta<\alpha.\] Thus \(F(x)\subseteq V_\alpha\), and consequently \(F(x)\in V_{\alpha+1}\). At \(\alpha=0\) the predecessor set is empty, so the same conclusion holds. Since \(\delta\) is a limit ordinal, \(\alpha+1<\delta\) for every \(\alpha<\delta\), and the range of \(F\) lies in \(V_\delta\).

For injectivity, induct on \(\max(\rho(x),\rho(x'))\). Suppose \(F(x)=F(x')\). For each \(yRx\), equality of these sets supplies \(y'Rx'\) with \(F(y)=F(y')\). Both \(\rho(y)<\rho(x)\) and \(\rho(y')<\rho(x')\), so the induction hypothesis gives \(y=y'\). This proves that every predecessor of \(x\) is a predecessor of \(x'\), and the reverse inclusion follows in the same way. Extensionality gives \(x=x'\). At induction parameter zero both predecessor sets are empty, so extensionality gives the conclusion directly. ◻

Proof. Suppose that such a sequence exists. For each \(k\), let \(\mathcal D_k\) be the diagram decoded from \(s_k\). The tests assert that every \(\mathcal D_k\) is valid and that \[ \mathcal D_k\restriction J=\mathcal D_{|J|} \qquad(\varnothing\ne J\subseteq[k]). \tag{18}\]

Choose a linearly ordered set \(X\) with \(|X|>|V_\delta|\). Such an \(X\) can be the initial ordinal of cardinality \(|V_\delta|^+\). For each nonempty finite \(A\subseteq X\), transport \(\mathcal D_{|A|}\) along the increasing enumeration of \(A\), so that its labels become \[\{(U,i):\varnothing\ne U\subseteq A,\ i<\omega\}.\] Let \(Q_A\), \(R_A\), and \(\rho_A\) denote its quotient, quotient relation, and tag function. If \(A\subseteq B\) are nonempty and finite, the label inclusion and Equation (18) give a map \[j_{A,B}:Q_A\longrightarrow Q_B.\] By Lemma 5, these maps are injective, preserve tags, preserve and reflect the relation, and satisfy \[j_{B,C}j_{A,B}=j_{A,C} \qquad(A\subseteq B\subseteq C).\]

We construct their limit explicitly. Form the set \[P=\{(A,a):\varnothing\ne A\subseteq X \text{ is finite},\ a\in Q_A\}.\] This is a set-indexed union of countable sets. Declare \[ (A,a)\sim(B,b) \quad\Longleftrightarrow\quad j_{A,A\cup B}(a)=j_{B,A\cup B}(b). \tag{19}\] Passing to a larger finite common stage preserves equality and reflects it by injectivity. The composition identities therefore show that \(\sim\) is an equivalence relation: in particular, two equalities witnessing transitivity can both be read in the stage indexed by the union of their three finite index sets. Put \(Q=P/{\sim}\), and let \(j_A:Q_A\to Q\) send \(a\) to the class of \((A,a)\). Each \(j_A\) is injective, and \[j_Bj_{A,B}=j_A.\] Every finite collection of elements of \(Q\) lies in the image of one \(j_A\), by taking a union of finitely many index sets.

Define tags on the limit by \(\rho(j_A(a))=\rho_A(a)\). Define its relation using a finite common stage: for \(a\in Q_A\), \(b\in Q_B\), and \(C=A\cup B\), set \[ j_B(b)\,R\,j_A(a) \quad\Longleftrightarrow\quad j_{B,C}(b)\,R_C\,j_{A,C}(a). \tag{20}\] These definitions are independent of the representatives. Indeed, representatives that describe the same limit points become equal in a finite common stage by Equation (19). Taking the union of that stage with all stages used in Equation (20) makes the relevant representatives equal simultaneously. Tag preservation gives the same tag, and preservation and reflection of \(R\) give the same truth value for the relation. It also follows that each \(j_A\) preserves and reflects \(R\), and that \[yRx\ \Longrightarrow\ \rho(y)<\rho(x) \qquad(x,y\in Q).\]

The limit relation is extensional. To see this, take distinct \(x,x'\in Q\) and put them in a common stage, say \(x=j_A(a)\) and \(x'=j_A(a')\). Injectivity implies \(a\ne a'\). Extensionality in \(Q_A\) gives a predecessor distinguishing them. After exchanging \(a,a'\) if needed, there is \(b\in Q_A\) with \[bR_Aa,\qquad \neg(bR_Aa').\] Because \(j_A\) preserves and reflects the relation, \(j_A(b)Rx\) and \(\neg(j_A(b)Rx')\). This witness remains valid even if larger stages add other predecessors.

For \(u\in X\), consider the element of \(Q_{\{u\}}\) represented by the label \((\{u\},0)\), and let \(q_u\) be its image in \(Q\). If \(u\ne v\), condition (iii) of Definition 2, applied in the stage \(Q_{\{u,v\}}\), says that the two corresponding elements are distinct. Injectivity of the stage map gives \(q_u\ne q_v\). Thus \[|X|\le |Q|.\] Lemma 24 applies to the set \(Q\), with its extensional relation and tags below \(\delta\). It gives an injection into \(V_\delta\), whence \[|X|\le |Q|\le |V_\delta|.\] This contradicts the choice of \(X\). ◻

Proof. Put \(\kappa=\xi^+\). This is a regular cardinal and a limit ordinal. The beth sequence is strictly increasing and continuous at limit ordinals, so \[\Lambda=\sup_{\alpha<\kappa}\beth_\alpha.\] This gives \(\mathop{\mathrm{cf}}(\Lambda)\le\kappa\). Conversely, a set of fewer than \(\kappa\) ordinals below \(\Lambda\) can be bounded by beth values with fewer than \(\kappa\) indices. Regularity of \(\kappa\) bounds these indices below \(\kappa\), and therefore bounds the original set below \(\Lambda\). This proves \(\mathop{\mathrm{cf}}(\Lambda)=\kappa\).

Given an infinite cardinal \(\nu<\Lambda\), choose \(\alpha<\kappa\) with \(\nu\le\beth_\alpha\). Since \(\alpha+1<\kappa\), \[2^\nu\le 2^{\beth_\alpha}=\beth_{\alpha+1}<\Lambda.\] Thus \(\Lambda\) is a strong limit. It is also a limit cardinal: for every cardinal below it, a strictly larger beth value still lies below it. In particular \(\xi<\Lambda\), and for infinite \(\zeta<\Lambda\), \[\xi^\zeta\le (2^\xi)^\zeta =2^{\xi\cdot\zeta}<\Lambda.\] The last inequality uses \(\xi\cdot\zeta<\Lambda\) and strong limitness. The successor of \(\xi^\zeta\) is also below the limit cardinal \(\Lambda\). ◻

Proof. By identifying the colors with elements of \(\xi\), it suffices to use the palette \(\xi\). We induct on \(m\), proving the statement for all infinite targets \(\chi<\Lambda\) at each step. When \(m=1\), take \[\mu=(\max(\xi,\chi))^+<\Lambda.\] If every color class had size less than \(\chi\), their union would have size at most \(\xi\cdot\chi<\mu\). Thus some class has at least \(\chi\) elements, from which we select exactly \(\chi\).

Suppose the statement is known for \(m\), and fix a target \(\chi<\Lambda\). Choose an infinite cardinal \(\zeta<\Lambda\) such that every \(\xi\)-coloring of \([\zeta]^m\) has a homogeneous \(\chi\)-element subset. Set \[q=\xi^\zeta,\qquad \mu=q^+<\Lambda,\] where the last inequality follows from Lemma 27. Let \(c:[\mu]^{m+1}\to\xi\). We seek \(\zeta\) increasing representatives and a later point \(x\) such that the color of any \(m+1\) representatives is unchanged when its last point is replaced by \(x\). Coloring an \(m\)-set by the color obtained after adjoining \(x\) then reduces to the induction hypothesis. The residual-set tree below groups points by their profiles on the named representatives along each branch. Its node count leaves an unnamed \(x\), whose residuals determine the required branch.

For each \(\alpha<\zeta\), fix an injection \[ \iota_\alpha:{}^{[\alpha+1]^m}\xi\longrightarrow q. \tag{21}\] Such an injection exists because \(|[\alpha+1]^m|\le\zeta\). Index potential tree nodes by sequences \(s\in{}^\alpha q\), for \(\alpha\le\zeta\). Define their residual sets \(X_s\subseteq\mu\) recursively as follows.

1. At the root, put \(X_\varnothing=\mu\).

2. Suppose \(s\) has length \(\alpha<\zeta\) and \(X_s\) is nonempty. Name its least point \[r_s=\min X_s.\] For \(y\in X_s\setminus\{r_s\}\), define its profile \(u_{s,y}\in{}^{[\alpha+1]^m}\xi\) by \[ u_{s,y}(a)=c\bigl(\{r_{s\upharpoonright\beta}:\beta\in a\} \cup\{y\}\bigr), \qquad a\in[\alpha+1]^m. \tag{22}\] For each \(i<q\), put \[X_{s^\frown i} =\{y\in X_s\setminus\{r_s\}:\iota_\alpha(u_{s,y})=i\}.\] If \(X_s\) is empty, set every immediate successor residual to the empty set.

3. If \(\gamma\le\zeta\) is a nonzero limit ordinal and \(s\in{}^\gamma q\), put \[ X_s=\bigcap_{\alpha<\gamma}X_{s\upharpoonright\alpha}. \tag{23}\]

Only nodes with nonempty residuals matter. Every such node has nonempty ancestral residuals, so all representatives in (22) are defined. Along a branch the representatives increase strictly: each one is the least point of the current residual, and successor residuals exclude that point. Consequently the arguments of \(c\) in (22) are \((m+1)\) distinct points. Once \(\alpha+1\ge m\), the index set \([\alpha+1]^m\) includes subsets containing \(\alpha\) itself, so the profile includes tests using the just named point \(r_s\).

The number of potential nodes, including those at limit levels, is bounded by \[ \left|\bigcup_{\alpha\le\zeta}{}^\alpha q\right| \le |\zeta+1|\cdot q^\zeta =\zeta\cdot(\xi^\zeta)^\zeta =\xi^\zeta=q. \tag{24}\] Here \(\zeta\) is infinite, \(q\ge\zeta\), and \(\zeta\cdot\zeta=\zeta\). In particular at most \(q\) points are named at levels below \(\zeta\). Since \(\mu=q^+\), choose a point \(x\in\mu\) that is never named.

There is a unique branch of residuals containing \(x\) through all levels at most \(\zeta\). Indeed, if \(x\in X_s\) at a successor step, then \(x\ne r_s\), so exactly one of the profile classes contains it. At a limit step, it belongs to the intersection (23) along the branch already constructed. Thus the branch cannot disappear at a limit. Write its named representatives as \[r_\alpha\quad(\alpha<\zeta), \qquad P=\{r_\alpha:\alpha<\zeta\}.\] They increase strictly and are all less than \(x\), so \(|P|=\zeta\).

Define a coloring of the preceding arity by \[d:[P]^m\longrightarrow\xi, \qquad d(A)=c(A\cup\{x\}).\] Consider indices \(\alpha_0<\cdots<\alpha_m<\zeta\). At level \(\alpha_{m-1}\) of the branch, all the first \(m\) representatives in this list have appeared, including the just named one. The last representative \(r_{\alpha_m}\) and the point \(x\) belong to the same successor residual at that level. Their profiles therefore agree on \(\{\alpha_0,\ldots,\alpha_{m-1}\}\), giving \[ c(\{r_{\alpha_0},\ldots,r_{\alpha_m}\}) =d(\{r_{\alpha_0},\ldots,r_{\alpha_{m-1}}\}). \tag{25}\] By the choice of \(\zeta\), the map \(d\) has a homogeneous subset \(H\subseteq P\) of cardinality \(\chi\). Equation (25) shows that \(H\) is homogeneous for \(c\) as well. This proves the induction step. ◻

Proof. Choose the colors recursively. After choosing \(p_1,\ldots,p_j\), maintain the following invariant: for every infinite cardinal \(\chi<\Lambda\), there is a set \(Y\subseteq X\) with \(\chi\le|Y|<\Lambda\) such that each \(c_i\) for \(1\le i\le j\) is constantly \(p_i\) on \([Y]^i\). For \(j=0\) this follows from \(|X|\ge\Lambda\).

Assume the invariant holds at \(j\). For each infinite \(\chi<\Lambda\), Lemma 28 supplies a source cardinal \(\mu_\chi<\Lambda\) for arity \(j+1\) and target \(\chi\). Choose an existing sample of size at least \(\mu_\chi\), restrict to \(\mu_\chi\) points, and apply the lemma to obtain a subset \(Z_\chi\) of size \(\chi\) on which \(c_{j+1}\) has a constant color \(q_\chi\in C_{j+1}\). All earlier colors are retained on this subset.

At least one color occurs as \(q_\chi\) for target cardinals \(\chi\) unbounded below \(\Lambda\). Otherwise, for every \(q\in C_{j+1}\) there would be a bound below \(\Lambda\) for the targets assigned color \(q\). Since \(|C_{j+1}|\le\xi<\mathop{\mathrm{cf}}(\Lambda)\), the supremum of these bounds would still be below \(\Lambda\). This contradicts the fact that we made the construction for every infinite target below the limit cardinal \(\Lambda\). Choose such a color as \(p_{j+1}\); its samples establish the invariant at \(j+1\).

After this recursion, fix a positive integer \(k\). The invariant at stage \(k\) supplies an infinite sample homogeneous in the first \(k\) chosen colors. Any \(k\) points of that sample give \(A_k\). ◻

Proof. Suppose instead that \(|I^M|\ge\Lambda\). Fix a well-order of \(I^M\), used only in this proof, and fix row representatives \(z_{t,n}\) for every tuple \(t\) and every \(n<\omega\) in \(M\). Let \[c_t:B^M\longrightarrow S\] be the resulting color profile of \(t\), as defined in Section 3. By CH, \(|S|=\delta\), and Lemma 9 gives \(|B^M|\le\delta\). Thus the palette of whole profiles has size at most \[ |S^{B^M}|\le\delta^\delta=2^\delta=\xi. \tag{26}\] For the middle equality, \(2^\delta\le\delta^\delta\) follows from \(2\le\delta\), while \(\delta^\delta\le(2^\delta)^\delta=2^\delta\) gives the reverse inequality.

For each \(j\ge1\), color a \(j\)-element subset of \(I^M\) by the profile of its increasing enumeration. Apply Lemma 29 to these colorings, with every palette equal to \(S^{B^M}\). Obtain profiles \(p_j\in S^{B^M}\) and, for each \(k\), an increasing witness tuple \(t_k\) of length \(k\) whose increasing \(j\)-subtuples all have profile \(p_j\), for \(j\le k\).

For the fixed global row representatives, let \(E_k\subseteq B^M\) be the countable exceptional set for the full object test of \(t_k\). By the definition of that test, it includes all required checks on the nonempty subsequences of \(t_k\). The set \[E=\bigcup_{1\le k<\omega}E_k\] is countable. Choose \(b\in B^M\setminus E\), possible because \(B^M\) is uncountable, and put \(s_j=p_j(b)\) for every \(j\ge1\). For each \(k\), evaluation on \(t_k\) proves \[T_k\bigl((s_{|J|})_{\varnothing\ne J\subseteq\{1,\ldots,k\}}\bigr).\] This is the sequence forbidden by Lemma 25. The contradiction proves the bound. ◻

Proof. Fix a bijection \(f:I^M\to I^N\). Both base orders are nonempty countable dense linear orders without endpoints. There is an order isomorphism \(g:B^M\to B^N\), as follows. Enumerate the two orders and build finite partial increasing bijections, alternately including the next unused point of each enumeration in the domain and in the range. At each step, density supplies a point between the finitely many already matched neighbors, or absence of endpoints supplies a point beyond them. The appropriate interval contains infinitely many points, so the finitely many used points can be avoided. The union is the required bijection \(g\).

The map \(g\) induces the group isomorphism \[\widehat g:G(B^M)\longrightarrow G(B^N), \qquad u\longmapsto g[u],\] where elements of the coded groups are identified here with their finite supports. Match the two copies of \(G_*\) by their distinguished elements. Enumerate \(B^M\) as \((b_k:k<\omega)\); this enumeration need not respect its order.

Fix one tuple \(t\) of distinct points in \(I^M\), and let \(f(t)\) be its coordinatewise image. Choose representatives \[\begin{array}{ll} z_n\in Z^M_{t,n},&w_k\in W^M_{t,b_k},\\ z'_n\in Z^N_{f(t),n},&w'_k\in W^N_{f(t),g(b_k)}. \end{array}\] Write their bit matrices as \[a(n,k)=e^M(z_n,w_k),\qquad a'(n,k)=e^N(z'_n,w'_k),\] and let \(d(n,k)=a(n,k)+a'(n,k)\), with addition in \(\mathbb Z/2\mathbb Z\). Define translators by \[ \begin{split} U_n&=\{g(b_k):k\le n\text{ and }d(n,k)=1\}\in G(B^N),\\ V_k&=\{n:n<k\text{ and }d(n,k)=1\}\in G_*. \end{split} \tag{27}\] Every \(U_n\) is finite, since it uses only the first \(n+1\) columns; every \(V_k\) is finite, since it uses only the first \(k\) rows. The two regions in (27) partition the matrix, so \[ \boldsymbol 1_{g(b_k)\in U_n} +\boldsymbol 1_{n\in V_k}=d(n,k)\pmod2 \qquad(n,k<\omega). \tag{28}\] Figure 1 illustrates this allocation of finite supports.

Set \(\widetilde z'_n=z'_n+U_n\) and \(\widetilde w'_k=w'_k+V_k\). The action equation for the bit relation and (28) give \[e^N(\widetilde z'_n,\widetilde w'_k) =a'(n,k)+d(n,k)=a(n,k).\]

Because every fiber is a torsor, its points have unique expressions relative to its chosen representative. We therefore obtain bijections of the row and column fibers by setting \[ \begin{aligned} z_n+u&\longmapsto\widetilde z'_n+\widehat g(u) &&(u\in G(B^M)),\\ w_k+v&\longmapsto\widetilde w'_k+v &&(v\in G_*). \end{aligned} \tag{29}\] These maps are equivariant and hence preserve the action graphs. For arbitrary \(u\in G(B^M)\) and \(v\in G_*\), their target bit is \[\begin{split} e^N(\widetilde z'_n+\widehat g(u),\widetilde w'_k+v) &=a(n,k)+\boldsymbol 1_{g(b_k)\in\widehat g(u)} +\boldsymbol 1_{n\in v}\\ &=a(n,k)+\boldsymbol 1_{b_k\in u}+\boldsymbol 1_{n\in v}\\ &=e^M(z_n+u,w_k+v). \end{split}\] Thus they preserve the entire bit relation, not just the bits at representatives.

Carry out this construction separately for every tuple \(t\). The row and column fibers of distinct tuples are disjoint, and there are no additional bit or action relations between different tuples. Together with \(f\), \(g\), \(\widehat g\), and the distinguished-element map on \(G_*\), these fiber maps give a bijection of the whole universes. They preserve and reflect the sort predicates, tuple and base projections, order, group incidence and operation graphs, action graphs, distinguished elements, and bits. They therefore form an isomorphism of the structures. ◻

Proof. Fix such a cardinal \(\mu\). By Lemma 13, choose a model with \(|I|=\mu\), base order \(\mathbb Q\), the specified group torsors, and, for example, zero bit sequences at the chosen representatives. The countable base order makes the object test automatic. Lemma 10 gives cardinality exactly \(\mu\), proving existence.

Now let \(M\in K\) have cardinality \(\mu\). By Lemmas 9 and 10, \[|B^M|\le\delta<\Lambda\le\mu, \qquad \mu=\max(|I^M|,|B^M|,\aleph_0).\] It follows that \(|I^M|=\mu\). Proposition 30 therefore forces \(B^M\) to be countable. Any two models of size \(\mu\) now have equally sized index sorts and countable base orders, so Lemma 32 makes them isomorphic. This proves existence of exactly one isomorphism type at every \(\mu\ge\Lambda\), including \(\mu=\Lambda\) itself. ◻

Proof of Corollary 34. The class and strong relation are given by fixed formulas with the set of coding maps as parameter. Expanding these formulas in the AEC axioms and the stated model assertions gives the sentence \(\Theta\). The construction and its verification in Theorem 1 therefore prove, in ZFC, \(\mathrm{CH}\Rightarrow\Theta\).

For each \(\Phi\) specified above, its ZFC-provable fixed-family instance applies to the parameter witnessing \(\Theta\). It would give categoricity in \(h(\aleph_0)\), contradicting the two nonisomorphic models required by \(\Theta\). Thus ZFC proves \(\Theta\Rightarrow\neg\Phi\).

Gödel’s relative-consistency theorem (Gödel 1938) gives \(\mathop{\mathrm{Con}}(\mathrm{ZFC})\Rightarrow \mathop{\mathrm{Con}}(\mathrm{ZFC}+\mathrm{CH})\). Since the latter theory proves \(\Theta\), its consistency implies \(\mathop{\mathrm{Con}}(\mathrm{ZFC}+\Theta)\), and the proved implication \(\Theta\Rightarrow\neg\Phi\) then gives \(\mathop{\mathrm{Con}}(\mathrm{ZFC}+\neg\Phi)\). If \(\Phi\) were a theorem of consistent ZFC, adjoining \(\neg\Phi\) could not give a consistent theory. ◻

Proof. Let \(M\) be the model with uncountable base from Theorem 23. By Theorem 18, choose a countable \(A\le_K M\). Construct an extension \(N\) of \(A\) by enlarging only its index sort to cardinality \(\Lambda^+\), keeping \(B^N=B^A\), both old group sorts, and all fibers and bits belonging to old tuples. For each new tuple add the required independent torsors and any bit array satisfying the translation law. The countability of \(B^N\) makes the object condition automatic. This is a basic inclusion \(A\subseteq N\), and the strong condition is vacuous because the base order has not grown. Thus \(A\le_K N\).

If \(M\) and \(N\) strongly embedded into a common model \(P\), the image of \(M\) would force \(B^P\) to be uncountable and the image of \(N\) would force \(|I^P|\ge\Lambda^+\). This contradicts Proposition 30. There is therefore no joint embedding of \(M,N\), and in particular no amalgam of the two extensions \(A\le_K M,N\). ◻

Proof. First we construct compatible colors for all tuples over \(I=I^M\). Choose an injection \(j:I\to\omega\). For each nonempty finite \(X\subseteq I\), choose a surjection \(d_X:\omega\to\omega\), requiring \(d_{\{x\}}(0)=j(x)\). For example, set \(d_X(n+1)=n\), and choose the zeroth value as prescribed for singletons and as zero otherwise. For a tuple \(t=(x_1,\ldots,x_k)\) and a label \((J,n)\in\mathcal L_k\), put \[q_t(J,n)=d_{\{x_r:r\in J\}}(n).\] Define a diagram \(D_t\) by equality of these values, by ordinal membership between them, and by the tag \(\rho_t(J,n)=q_t(J,n)\). Its quotient is \(\omega\), since the labels \(([k],n)\) already surject onto \(\omega\). Ordinal membership on this quotient is extensional and strictly decreases the tags, which lie below \(\delta\). The distinguished singleton labels have the distinct values \(j(x_r)\). Thus \(D_t\) is valid. Restricting to a subsequence gives exactly its separately valid diagram: the definition of \(d_X\) depends on the underlying finite set, not its position in a larger tuple. Consequently the colors \(s_t=\iota_k(D_t)\) satisfy every full-subsequence test. When \(I\) is infinite, the unary colors are distinct; when \(I\) is finite, there are no tuples at sufficiently large arities. Thus this does not produce the fixed-arity pattern excluded by Lemma 25.

Take the ordered sum \(B'=B^M+\mathbb Q\), with a disjoint copy of \(\mathbb Q\). It is a countable dense order without endpoints, and \(B^M\) is convex in it. Keep \(I^M\) and the exact old labeled group \(G_*^M\). Enlarge \(G(B^M)\) to \(G(B')\) by retaining each old code with its old support and adding one new code for every remaining finite subset of \(B'\). Choose old row origins \(z_{t,n}\), and extend each old row torsor to a \(G(B')\)-torsor: retain the points with old support coordinates and adjoin one point for each remaining coordinate, with the action given by symmetric difference. Keep every old column torsor, choose an origin \(w_{t,b}\) in it, and add a new \(G_*^M\)-torsor with an origin \(w_{t,b}\) for each new \(b\).

Choose \(a_t\in2^\omega\) representing \(s_t\), and prescribe the origin bits by \[a_{t,b}(n)= \begin{cases} e^M(z_{t,n},w_{t,b}),&b\in B^M,\\ a_t(n),&b\in B'\setminus B^M. \end{cases}\] Extend them to all points by the torsor formula \[e'(z_{t,n}+u,w_{t,b}+v) =a_{t,b}(n)+\boldsymbol1_{b\in\mathop{\mathrm{supp}}(u)} +\boldsymbol1_{n\in v}\pmod2.\] Unique torsor coordinates make this well-defined. The old translation law (5) shows that every old bit, true or false, is unchanged. All group and action values on old arguments are unchanged as well. Give the enlarged carriers exactly the required relations, with zero bits between different tuple fibers. This is a basic inclusion, and its countable base makes the enlarged structure an object.

At every new base point the colors, using the chosen old rows, are the \(s_t\), so all old-tuple tests pass. Changing to other old row points has no effect there: the translators have supports contained in \(B^M\). Changing column origins preserves colors modulo \(=^*\). Hence the inclusion is strong, not just basic. Finally, Lemma 10 makes the extension countable. ◻

Proof. Choose a countable strong map \(a:A\to H\) whose image contains \(B^H\), using the downward Löwenheim–Skolem property and then the representative in \(\mathcal C_0\). Define \[R_A=\{r:A\to D\text{ in }\mathcal C_0: r[B^A]\subsetneq B^D\}\subseteq y_A.\] Injectivity makes this a cosieve. For any \(f:A\to D\), Lemma 36, followed by an isomorphism to the chosen representative in \(\mathcal C_0\), gives a countable strong map \(g:D\to D'\) adding a base point outside \(g[B^D]\). It follows that \(gf\in R_A\). Thus \(R_A\) satisfies (30), without any amalgamation assumption.

The image of \(p_H^*(R_A)\to p_H^*(y_A)\) consists exactly of maps \(A\to H\) factoring as \(hr\) with \(r\in R_A\) and \(h:D\to H\) strong. But \(a\) has no such factorization. If \(a=hr\), choose \(b\in B^D\setminus r[B^A]\). Since \(h(b)\in B^H=a[B^A]\), there is \(x\in B^A\) with \(h(b)=a(x)=h(r(x))\), contrary to injectivity of \(h\).

Sheafification for \(J_{\neg\neg}\) inverts the dense inclusion \(R_A\hookrightarrow y_A\). If \(p_H\) factored through the sheaf subtopos, its inverse image would therefore send that inclusion to an isomorphism. The omitted element \(a\) proves that it does not even send it to a surjection. Finally, models of cardinality at least \(\Lambda\) have countable base by Lemmas 9 and 10 together with Proposition 30, and exist by Theorem 33. ◻