Proof. For an ideal \(U\), choose elements whose heights approach \(\sup\rho[U]\), and replace their successive initial segments by their finite joins. This gives a nondecreasing sequence \((n_i)\) in \(U\) with heights approaching the same supremum. If \(d\in U\) divides none of the \(n_i\), then \[\rho(n_i\vee d)-\rho(n_i)>\epsilon_d\] for every \(i\), contradicting convergence to the supremum. Prepending \(1\) makes \(n_0=1\). The proof applies in the stated extension as well; its choices are made in that \(\mathsf{ZFC}\) universe. ◻

Proof. Normal forms. Let \(S\) be the direct limit of the sets \(M\) under the maps \(x\mapsto xd_i\). Write \([x,i]\) for the image of \(x\) at stage \(i\). Equality in this direct limit means equality at a finite common stage. The transition maps need not be injective: no right cancellation has been assumed. Nevertheless the left \(M\)-action on \(S\) is injective for each multiplier. Indeed, equality after multiplying two letters by an old \(u\) becomes \(uX=uY\) at a common stage, where left cancellation gives \(X=Y\).

There are well-defined equivariant maps \[k([x,i])=xc_i,\qquad h(s)=k(s)e.\] The identity \(d_ic_{i+1}=c_i\) proves well-definedness. Before imposing the second relation in Equation (6), the normal forms are strings \[s_1\cdots s_j y\qquad(s_i\in S,\ y\in M),\] including \(j=0\). The letter \([x,i]\) represents \(xp_i\). Old factors between new generators are absorbed into the following letter, and the transition relations are precisely equality in \(S\). Multiplication concatenates strings, using the left action to absorb the terminal old factor of the first string.

The remaining reductions are \[ s(bt)\longmapsto h(s)t, \tag{8}\] where \(t\) is a letter of \(S\) or a terminal old element. The quotient \(t\) is unique because the left \(b\)-action is injective. Each reduction removes one new letter. The only overlapping reductions occur in \(s\,(bt)\,(bu)\), with the final factor possibly terminal. Reducing in either order gives the same result by \[h(bt)=b h(t),\qquad h(h(s)t)=h(s)h(t).\] Disjoint reductions commute by associativity of the action. By Newman’s lemma (Newman 1942) (see (Dershowitz and Plaisted 2001, Lemma 5.13)), these local diamonds and termination give unique irreducibles: besides the old elements, they are strings whose first letter is arbitrary and whose later letters and terminal factor are not left-divisible by \(b\).

Old left multipliers act injectively on these forms. Left multiplication by a letter \(s\) either prepends \(s\), when the input is not a \(b\)-multiple, or sends \(bZ\) to \(h(s)Z\). Both cases are injective. Their ranges are disjoint, because \[ s\notin h(s)S. \tag{9}\] To see this, \(s\in xS\) implies \(x\sqsubseteq k(s)\), whereas \(k(s)e\not\sqsubseteq k(s)\) by conicality and left cancellation. Thus every left multiplication is injective. A new word can become old only by consuming its first letter, at which point it is a multiple of \(h(s)\ne1\). It cannot equal \(1\), proving conicality.

Old cones and the first-letter blocks. For \(s\in S\), let \(B_s\) consist of all irreducibles beginning with \(s\). For old \(x\) the normal forms give \[ xM'=xM\ \cup\!\bigcup_{s\in xS}B_s. \tag{10}\] At a common stage in the direct limit, \(xS\cap yS\) is \((x\vee y)S\) if the old join exists, and is empty if the old cones are disjoint. Thus old comparisons, their right factors, joins and nonjoins are unchanged. Notice that this conclusion has not used a join theorem for arbitrary new words.

Exits and gates. Fix an irreducible \(w=sY\). Right multiplication either leaves its first letter intact or eventually consumes that letter. We prove the following precise alternative: the set \(wM'\setminus B_s\) is empty, or it is one cone \(g(w)M'\) whose root \(g(w)\) is old. Thus the gate will describe every exit from the fixed-head block, not only the old multiples of \(w\).

The first letter is consumed exactly when the suffix becomes a \(b\)-multiple, so first calculate \(YM'\cap bM'\). If \(Y\) is old, Equation (10) gives the old join \(Y\vee b\), or an empty intersection. If \(Y\) is new with head \(t\), irreducibility gives \(t\notin bS\). No member of \(B_t\) is then a \(b\)-multiple. By induction on the number of letters in the suffix, all possible exits of \(Y\) form the old-rooted cone \(g(Y)M'\), if there are any. Its intersection with \(bM'\) is calculated by the old join \(g(Y)\vee b\).

In either case the suffix intersection is empty or is \(zM'\) for an old \(z=bu\) with old \(u\). The factor \(u\) is old by conservation of old comparisons. In the nonempty case, multiplication by \(s\) and the reduction \(sbu=h(s)u\) give \[ wM'\setminus B_s=g(w)M',\qquad g(w)=h(s)u. \tag{11}\] This cone cannot return to \(B_s\): every new head in it belongs to \(h(s)S\), whereas \(s\notin h(s)S\) by Equation (9). This proves the exit alternative. Every old multiple of \(w\) lies outside \(B_s\), so \(g(w)\) is in particular its least old multiple.

We record also the right factor \(c(w)\) with \(wc(w)=g(w)\). If \(Y\) is old, it is the old quotient of \(z\) by \(Y\). If \(Y\) is new and \(Yc(Y)=g(Y)\), it is \[ c(w)=c(Y)v, \qquad g(Y)v=z. \tag{12}\] All quotients in this recursion are old except the already constructed \(c(Y)\). This explicit calculation will ensure conservation of right factors when the same presentation is simulated over a larger base.

Append an old \(d\) to \(w\). If the product leaves \(B_s\), its first letter has been consumed; that reduction can occur only after all intervening letters have been consumed. The result is then entirely old. Since the gate cone is disjoint from \(B_s\), the hypothesis \(g(w)\sqsubseteq wd\) implies just such an exit. This proves Equation (4).

All conditional joins. For two forms with the same head, cancel that head and intersect their suffix cones, using induction on the total number of new letters. For old \(x\) and new \(w\in B_s\), either \(s\in xS\), in which case \(x\sqsubseteq w\), or every common multiple must leave \(B_s\). The latter intersection is computed through \(g(w)\) and an old join. For \(w\in B_s\) and \(v\in B_t\) with \(s\ne t\), an intersection inside \(B_s\) requires \(g(v)\) to divide a member of \(B_s\). By Equation (10) it then divides all of \(B_s\), so \(v\sqsubseteq w\). The symmetric case is the same. Otherwise a common multiple must leave both blocks, and the intersection is computed by the old join of their gates. Missing gates or missing old joins give an empty intersection. This proves conditional joins in every case.

The prescribed divisor profile. For any letter \(s\), the old divisors of every element of \(B_s\) form \[ P_s=\{x\in M:s\in xS\}\subseteq\downarrow k(s). \tag{13}\] This is an ideal: common-stage representatives and old joins prove join closure. For the head \([1,0]\) of \(m=p_0\), it is precisely \(\bigcup_i\downarrow_M n_i\), and the gate is \(ae\). The defining relation gives \(mb=ae\). Since \(ae\not\sqsubseteq a\), no member of \(B_{[1,0]}\) divides \(a\); in particular \(m\not\sqsubseteq a\).

Now let \(x\) be a new divisor of \(a\). It is outside that block and has an old gate \(g(x)\sqsubseteq a\). If \(x\sqsubseteq m\), the comparison leaves its block, so \(g(x)\sqsubseteq m\), and the old profile puts \(g(x)\) below some \(n_i\). Conversely \(x\sqsubseteq n_i\) implies \(x\sqsubseteq m\). If \(x\not\sqsubseteq m\), its gate also fails to divide \(m\). The possibility \(m\sqsubseteq x\) is excluded by \(x\sqsubseteq a\). The gate calculation consequently gives \(x\vee m=g(x)\vee m=ae\). The corresponding assertions for old \(x\) follow directly from its block membership. This proves Equation (7), including new divisors of \(a\). ◻

Proof. Use \(P_s\) from Equation (13), and put \(A_s=\sup\rho[P_s]\). We place the whole block \(B_s\) in a short height interval above its old divisors and below \(\rho(h(s))\). Here \(h(s)\) is the gate of the bare letter \(s\); the gate of a longer word in \(B_s\), when present, is a multiple of \(h(s)\) and need not equal it. The interval must leave enough room for the costs of both the old divisors and the new words. More precisely, there are positive \(u_s,\delta_s\) with \[ \begin{split} u_s-A_s&>\delta_s,\\ \rho(h(s))-u_s-\delta_s &>\sup\{\epsilon_d:d\sqsubseteq h(s),\ d\in M\setminus P_s\}. \end{split} \tag{14}\] Indeed, put \(p=\rho(k(s))-A_s\geq0\) and \(q=\rho(h(s))-\rho(k(s))>0\). For \(d\sqsubseteq k(s)\) missing \(P_s\), every \(x\in P_s\) misses \(d\), and the old margin yields \(\epsilon_d<\rho(k(s))-\rho(x)\). The supremum of these costs is at most \(p\). The supremum for \(d\sqsubseteq h(s)\) not dividing \(k(s)\) is strictly below \(q\). Thus the full supremum on the right of Equation (14) is strictly less than \(p+q=\rho(h(s))-A_s\), also when \(p=0\). This leaves the required positive room for \(u_s\) and \(\delta_s\).

Define recursively on irreducibles \[ \begin{gathered} \rho(sY)=u_s+\delta_s\rho(Y),\qquad 0<\epsilon_{sY}\leq\delta_s\epsilon_Y,\\ \epsilon_{sY}\leq\epsilon_{g(sY)} \quad\text{whenever the gate exists}. \end{gathered} \tag{15}\] These choices give heights in \((0,1)\) and costs in \((0,1]\). We verify all comparisons, including the suprema.

For two elements in one block \(B_s\), a divisor of the upper element from outside that block also divides the lower one. An old divisor belongs to \(P_s\); a new divisor with a different head must enter by its old gate, which then divides every member of \(B_s\). Inside the block, cancellation removes \(s\), and the margin follows by induction from the factor \(\delta_s\) in both height differences and cost bounds.

Suppose an old \(x\) lies strictly below \(sY\). Then \(x\in P_s\). A missed divisor outside \(B_s\) is old in \(P_s\), or has an old gate there of at least its cost. For such an old divisor \(d\) missing \(x\), the join \(x\vee d\) lies in \(P_s\), and hence \[\epsilon_d<\rho(x\vee d)-\rho(x)\leq A_s-\rho(x).\] Their supremum is at most \(A_s-\rho(x)\). Divisors inside \(B_s\) have cost at most \(\delta_s\). Equation (14) makes \(\rho(sY)-\rho(x)\) strictly larger than both bounds.

Suppose \(sY\) lies strictly below an old \(y\). Then \(h(s)\sqsubseteq y\). Every divisor of \(y\) missing \(sY\) is old outside \(P_s\), or has a gate there with at least its cost: a gate in \(P_s\) would put the divisor below all of \(B_s\). Among these old costs, those for divisors of \(h(s)\) are bounded by Equation (14). If \(y\ne h(s)\), the remaining costs have supremum strictly below \(\rho(y)-\rho(h(s))\) by the old margin. The total gap \(\rho(y)-\rho(sY)\) is the sum of two positive gaps and exceeds both cost suprema. This proves this comparison case.

Distinct comparable new blocks have an intervening old gate, so the preceding cases apply transitively. To justify this use, if \(x<z<y\), any divisor of \(y\) missing \(x\) either divides \(z\) and misses \(x\), or misses \(z\); the sum of the two positive height gaps strictly dominates both relevant suprema.

Finally, for old \(x<y\), any new divisor \(d\) of \(y\) missing \(x\) has an old gate \(g(d)\sqsubseteq y\) missing \(x\), with \(\epsilon_d\leq\epsilon_{g(d)}\). No new cost increases the old supremum, while every old divisor remains present. The supremum is therefore exactly unchanged. This also proves persistence of the margins at unions of a conservative tower of these extensions. ◻

Proof. Let \(D\) be the prescribed quotient of the copies, writing \(t_i x\) for the image of \(x\) in copy \(i\). This quotient carries one layer of the required overlaps; strings of its elements will complete that layer to a monoid. It is a right \(M\)-set and each map \(x\mapsto t_i x\) is injective. On \(D\) use the order \(z\sqsubseteq w\) when \(zq=w\) for some \(q\in M\); left cancellation and conicality inside a representing copy make this a partial order. Its right cones have conditional joins. Within one copy this is the old join. For elements represented in different copies, every common multiple must lie in their specified overlap, if there is one. In each copy join the element with the start of that overlap; transfer the two resulting elements into the overlap and join there. A missing join at any step means that the original cones are disjoint. This calculates exactly their intersection, because every common multiple must pass through both of those preliminary joins.

Adjoin generators \(l_i\) with the specified relations \(l_i a_{ij}=l_j a_{ji}\). The normal forms are \[ xz_1\cdots z_j\qquad(x\in M,\ z_i\in D), \tag{16}\] including \(j=0\). Each relation acts inside a new-generator/old-factor pair, exactly as in \(D\); it changes neither the number of new letters nor the preceding old coefficient. This proves uniqueness of the forms. Multiplication acts by the leading old coefficient of the second word on the last \(D\)-letter of the first, and then appends the remaining letters. For a fixed \(z=t_i a\), the map \(y\mapsto zy\) is injective by left cancellation in copy \(i\). Together with old left cancellation, this proves cancellation for arbitrary products of forms. Letter count proves conicality and that no new word divides an old element.

Unlike the probe extension, this construction never consumes a new letter. Its cones are therefore read from the final letter rather than from the first-letter blocks used above. For a positive-length word, right multiplication fixes the prefix before its final letter, advances that letter within its \(D\)-cone, and possibly appends further letters. More explicitly, compare \(xz_1\cdots z_p\) and \(yt_1\cdots t_q\) with \(p,q>0\). A common multiple requires \(x=y\) and equality of the letters before position \(\min(p,q)\). If \(p=q\), their intersection is obtained by joining \(z_p\) and \(t_p\) in \(D\), or is empty if that join is absent. If \(p<q\), a common multiple exists exactly when \(z_p\) divides \(t_p\) in the right \(M\)-set \(D\); then the first word divides the second and the second is their join. The case \(q<p\) is symmetric. An old \(x\) and a positive-length word with head \(y\) have a common multiple exactly when \(x\sqsubseteq y\), in which case \(x\) divides that word. Two old words use their old join, because the heads of common multiples are precisely their old common multiples. These descriptions prove conditional joins and preserve old comparisons, quotients and nonjoins. The words \(l_i x\) have exactly the identifications in \(D\), as required.

It remains to supply margins. If the number of copies is \(r\), set \[\rho_D(z)=\frac1r\sum_{i<r}\rho_i(z),\qquad \rho_i(z)= \begin{cases} \rho(x),&z=t_i x,\\ 0,&z\text{ has no representation in copy }i. \end{cases}\] Each coordinate is nondecreasing along a comparison, and some coordinate increases strictly in a proper comparison. Choose positive costs with \[\epsilon^D_z\leq\frac1r \min\bigl(\{\rho(1)/2\}\cup \{\epsilon_x:z=t_i x\text{ for some }i\}\bigr).\] For \(u<v\) in \(D\), classify a divisor \(d\) of \(v\) missing \(u\) by a copy representing \(d\). That copy also represents \(v\). If it represents \(u\), its old margin bounds the supremum of these costs strictly below its coordinate increase divided by \(r\). Otherwise that increase is at least \(\rho(1)\), while each such cost is at most \(\rho(1)/(2r)\). There are only finitely many copies, so their strict bounds still give the required strict supremum bound for \(\rho_D(v)-\rho_D(u)\).

Choose \(\theta,\phi>0\) with \(\theta+\phi<1\), and recursively set \[ \begin{split} \rho(wz)&=\rho(w)+(1-\rho(w))(\theta+\phi\rho_D(z)),\\ 0<\epsilon_{wz}&\leq (1-\rho(w))\min(\theta/2,\phi\epsilon^D_z). \end{split} \tag{17}\] For comparable new words of equal length only their last letters vary; missed divisors of that length are handled by the scaled \(D\)-margin, and all shorter divisors divide both words. For a word \(w\) compared with \(wz\), every missed divisor has the new length and prefix \(w\), so its cost is at most \((1-\rho(w))\theta/2\), strictly less than the height increase. An arbitrary comparison factors through these comparisons, and, when the lower word is old, an old comparison of leading coefficients. Transitivity of the margin, proved in Lemma 6, finishes the check. Old cost suprema are unchanged because there are no new old divisors. ◻

Proof. For the last assertion, the only nontrivial transitivity check passes through three copies. In the middle copy, intersect the two prescribed overlap starts. If their old cones are disjoint, conservativity keeps them disjoint. Otherwise their old join and its right quotients are unchanged. Every later common multiple is a multiple of that join. The two endpoint identifications at the join already agree in a valid prescription over \(B\), so right multiplication gives agreement at all later common multiples. This proves validity over \(M\). Conversely, restrict a valid prescription to \(B\). Comparisons between its old parameters have their quotients in \(B\), so no identification or transitivity witness between elements of \(B\) requires leaving \(B\). The restriction has exactly the indicated pair relations and is valid.

For probes, equality of two letters in the smaller direct limit is preserved and reflected because it is an equality at a common finite stage. If an old \(b\in B\) divides a smaller letter \([x,i]\) in the larger direct limit, there is a common stage at which \[by=x d_i\cdots d_{j-1}.\] Both endpoints of this comparison belong to \(B\), so its right factor \(y\) belongs to \(B\). Thus divisibility of a smaller letter by an old smaller multiplier, including its quotient, is unchanged. The same irreducible words therefore embed. The gate recursion uses only the previous gates and old joins and quotients, so it has the same outcome, including the absence of a gate. The join calculations in Lemma 5 now preserve and reflect joins and nonjoins.

For clarity, preservation of right quotients between new forms follows by a separate division argument. If both forms are old, use the base hypothesis. If the divisor is old and the dividend new, divide its first direct-limit letter by the preceding common-stage calculation, and retain its suffix. If both forms have the same new head, cancel that head and recurse on their suffixes. In the remaining cases the new divisor must leave its first-letter block. Factor through its gate, using the quotient in Equation (12), and divide that old gate into the dividend by the first two cases. Every factor obtained lies in the smaller extension. Left cancellation makes their product the unique required quotient.

For mergers, representation in an overlap and intersections of cones in \(D\) were calculated solely using old joins and their right quotients. These calculations are consequently unchanged. The normal forms in Equation (16) then preserve comparisons, their right factors, joins and nonjoins. This proves conservative simulation for both operations. ◻

Proof. A merger introduces no new divisor of the old \(a\). At a probe extension, a new \(x\sqsubseteq a\) has an old gate \(g(x)\sqsubseteq a\). If \(x\) also divides the old probe, its gate lies below that probe and hence below some original path element; then \(x\) does too. If \(x\) does not divide the old probe, its gate does not either. The old probe cannot divide \(x\), because it does not divide \(a\). The join calculation through the gate therefore gives \(ae\) in this case. This proves both alternatives at a successor step. At a limit every tested element has already appeared, and all comparisons and joins have been preserved. Conservativity directly preserves joins between existing probes. ◻

Proof of Theorem 4. Saturating the geometric requirements. Start with the free monoid on \(e\). For \(n<\omega\), for example, put \[\rho(e^n)=1-2^{-n-1},\qquad \epsilon_{e^n}=2^{-n-3}.\] These satisfy Equation (2). Perform \(\omega_1\) rounds. At the start of a round schedule every available probe datum \((a,b,(n_i))\) with the fixed \(e\), and every available finite valid merger. For each probe datum schedule \(\mu\) successive insertions. Execute the resulting wellordered list with the two lemmas, and take unions at limits. Lemma 8 keeps every scheduled merger valid until it is executed.

A monoid of size at most \(\mu\) has at most \(\mu^{\aleph_0}=\mu\) countable paths and at most \(\mu\) finite prescriptions. A probe extension uses a quotient of \(M\times\omega\) and finite strings; a merger uses finitely many copies and finite strings. Thus every operation preserves size at most \(\mu\), and each round has at most \(\mu\) steps. The union of \(\omega_1\) such rounds still has size at most \(\mu\). The margin lemmas ensure that old values are never changed and that old missed-cost suprema never increase, so the final union \(T\) has Equation (2) as well as all the algebraic properties.

Given an ideal in \(\downarrow_T a\), use Lemma 3 to obtain a cofinal path starting at \(1\). Its elements, \(a,b\), and all its transition and terminal quotients occur before one round: the set is countable and the rounds have cofinality \(\omega_1\). Alternatively, quotient conservativity already puts every quotient into any stage containing its endpoints. The corresponding requirement is scheduled. Its final lower closure is the given ideal, and Lemma 9 therefore gives Equation (3) for the \(\mu\) insertions. For any earlier and later insertion with the same datum, the earlier probe is old but is not a divisor of \(a\), so it is not an old divisor of the new probe. Joining through the new probe’s gate gives \(ae\). This join persists in the final union, proving independence.

Every final finite overlap prescription has its parameters in one stage. Its validity reflects to that stage by Lemma 8, and the schedule realizes it later. The realization remains exact by conservation of comparisons and quotients: equality \(l_i x=l_j y\) in a later stage must still factor through the preserved join of the two roots, with its prescribed quotients. Thus later right factors add exactly the stipulated identifications and no others. Finally use \(a=1,b=e\) and \(U=\{1\}\). Its probes have no old divisor \(e\), so there are \(\mu\) elements of \(T\setminus eT\). This proves both cardinality assertions.

Extracting a countable initial base. It remains to prove the local construction property for this same \(T\). We first select countably many operations containing any prescribed countable set of elements, and then perform all omitted operations over their union. The resulting tower must retain the gate rule: this is what will let a later descent replace a position by one born at an earlier stage. Regard the entire schedule as a continuous tower \((M_\alpha)_{\alpha\leq\lambda}\) of individual operations. Record each parameter by a finite word in previous generators. Every element of the presented monoid has such a word, and each equality has a finite derivation from the relations. This does not assert that a whole countable path has finite support.

Choose a sufficiently large regular \(\Theta\) and a countable elementary submodel \(N\) of \(H_\Theta\) containing the tower, its presentations and an enumeration of the prescribed countable subset of \(T\). Countable objects in \(N\), in particular the parameter paths of operations indexed in \(N\), have all their entries in \(N\). First perform just the operations whose indices belong to \(N\), in their original order. Let \(S_\alpha\) denote this subconstruction using selected indices below the cut \(\alpha\).

At cuts \(\alpha\in N\) we have \[ S_\alpha=M_\alpha\cap N, \tag{18}\] with a conservative inclusion in \(M_\alpha\). Here is the induction justifying the assertion. Old comparisons, their quotients and joins in an elementary intersection are reflected by elementarity; a nonjoin remains a nonjoin in the larger monoid. Before a selected operation, every parameter is already present: its finite term code belongs to \(N\), and all entries of a countable path in \(N\) belong to \(N\). Conservative simulation makes that operation legal in the subconstruction and embeds its result. Conversely, every element of \(M_\alpha\cap N\) has by elementarity a finite term code in \(N\); all of its finitely many generator indices belong to \(N\) and precede \(\alpha\). It is therefore produced by the selected subconstruction. This proves Equation (18) and the successor step of the induction. At a cut \(\alpha\notin N\), fix the finitely many words in a comparison or join test. If they use selected operation indices, let \(\gamma\) be the greatest such index and put \(\beta=\gamma+1\); if there are no such indices, put \(\beta=0\). Then \(\beta\in N\), \(\beta<\alpha\), and all the words belong to \(S_\beta=M_\beta\cap N\). The original inclusion \(M_\beta\subseteq M_\alpha\) is conservative. Any right quotient or conditional join required by the test therefore already lies in \(M_\beta\) and, by elementarity, in \(N\), hence in \(S_\beta\). This also preserves nonjoins and proves conservation at \(\alpha\). Unions introduce no additional finite relation. This completes the induction.

The resulting selected submonoid \(T_0\) is countable: the initial monoid is countable, there are countably many selected steps, and each operation over a countable base adds only countably many elements. It contains the prescribed sequence by its finite term codes. The set of selected indices need not be an initial segment; the argument has used Equation (18) only at cuts belonging to \(N\).

Reinserting the omitted operations. Append now the omitted steps in their original order. Before an omitted step \(\alpha\), the current presentation is the union of the original relations below \(\alpha\) and all selected relations. It has an alternative realization: start with \(M_\alpha\), and then perform the selected steps at indices at least \(\alpha\) in their order. Indeed \(S_\alpha\subseteq M_\alpha\) is conservative, and repeatedly simulating the selected subconstruction makes all these operations legal. Each extends its whole base conservatively, so this alternative realization conservatively contains \(M_\alpha\). It has precisely the same generators and relations as the current reordered presentation. Consequently the original operation at \(\alpha\) is legal over the current base, by conservative simulation again. Induction validates every appended step. At limits the presentations are their unions; at the end their union is exactly the original presentation of \(T\).

Each step of this reordered tower is one of the two operations. The merger has no new old divisors, and the probe extension has its least-old-multiple rule, including Equation (4). Conservation allows those comparisons to be tested in \(T\). This proves the last assertion and completes the theorem. ◻

Proof. If \(m\) is not in that submonoid, take its first birth step in the reordered tower. It has the old multiple \(n_N\), so this is a probe step and its gate satisfies \(g(m)\sqsubseteq n_N\). Choose an admissible replacement with \(n_N\sqsubseteq md\). The quotient \(d\) belongs to the initial submonoid and is therefore old at this step. Conservation and Equation (4) imply that \(md\) belongs to the strictly earlier base. Repeat if necessary. Each repetition strictly lowers the birth ordinal, so the process terminates after finitely many repetitions. The resulting position lies in the countable initial submonoid. ◻

Proof. A descending countable sequence has its union as a lower bound. Deciding the entries of a name for a sequence in a ground set and then taking such a lower bound shows that no new countable sequence in that set is added. This also preserves \(\omega_1^V\).

We recall the relevant delta-system argument to identify the exact cardinal bound. A family of \(\mu\) countable sets has a delta-system subfamily of size \(\mu\). Code its union into \(\mu\), and write its members as \(S_\alpha\subseteq\mu\), for \(\alpha<\mu\). There is a club of \(\delta<\mu\) such that \(S_\alpha\subseteq\delta\) whenever \(\alpha<\delta\). On the stationary part of this club of cofinality \(\omega_1\), each \(S_\alpha\cap\alpha\) is bounded in \(\alpha\). The pressing-down lemma makes a bound constant, say \(\gamma<\mu\), on a stationary subset. There are at most \(|\gamma|^{\aleph_0}+\aleph_0<\mu\) possible countable subsets of \(\gamma\), by Equation (19) and its preceding bound. Regularity of \(\mu\) therefore makes \(S_\alpha\cap\alpha\) one fixed set on a stationary subset. For \(\alpha<\beta\) in that subset, \(S_\alpha\subseteq\beta\), so their intersection is this fixed root.

Apply this to the domains of \(\mu\) Cohen conditions. There are at most \(2^{\aleph_0}=\mathfrak c<\mu\) assignments on the countable root. Thinning once more gives two, indeed \(\mu\), conditions agreeing on the root. They are compatible, which proves the chain condition. The usual antichain bound then preserves all cardinals at least \(\mu\): the possible values at any one coordinate of a name for an ordinal-valued function are covered by fewer than \(\mu\) ground ordinals, and regularity handles the case of \(\mu\) itself. Countable closure and the chain condition together preserve all cardinals when \(\mu=\aleph_2\). In a general ground we assert no preservation of cardinals strictly between \(\kappa\) and \(\mu\).

Finally, any sequence of ground elements has its values in some ground rank segment: their ranks have an ordinal bound, and forcing preserves ordinals. Thus the assertion about sequences in ground sets covers all countable sequences of ground elements. ◻

Proof. The probes from Theorem 4 for \(a=1,b=e,U=\{1\}\) give \(\mu\) distinct elements \(m\) with \(me=e\). None belongs to \(eT\): if \(m=ex\), left cancellation would give \(xe=1\), contrary to conicality and \(e\neq1\). Hence \(|T\setminus eT|=\mu\). Define \(r(ex)=p(x)\), using left cancellation, and fill the complement injectively in \(I\setminus D_p\), including \(J\setminus D_p\). Both the size of that complement in \(T\) and the strict inequality \(\mu<|I|\) give the first assertion.

For the second assertion, identify the copies of \(T\) exactly where their labels in \(I\) coincide. The hypothesis says that these identifications have the form required by the finite-merger property; their transitivity and absence of collapse within a copy follow from actual equality of labels. Let \(l_i\in T\) realize this merger. On \(\bigcup_i l_iT\), assign \(l_ix\) the value \(s_i(x)\). The exact-overlap property makes this well defined and injective. Extend it injectively to the rest of \(T\). The resulting \(r\) satisfies \(r_{l_i}=s_i\).

For the last assertion, the prescribed domain and range each have size at most \(\mu\). Their complements in \(I\) both have cardinality \(\mu^+\), so a bijection between the complements extends the partial bijection to a permutation. Fresh images can first be chosen off the excluded set, whose size is still at most \(\mu\), and then the same argument applies. All these choices occur in \(V\). ◻

Proof. Apply the set-forcing symmetric-extension theorem (Karagila 2026a, sec. 2.1, p. 4) to \(\mathbb Q\), \(G\), and the normal subgroup filter verified above. Its internal formulation concerns all hereditarily symmetric names and yields the full Separation and Replacement schemata, as well as Foundation; this formulation is recalled in Lemma 34. It requires no countable-completeness assumption on the filter. External transitivity of \(V\) permits the usual recursive name evaluation and gives the displayed literal inclusions. For an arbitrary countable ground, Lemma 35 instead gives truth in the membership-closed symmetric quotient; it makes no assertion of external well-foundedness. ◻

Proof. If the first assertion fails, there are \(s_0,s_1\leq p\) forcing contrary answers in \(V[F]\). Choose \(d_0,d_1\in F\) witnessing those answers in the factorized forcing relation. Their restrictions to \(D_p\times\kappa\) are compatible. By Lemma 12, choose \(\pi\in\mathop{\mathrm{Fix}}(D_p)\) so that, outside \(D_p\), the coordinates of \(s_1,d_1\) move away from those of \(s_0,d_0\). The diagrams \(s_0,\pi s_1\) meet exactly in their common subdiagram \(p\), so have a common extension. The conditions \(d_0,\pi d_1\) agree on the root and have disjoint supports off it, so are compatible. All parameter names are fixed by \(\pi\). Equation (20) now gives two contrary assertions forced by compatible product conditions, a contradiction. This argument does not assert that \(\pi d_1\) belongs to \(F\).

For the second assertion, put \(\delta=d\restriction D_s\). If \(\delta\) does not force the indicated factorized assertion, there is \(c\leq\delta\) forcing its negation. Choose \(\pi\in\mathop{\mathrm{Fix}}(D_s)\) moving \(\mathop{\mathrm{supp}}_I(d)\setminus D_s\) off \(\mathop{\mathrm{supp}}_I(c)\setminus D_s\). The condition \(\pi d\) is compatible with \(c\). It forces the original factorized assertion, by product symmetry, because \(s\) and all its parameter names are fixed. This contradicts the assertion forced by \(c\). ◻

Proof. Take \(d\in F\) witnessing the equality forced at \(v\). Both parameter supports lie in \(D_v\), so Lemma 14 allows us to replace \(d\) by \(d\restriction D_v\). Set \(\delta=d\restriction D_{s_0}\). We will combine the translates of \(\sigma_0\) into one \(D_p\)-supported name. A translate contributes its value only when the generic contains the corresponding translate of \((\delta,s_0)\); the value of the new name will be the union of these contributing values. Thus the main task is to prove that any two contributing copies agree. For this coherence argument, allow both factors of the product generic to vary. We will return to the fixed \(F\) after constructing the name.

For every \(\pi\in\mathop{\mathrm{Fix}}(D_p)\), call the copy \(\pi\sigma_0\) active when its trigger \((\pi\delta,\pi s_0)\) belongs to the product generic. We first prove that any two active copies have equal values.

Consider two copies whose diagrams \(\bar s,\bar s'\) have intersection exactly \(D_p\). If they can be unequal while active, some product condition \((c,t)\) extends both triggers and forces the inequality. Place a copy \(u\) of \(s_1\) over \(p\), with the rest of its range fresh relative to \(D_t\cup\mathop{\mathrm{supp}}_I(c)\). Extend the respective placements of \((s_0,s_1)\) onto \((\bar s,u)\) and \((\bar s',u)\) to placements of \(v\), producing diagrams \(v',v''\). Use the same placement on all of \(D_{s_1}\) in both cases. Choose all remaining coordinates freshly, so that the ranges have the intersections shown in Figure 2: \[ \begin{aligned} D_{v'}\cap D_t&=D_{\bar s},& D_{v''}\cap D_t&=D_{\bar s'},& D_{v'}\cap D_{v''}&=D_u . \end{aligned} \tag{21}\]

Every intersection in this display is its indicated common subdiagram. The required partial maps agree on the root, and their domain and range sizes are at most \(\mu\); Lemma 12 therefore supplies the ground permutations realizing these placements.

The two placed copies of \(d\) agree on \(D_u\). They agree with \(c\) on \(D_{\bar s}\) and \(D_{\bar s'}\), respectively, because \(c\) extends the two placed copies of \(\delta\). On the remaining coordinates freshness gives compatibility. Thus the Cohen conditions have a common extension. The three diagrams \(v',v'',t\) also have a common extension by Equation (21) and finite amalgamation. The two transported \(\sigma_1\) names are literally equal, since the placements agree on the entire \(D_{s_1}\). The equalities transported from \((d,v)\) therefore contradict the inequality forced by \((c,t)\).

For two active copies with arbitrary overlap, start again with any proposed inequality-forcing common extension \((c,t)\). Place a third copy of \(s_0\) over \(p\), independent of \(t\) off the root, and place its Cohen trigger compatibly with \(c\). It has a common product extension with \((c,t)\). The independent case just proved applies between this third copy and each of the original ones, contradicting the inequality. This proves coherence of all active copies, below every possible inequality witness.

Define a mixture using all joint strengthenings: \[ \sigma= \left\{(\pi\eta,(c,t)): \begin{array}{l} \pi\in\mathop{\mathrm{Fix}}(D_p),\quad (\eta,(a,u))\in\sigma_0,\\ (c,t)\leq(\pi\delta,\pi s_0),\quad (c,t)\leq(\pi a,\pi u) \end{array}\right\}. \tag{22}\] This is a set name. Left multiplication in \(\mathop{\mathrm{Fix}}(D_p)\) permutes its entries, so it is supported by \(D_p\). Its member names are translates of member names of \(\sigma_0\) and hence are \(\mathrm{HS}\). In any product generic its value is the union of the values of the active copies. Both inclusions in this description follow from directedness of the generic: all common strengthenings, rather than a selected one, occur in Equation (22). When the original trigger is active, coherence makes this union exactly the value of \(\sigma_0\). Return now to the fixed \(F\). Since \(\delta\in F\), the original trigger is active in every product generic with this Cohen factor and with \(s_0\) in its diagram filter. It follows that \(s_0\Vdash_{\mathbb P}\sigma[F]=\sigma_0[F]\). The equality with \(\sigma_1[F]\) holds below \(v\). Its parameters are supported by \(D_{s_1}\), so Lemma 14 makes it hold already below \(s_1\).

No step imposed a rank bound. For the subset assertion, replace the mixture by its intersection with \(A\), using the normalization in the next paragraph. ◻

Proof. Let \(\sigma\) be a ground \(\mathrm{HS}\) name, and let \(p\) have \(D_p\) as a support for \(\sigma\). Form the graph name \[ \dot h_{\sigma,p}= \left\{\left( \operatorname{op}(\dot A_{\pi(p(1))},\pi\sigma), (1_{\mathbb R},\pi p)\right):\pi\in G\right\}, \tag{24}\] where \(\operatorname{op}\) denotes the canonical ordered-pair name. This name is invariant, and all its member names are \(\mathrm{HS}\).

Its value is a partial function on \(A\). Indeed, suppose two contributing pairs have equal first coordinates. Label distinctness gives \(\pi(p(1))=\rho(p(1))\). There is a common extension \(r\in H\) of \(\pi p,\rho p\); write \(\pi p=r_n\) and \(\rho p=r_m\). The equality of centers and injectivity of \(r\) give \(n=m\). Consequently \(\pi p=\rho p\) pointwise, so \(\rho^{-1}\pi\in\mathop{\mathrm{Fix}}(D_p)\). It fixes \(\sigma\), and hence \(\pi\sigma=\rho\sigma\) literally. The two values therefore agree. This argument concerns names under compatible diagram conditions, not an action on one fixed symmetric model.

The orbit construction gives invariant partial functions. We now form a set-indexed family of them whose ranges cover \(X\). Choose an \(\mathrm{HS}\) name \(\tau\) for \(X\). The set \(M\) of member names appearing in \(\tau\) is a ground set of \(\mathrm{HS}\) names. In \(V\), enumerate by an ordinal \(\eta\) the set \[B=\{(\sigma,p)\in M\times\mathbb P: \mathop{\mathrm{Fix}}(D_p)\text{ fixes }\sigma\}.\] Every member name has a support of size at most \(\mu\), and Lemma 12 provides supporting diagrams. We include all such diagrams, because one chosen diagram need not belong to the generic filter. The corresponding sequence of graph names \(\dot h_{\sigma,p}\) is a ground sequence of invariant \(\mathrm{HS}\) names. Its canonical sequence name is itself invariant and \(\mathrm{HS}\), so its interpretation \(\langle h_i:i<\eta\rangle\) belongs to \(W\).

These partial functions cover \(X\). For \(x\in X\), an active member name \(\sigma\) of \(\tau\) has value \(x\). The set of diagrams whose ranges contain a fixed support of \(\sigma\) is ground dense, by Lemma 12. Thus some such \(p\) belongs to \(H\). The identity entry of \(\dot h_{\sigma,p}\) maps \(A_{p(1)}\) to \(x\).

All remaining definitions take place in \(W\). For nonempty \(X\), fix one \(x_0\in X\), and define \[h(a,i)= \begin{cases} h_i(a),&a\in\mathop{\mathrm{dom}}(h_i)\text{ and }h_i(a)\in X,\\ x_0,&\text{otherwise}. \end{cases}\] Separation and Replacement form this function on \(A\times\eta\), and coverage makes it surjective. The one default element uses only nonemptiness of \(X\). The enumeration above is over \(M\times\mathbb P\), a set depending on the particular name \(\tau\); no restriction to names below a fixed rank was made. ◻

Proof. We first treat a family \(\langle X_\xi:\xi<\eta\rangle\) of nonempty subsets of \(A\). Start below a product condition \((d_0,p)\) forcing this assertion for an \(\mathrm{HS}\) family name. By extending the diagram, arrange that \(D_p\) contains its support and \(\mathop{\mathrm{supp}}_I(d_0)\). The assertions that a given graph is a function and has nonempty subset values are absolute between \(W\) and the full extension. Consequently this use of ordinary forcing follows equally from a symmetric-forcing hypothesis. Names for the individual \(X_\xi\) can be obtained by the membership forcing relation from the family and \(\check\xi\); they retain support \(D_p\). Choose once and for all \(q\) with \(q_e=p\). This same \(q\) will work for every family index. Witnesses already available on \(p\) need no move; for witnesses on proper extensions of \(p\), the probes place independent copies inside \(q\) and Cohen genericity activates one of them.

Fix \(F\) containing \(d_0\), and fix \(\xi<\eta\). In \(V[F]\), some \(t\leq p\) and \(j\in I\) satisfy \[t\Vdash_{\mathbb P} A_j\in X_\xi.\] This follows by deciding a witness in the ground index set \(I\) for membership in \(A\). Extend \(t\) to include \(j\) in its range, and write \(p=t_b\). Choose \(d\in F\) witnessing the displayed forcing assertion, and restrict it to \(D_t\) by Lemma 14. If \(b=1\), then \(t=p\), so \(q\) already forces a witness whose index belongs to \(D_q\).

Suppose \(b\neq1\). The probes of Theorem 4, with \(a=1,U=\{1\}\), give \(\mu\) elements \(m\) satisfying \(mb=e\) and \(mT\cap m'T=eT\) for distinct probes. Thus \[(q_m)_b=p,\qquad D_{q_m}\cap D_{q_{m'}}=D_p\quad(m\neq m').\] Each \(q_m\) is a copy of \(t\) over \(p\). Choose in \(V\) a permutation \(\pi_m\in\mathop{\mathrm{Fix}}(D_p)\) taking \(t\) to \(q_m\). The conditions \(\pi_m d\) all restrict on \(D_p\) to \(d_*=d\restriction D_p\), and their coordinate supports off that root are pairwise disjoint.

For these fixed ground data, the set \[ \{c:c\perp d_*\}\ \cup\ \{c:(\exists m)\ c\leq\pi_m d\} \tag{25}\] is dense in \(\mathbb R\). Given \(c\) compatible with \(d_*\), first extend it by \(d_*\). Its support is countable, so it meets the nonroot support of only countably many of the pairwise disjoint copies. Choose a remaining probe and extend \(c\) by its placed condition \(\pi_m d\). This proves density. Because \(d_*\in F\), the generic meets the second alternative of Equation (25). For the resulting \(m\), product symmetry and \(\pi_m X_\xi=X_\xi\) give \[q_m\Vdash_{\mathbb P} A_{\pi_mj}\in X_\xi \quad\text{in }V[F].\] Since \(q\leq q_m\) and \(\pi_mj\in D_q\), this supplies the required witness in \(A[D_q]=\{A_j:j\in D_q\}\).

The condition \(q\) was chosen before \(\xi\). Although \(t,d,j\) were chosen in the argument after \(F\), each is an individual ground object. The dense set in Equation (25) therefore belongs to \(V\), and \(F\) meets it. No sequence of witnesses for all \(\xi\) is being selected or imported into \(W\). For each \(\xi<\eta\) the argument shows that \(q\) forces \(X_\xi\cap A[D_q]\neq\varnothing\) in \(V[F]\). It forces the universal statement as well: a condition forcing a counterexample could be strengthened to decide its index in \(\check\eta\) to one ground \(\xi\), contradicting the assertion for that index. Since this holds for every \(F\) containing \(d_0\), the product condition \((d_0,q)\) forces the universal meeting property.

A ground enumeration of \(D_q\) yields a sequence of its labels with an \(\mathrm{HS}\) name supported by \(D_q\). Distinctness of labels turns that enumeration into a wellordering of \(A[D_q]\) in \(W\). Taking the first element of each \(X_\xi\) in this wellordering defines the required choice function by Replacement in \(W\). The argument works below an extension of every starting condition forcing the subset-family hypothesis, and hence proves choice for all such families in \(W\).

Finally let \(\langle Y_\xi:\xi<\eta\rangle\) be any family of nonempty sets in \(W\). For \(\eta=0\) use the empty function. Otherwise Proposition 16, applied once to the union of the family, gives a surjection \(h:A\times\theta\to\bigcup_{\xi<\eta}Y_\xi\) in \(W\). For each \(\xi\), take the least \(\alpha_\xi<\theta\) whose slice meets \(Y_\xi\), and form \[B_\xi=\{a\in A:h(a,\alpha_\xi)\in Y_\xi\}.\] These are a family of nonempty subsets of \(A\) in \(W\). The subset case chooses \(a_\xi\in B_\xi\); then \(h(a_\xi,\alpha_\xi)\) is the desired choice from \(Y_\xi\). ◻

Proof. Suppose an \(\mathrm{HS}\) name is forced to be a function from an ordinal \(\eta\) onto \(A\). Choose a forcing condition \((d,p)\) whose diagram range contains the name’s support and \(\mathop{\mathrm{supp}}_I(d)\). Fix \(j\notin D_p\), which exists since \(|D_p|^V=\mu<|I|^V\). Strengthen to a product condition \((c,t)\) deciding a ground \(\beta<\eta\) with value \(A_j\), and extend the diagram further to have \(j\in D_t\).

Choose \(\pi\in\mathop{\mathrm{Fix}}(D_p)\) moving all coordinates of \(t,c\) outside \(D_p\) to fresh ones. Then \(t,\pi t\) are independent over \(p\) and have a common extension; \(c,\pi c\) are also compatible. The function name and \(\check\beta\) are fixed. Their common product extension would therefore force that one entry has both values \(A_j\) and \(A_{\pi j}\). They are distinct because \(j\notin D_p\) and \(\pi\) moved it freshly. This is a contradiction. ◻

Proof. Choose a product \(\mathrm{HS}\) name \(\tau\) for \(f\). In \(V[F]\), the ordinary \(\mathbb P\)-truth lemma supplies a condition in \(H\) forcing that \(\tau[F]\) is a function \(\check\omega\to\check X\). Extend within \(H\) to a diagram \(p\) whose range covers a support of \(\tau\). For each \(n<\omega\), the ordinary forcing theorem supplies an extension of \(p\) and some \(x\in X\) forcing \(\tau[F](n)=\check x\). Both \(\tau\) and the check-name parameters are supported by \(D_p\), so Lemma 14 makes \(p\) itself force that equality. There is exactly one such \(x\), since \(p\) forces functionhood.

The forcing relation is definable in \(V[F]\). Replacement there therefore forms the sequence of these unique values, a function \(g:\omega\to X\) in \(V[F]\). Then \(g=f\) in \(V[F][H]\), because \(p\in H\). By Lemma 11, \(\mathbb R\) adds no countable sequences in the ground set \(X\), so \(g\in V\). Thus \(f\in V\). The final assertion follows by bounding the ranks of the entries of any countable sequence of ground elements, as in the proof of Lemma 11. ◻

Proof. For an element choose a representative \(\tau\) and a diagram \(t\le r\) forcing \(\tau=[\dot A_j]_E\) for some \(j\in D_t\). The ordinary forcing theorem permits deciding a representative label; extending the diagram includes its index. Write \(r=t_b\). By Cohen restriction in Lemma 14, there is \(d\in F\), supported in \(D_t\), witnessing this \(\mathbb P\)-forcing assertion. Record the triple \[(b,x,t^{-1}d),\qquad t(x)=j,\] where \(t^{-1}d\) is the partial binary function on \(T\times\kappa\) obtained by replacing each coordinate \(t(y)\) with \(y\). Its domain has size less than \(\kappa\). The ground set of possible records has size at most \(\mu\), since \(|T|=\mu\), \(\kappa\le\mu\), and \(\mu^{<\kappa}=\mu\). Its ground enumeration remains an enumeration in \(V[F]\).

Suppose two chosen representatives \(\tau_1,\tau_2\) have the same record, witnessed by \(t_1,t_2,d_1,d_2,j_1,j_2\). The ground bijection \(t_1(y)\mapsto t_2(y)\) agrees with the identity on \(D_r\): in both diagrams \(r=(t_i)_b\). It maps points outside \(D_r\) to points outside \(D_r\). Extend it to a ground permutation \(\pi\) of \(I\) fixing \(D_r\). This is possible since the two ranges have size \(\mu<|I|\) and their complements have the same cardinality \(|I|\). Then \[\pi t_1=t_2,\qquad \pi d_1=d_2,\qquad \pi j_1=j_2, \qquad \pi\tau_1=\tau_1.\] Product symmetry makes \(d_2\) witness at \(t_2\) equality of both \(\tau_1\) and \(\tau_2\) with \([\dot A_{j_2}]_E\). Since \(d_2\in F\), \(t_2\) forces \(\tau_1=\tau_2\) in \(V[F]\). Decision at \(r\) gives the same equality there. Thus distinct elements have distinct records. Choosing representatives and records uses Choice in the ordinary extension \(V[F]\), not in the symmetric model. ◻

Proof. Both sets contain \(1\) and are downward closed by inclusion of subdiagrams. Suppose \(n,n'\in U_h\) and put \(k=n\vee n'\). The ranges of \(r_n,r_{n'}\) intersect exactly in \(D_{r_k}\). Choose supported names for their representations of \(h\). They are forced equal by \(r\). Lemma 15, with root \(r_k\), supplies a \(D_{r_k}\)-supported name equal to them. Normalize it without changing support. Decision at \(r_k\) shows it is an \(E\)-class there: its negation would persist to the extension \(r\). Thus \(k\in U_h\). For labels the identical argument is the literal equality of cone intersections, without any name descent.

For the final assertion, apply Lemma 3 in \(V[F]\). The ground monoid, order, heights and costs retain their meanings there, so every nonempty ideal has a countable cofinal sequence. It consists of ground elements of \(T\), so countable closure of \(\mathbb R\) puts it in \(V\). Its downward closure, computed with the unchanged ground order, is the original ideal. The argument applies to every ideal in \(V[F]\), not only to ground ideals. ◻

Proof. The common root \(p\) will separate the copies used in this proof. We first find a class with no representation supported by \(D_p\). Copying it into diagrams whose unwanted intersections are exactly \(D_p\) will then rule out both coincidences between copies and availability at forbidden subdiagrams, by support descent.

A class unavailable at the root. Enumerate \(\mathcal X(p)\) in \(V\) as \((\tau_\xi:\xi<\lambda)\). The canonical name for the sequence of its evaluations is hereditarily symmetric with support \(D_p\). Explicitly, its entries are the canonical pairs \((\check\xi,\tau_\xi)\), each placed under every product condition. Every member of \(\mathop{\mathrm{Fix}}(D_p)\) fixes each entry literally. The range of this sequence is wellorderable inside \(W\): map each value to its least index of occurrence. If it contained every \(E\)-class, the same map restricted to \(A/E\) would wellorder that quotient. The hypothesis therefore implies, ordinarily below \((d_0,p)\), that some \(E\)-class lies outside the evaluations of all names in \(\mathcal X(p)\).

Fix \(F\) containing \(d_0\). By the ordinary forcing theorem choose \(t\le p\) and \(j\in D_t\) such that \(t\) forces the class of \(A_j\) outside that entire evaluation list. Choose a witnessing Cohen condition \(d\in F\) supported in \(D_t\), using Lemma 14. Write \(p=t_b\). Necessarily \(b\ne1\), since a class represented by a label in \(D_p\) has a name in \(\mathcal X(p)\).

Independent copies with active Cohen conditions. As \(p=r_{ae}\), the probe property of Theorem 4 supplies \(\mu\) elements \(m\) with \(mb=ae\) and the prescribed ideal \(U\). The diagrams \(r_m\) are copies of \(t\) over \(p\), with pairwise intersection exactly \(D_p\). Choose the ground permutations taking \(t\) to these diagrams and fixing \(D_p\), and transport \(d\) and the class name along them. Their nonroot coordinate sets are disjoint. This is the role of the earlier extension \(q_e=p\): the availability pattern is prescribed among divisors of \(a\), while the common root lies at \(ae\), strictly beyond \(a\).

There are \(\mu\) copies whose transported Cohen conditions belong to \(F\). To see this without any \(\mu\)-closure assertion, partition the ground family into \(\mu\) ground subfamilies of size \(\mu\). In each subfamily the conditions extending at least one transported copy of \(d\) form a dense set below \(d\restriction D_p\). Indeed, a Cohen condition uses countably many coordinate indices; among the pairwise disjoint nonroot ranges there is one it misses, and on the root the two conditions agree. Their union is a Cohen condition. Genericity meets each of these ground dense sets. A hit in each disjoint subfamily yields \(\mu\) different hits.

Distinct classes with the prescribed exact ideal. Each hit gives a \(D_{r_m}\)-supported class name forced at \(r_m\) to lie outside the evaluations of \(\mathcal X(p)\). The diagram \(r_m\) extends \(p\) but need not extend \(q\); we use its class name, not a set \(\mathcal D_F(r_m)\). As \(r\) extends \(r_m\), this name represents a symbolic class in the defined set \(\mathcal D_F(r)\). Two such classes cannot be equal there: support descent over their common root \(p\) would supply a name in \(\mathcal X(p)\) for their common value, contrary to the outside assertion. If \(n\in U\), then \(n\sqsubseteq m\), so \(r_n\) extends \(r_m\) and the class is available at \(r_n\). If \(n\sqsubseteq a\) and \(n\notin U\), the exact probe intersection gives \[nT\cap mT=aeT, \qquad D_{r_n}\cap D_{r_m}=D_p.\] Availability at \(r_n\) would again descend to a name in \(\mathcal X(p)\), a contradiction. Its exact availability ideal is therefore \(U\). This gives \(\mu\) distinct elements of \(B_{r,U}(F)\); Lemma 20 bounds that fiber from above.

The label fiber. For labels use the probe centers \(r(m)\). Their availability ideals are exactly \(\downarrow m\cap\downarrow a=U\), and distinct probes have distinct centers. This supplies a ground \(\mu\)-subset of \(L_{r,U}\); the upper bound follows from \(|D_r|=\mu\). ◻

Proof. Let \(v=(r,U)\), \(w=(r_n,U_n)\), and first take a symbolic class available at \(r_n\). Its full availability ideal \(J\) at \(r\) contains \(n\). For \(z\sqsubseteq a\), ideal closure gives \[z\in J\quad\Longleftrightarrow\quad z\vee n\in J.\] Write \(z\vee n=nx\). Availability at \(r_{z\vee n}\) is exactly the corresponding availability at the subdiagram \((r_n)_x\) of \(r_n\). Thus the restricted ideal at \(r_n\) determines the full ideal at \(r\). If that restricted ideal is \(U_n\), the last test is equivalent to \(z\vee n\in U\), and hence to \(z\in U\). Conversely, an element of \(B_v(F)\) is available at \(r_n\) because \(n\in U\), and its restricted ideal is \(U_n\). This proves surjectivity; injectivity follows from Equation (26). For labels use the same argument with literal membership in ranges. Commutation follows because all the symbolic maps retain the same representative names. ◻

Proof. Choose the countable-base tower of Theorem 4 so that its initial submonoid \(T_0\) contains all \(n_i\) and all right quotients between them. For \(\pi\in G_C\), consider its alignments with contractions of the chosen vertex: \[\mathcal A_\pi= \{(l,m)\in\omega\times U:\pi r_{n_l}=r_m\}.\] This set is nonempty: the moved chain is cofinal in \(C\), so one of its terms is a successor of \(v_0\). Every second coordinate \(m\) of an alignment divides some \(n_N\), by cofinality of \((n_i)\) in \(U\).

To apply Lemma 10, fix \((l,m)\in\mathcal A_\pi\) and any \(N\). Choose \(l'\ge l\) so that \(\pi v_{l'}\) is a successor of \(v_N\). Its diagram is \(r_k\) for some \(k\in U\) with \(n_N\sqsubseteq k\). Let \(d\in T_0\) be the right quotient \(n_ld=n_{l'}\). Then \[r_k=\pi r_{n_{l'}}=(\pi r_{n_l})_d=r_{md}.\] Injectivity of \(r\) gives \(k=md\). Consequently \(md\in U\), \(n_N\sqsubseteq md\), and \((l',md)\in\mathcal A_\pi\). These are exactly the replacement hypotheses of Lemma 10. Its conclusion supplies an alignment \((l,m)\) with \(m\in T_0\).

There are countably many resulting alignment pairs \((l,m)\in\omega\times T_0\). Two permutations giving the same pair agree pointwise on \(D_{r_{n_l}}\); if they are \(\pi\) and \(\rho\), then \(\pi^{-1}\rho\in\mathop{\mathrm{Fix}}(D_{r_{n_l}})\subseteq K_C\). Enumerate the pairs, and assign to each coset the first pair realized by any of its members. Distinct cosets receive distinct pairs. This proves the bound. ◻

Proof. Choose \(N\) such that \(k\) fixes \(D_{r_{n_N}}\) pointwise. For \(i\ge N\) it fixes \(r_{n_i}\) and every name in \(\mathcal X(r_{n_i})\) literally. Consequently each particular ground code \(c\) represents \(b\) at \(F\) if and only if the same code represents \(T_k^F(b)\) at \(kF\). The forcing symmetry lemma proves this on the tail; the definition ignores the remaining finite prefix. Thus the sets of functioning codes are identical, and their minima under the fixed ground wellorder are identical. This proves the order assertion. Also \(L_C\subseteq D_{r_{n_i}}\) for every \(i\), so \(k\) fixes its every member. ◻

Proof. If \(k\in K_C\), it fixes all \(s_{\delta,i}\) once \(i\) is sufficiently large. Replacing \(\pi\) with \(\pi k\) therefore changes each detector sequence in only finitely many places, proving representative independence.

Suppose \(\pi K_C\ne\pi'K_C\). Use the detector for \(\delta=(\pi^{-1}\pi')K_C\) and write \(\pi^{-1}\pi'=\gamma_\delta k\) with \(k\in K_C\). Eventually \(k(s_{\delta,i})=s_{\delta,i}\), and hence \[\pi(s_{\delta,i})\ne\pi'(s_{\delta,i}).\] Distinct label indices give distinct Cohen rows. For each of these tail positions choose a bit where the two rows differ. The countably many bit ordinals are bounded below regular \(\kappa\). Above that bound the two restricted sequences disagree at every position on a tail, so are unequal modulo eventual equality. There are countably many pairs of cosets; a further countable supremum supplies one bound that distinguishes all pairs. These choices take place in \(V[F]\). They use regularity of \(\kappa\), not closure of \(\mathbb P\).

At the least distinguishing \(\alpha\), choose the coset whose pattern is least in the fixed ground wellorder. If \(\Gamma_C\) is trivial, choose its sole element and use \(\alpha=0\). For \(\sigma\in G_C\), label transport gives, for every \(s\in I\), \(A_{\sigma s}^{\sigma F}=A_s^F\). Thus \[ P_{\sigma F}^\alpha((\sigma\pi)K_C) =P_F^\alpha(\pi K_C). \tag{35}\] The actual ground pattern objects on the two sides are equal. Left multiplication permutes the coset set, so the least distinguishing bound is unchanged and the same pattern object is minimal. This proves Equation (34). ◻

Proof. We first finish the construction for the equivalence relation fixed at the start of Section 4. Use canonical equivariant ordered-pair names and form the product name \[ \dot J= \left\{ \left(\langle\dot A_j,\tau\rangle^{\bullet},(d,r)\right): \begin{array}{l} r\le q,\ j\in D_r,\ \tau\in\mathcal X(r),\ d\le d_0,\\ d\Vdash_{\mathbb R}\Phi(\dot F,r,j,\tau) \end{array}\right\}. \tag{40}\] The superscript denotes the name for the ordered pair. This is a set name: every index ranges over a ground set and the defining forcing relation is a ground relation. Equation (39) sends each entry under \(\pi\in G_q\) to another entry. Applying \(\pi^{-1}\) gives equality of the sets of entries, so \(G_q\) fixes \(\dot J\) literally. Each member name is a pair of HS names; thus \(\dot J\) is HS with support \(D_q\). The individual member names may have different supports. Hereditary symmetry does not require all of them to use \(D_q\).

Take a product generic \((F,H)\) containing \((d_0,q)\). For every \(r\in H\) below \(q\), the graph contains exactly the local assignments of Equation (37). In detail, whenever \(\Phi(F,r,j,\tau)\) holds, the \(\mathbb R\) truth lemma gives a condition of \(F\) forcing it; strengthening with \(d_0\) retains a condition of \(F\), and Equation (40) includes its entry. Conversely, every active entry forces its asserted assignment. All classes are represented by names in their symbolic equivalence classes, so the local assignments are complete.

We check the comparison when the diagram is strengthened. Suppose \(t\le r\le q\), \(r=t_b\), and \(j\in D_r\). The availability ideal of \(j\) at \(t\) contains \(b\). Hence \[(t,U_j\text{ computed at }t) \longrightarrow(r,U_j\text{ computed at }r)\] is a contraction. Equation (37) therefore gives the same assigned symbolic element under inclusion. In particular, its product-name evaluations are equal in every \(\mathbb P\)-generic containing \(t\).

Any two active entries of \(\dot J\) occur together below a common stronger diagram in \(H\). At that diagram the union of the exact-fiber bijections is a bijection \(D_t\to\mathcal D_F(t)\): availability ideals partition both sets. The preceding comparison proves single-valuedness and injectivity of \(\dot J^{F,H}\). Distinct symbolic elements are forced unequal there by local decision, and distinct indices have distinct Cohen labels. Thus these are also single-valuedness and injectivity for the actual sets of the graph.

Every label index belongs to a diagram in \(H\) below \(q\), by the density of extending diagrams to contain prescribed supports. Therefore the graph has domain \(A\). To reach an arbitrary \(E\)-class, take any label belonging to that class and include its index in such a diagram \(r\). Its canonical supported class name represents an element of \(\mathcal D_F(r)\). The local fiber bijection is onto the fiber containing that element, so the graph reaches the class. This is a pointwise existence argument; no simultaneous selection of representatives of all classes has been made. The range is exactly \(A/E\). The graph belongs to \(W\) because its name is HS.

The construction was made on an extension of an arbitrary symmetric condition asserting the nonwellorderable-quotient hypothesis. Applying the symmetric forcing theorem and truth lemma therefore proves in \(W\) that every such quotient \(A/E\) is in bijection with \(A\). Finally, for a surjection \(h:A\to Y\) in \(W\), form its kernel relation \(E\) in \(W\). The map \([a]_E\mapsto h(a)\) is a bijection \(A/E\to Y\), defined by its unique values without choosing class representatives. If \(Y\) is nonwellorderable, so is \(A/E\), and composing this bijection with the one just constructed proves the theorem. ◻

Proof. Suppose \(c\) were a choice function for this family, and let \(\lambda\) be the Hartogs ordinal of \(A\), so there is no injection \(\lambda\longrightarrow A\). Foundation gives \(A\notin A\). By transfinite recursion define \(a:\lambda\longrightarrow A\cup\{A\}\) as follows. At stage \(\alpha\), put \(S_\alpha=A\setminus\mathop{\mathrm{ran}}(a|\alpha)\) and set \[a(\alpha)= \begin{cases} c(S_\alpha),&S_\alpha\ne\varnothing,\\ A,&S_\alpha=\varnothing. \end{cases}\] If every \(S_\alpha\) were nonempty, the recursion would choose a different member of \(A\) at every stage, giving an injection \(\lambda\longrightarrow A\). Hence there is a least \(\alpha<\lambda\) with \(S_\alpha=\varnothing\). Before that stage no value is the sentinel \(A\), and \(a|\alpha\) is a bijection onto \(A\). This wellorders \(A\), a contradiction. Hartogs’ theorem and the recursion used here are available in \(\mathsf{ZF}\). ◻

Proof. The symmetric system is for one set forcing, with the set group and normal filter specified above. The set-forcing symmetric-model theorem, in its internal form, therefore gives full \(\mathsf{ZF}\), the canonical ground embedding, and preservation of the interpreted ordinals. For an externally transitive ground its evaluated hereditarily symmetric interpretation is transitive. These are pure-set models, so Foundation and the full Separation and Replacement schemata are included.

Proposition 16 gives the first hypothesis of Lemma 28 inside \(W\), and Proposition 17 gives the second, for all ordinal-indexed families in \(W\). Theorem 27, together with Remark 29, gives the third. The lemma proves \(\mathsf{PP}\) for every surjection in \(W\), with its witnessing injection in \(W\).

Proposition 18 proves that \(A\) is not wellorderable in \(W\). Applying Lemma 31 inside \(W\) gives the displayed family and failure of \(\mathsf{AC}\) there. Finally, Proposition 19 supplies the assertion about countable sequences. This last assertion concerns the symmetric model itself; it does not require countable closure of the full product forcing. ◻

Proof. The constructible-universe theorem proves, in \(\mathsf{ZF}\), the relativization to \(L\) of every \(\mathsf{ZF}\) axiom, of Choice, and of \(V=L\). These are assertions for each individual axiom instance, including the instances of Separation and Replacement. See (Welch 2020, Theorem 4.7, Lemma 4.10, Corollary 4.13, and Theorems 4.14 and 4.18).

Relativization commutes with Boolean connectives and preserves first-order inference when quantifiers are restricted to the nonempty interpreted domain. A finite contradiction proof from \(\mathsf{ZFC}+V=L\) would therefore yield, by relativizing each line and using the finitely many required interpreted axioms, a contradiction proof from \(\mathsf{ZF}\). This proves the consistency implication. The same constructible-universe theorem proves GCH in \(L\), hence proves GCH from \(\mathsf{ZFC}+V=L\). ◻

Proof. Atomic forcing is defined by the usual recursion on names. For a fixed formula, extend these atomic definitions through its finitely many connectives and quantifiers, restricting quantified names to \(\mathrm{HS}_{\mathcal S}\). For example, define \[D_{\varphi,\vec\tau} =\{q\in\mathbb Q:(\exists\sigma\in\mathrm{HS}_{\mathcal S})\ q\Vdash_{\mathrm{HS}_{\mathcal S}}\varphi(\sigma,\vec\tau)\}.\] Existential forcing is characterized by \[ p\Vdash_{\mathrm{HS}_{\mathcal S}}\exists x\,\varphi(x,\vec\tau) \quad\Longleftrightarrow\quad D_{\varphi,\vec\tau}\text{ is dense below }p. \tag{44}\] The set \(D_{\varphi,\vec\tau}\) exists by Separation from \(\mathbb Q\). The class of names and the hereditary symmetry predicate are definable by set-theoretic recursion. Thus all the displayed relations are ordinary first-order predicates. This construction is a schema indexed externally by formulas; it asserts no single satisfaction predicate for all formulas.

The logical and symmetry rules follow by induction on a fixed formula, with the internal name recursion supplying the atomic case. The resulting symmetric-model theorem and its forcing relation are standard; see (Jech 2003, Equations (15.39)–(15.41) and Lemma 15.51) and (Karagila 2026a, sec. 2.1, p. 4). We recall the parts that ensure the full axiom schemata.

Fix an arbitrary formula \(\varphi(x,\vec a)\) and hereditarily symmetric names \(\sigma,\vec\tau\) for its set and parameters. A Separation name uses the pairs \((\rho,q)\in\mathop{\mathrm{dom}}(\sigma)\times\mathbb Q\) for which \[q\Vdash_{\mathrm{HS}_{\mathcal S}} \rho\in\sigma\ \wedge\ \varphi(\rho,\vec\tau).\] The intersection of the stabilizers of \(\sigma\) and the finitely many parameter names fixes this name. That intersection belongs to \(\mathcal F\), and every member name is hereditarily symmetric. The atomic forcing rules and Equation (44) verify that it is the required subset. No restriction on \(\varphi\) or on the rank of \(\sigma\) has been imposed.

Write \(\operatorname{nrk}(\eta)\) for the name-rank \[\operatorname{nrk}(\eta)= \sup\{\operatorname{nrk}(\zeta)+1:(\zeta,r)\in\eta\}.\] For Replacement, fix a formula \(\psi(x,y,\vec a)\), a domain name \(\sigma\), and parameter names \(\vec\tau\). For each pair \((\rho,q)\in\mathop{\mathrm{dom}}(\sigma)\times\mathbb Q\) for which some hereditarily symmetric name \(\eta\) satisfies \[q\Vdash_{\mathrm{HS}_{\mathcal S}}\psi(\rho,\eta,\vec\tau),\] take the least possible name-rank of such an \(\eta\). This defines an ordinal-valued function on a ground set. Replacement in the ground bounds all these ranks strictly below one ordinal \(\beta\). All \(\mathbb Q\)-names of name-rank less than \(\beta\) form a set. Consequently \[\dot B_\beta= \{(\eta,1):\eta\in\mathrm{HS}_{\mathcal S},\ \operatorname{nrk}(\eta)<\beta\}\] is a set name. Every automorphism preserves name-rank and hereditary symmetry, so \(\dot B_\beta\) is fixed by the whole group and belongs to \(\mathrm{HS}_{\mathcal S}\).

Below a condition forcing totality of the relation on \(\sigma\), local witnesses from Equation (44) can therefore be replaced, at the same witnessing conditions, by names occurring in \(\dot B_\beta\). This gives a set bounding the required witnesses. When the relation is functional, Separation in that set gives its image. The bound \(\beta\) depends on the particular domain name and formula; it is not a bound on the universe of names.

For Power Set, normalize a name for a subset of \(\sigma\) using member names from \(\mathop{\mathrm{dom}}(\sigma)\) and the forcing tests for membership in that subset. The normalized names lie in the ground set \(\mathcal P(\mathop{\mathrm{dom}}(\sigma)\times\mathbb Q)\). Use all hereditarily symmetric candidates, under the conditions forcing that they are subsets of \(\sigma\). The stabilizer of \(\sigma\) permutes this collection, giving a hereditarily symmetric power-set name. Every symmetric subset has such a normalization, so the name supplies the entire internal power set. Check names and the canonical pairing and union constructions supply the remaining elementary existence axioms.

The usual internal name-rank argument verifies Foundation. Equivalently, the interpreted hereditary class is membership-closed inside the ordinary forcing extension: an element of an HS-valued set has an active member name of an HS name. Extensionality and Foundation then inherit their witnesses from the ordinary extension. This argument concerns first-order Foundation and does not assume that an arbitrary model is externally well founded.

All these name constructions and forcing verifications are proofs in the ground theory, for the chosen formula. They prove the asserted schema. They use local existential witnesses rather than a maximum principle for symmetric forcing; that maximum principle need not hold (Karagila 2026b, Proposition 10.26). ◻

Proof. Induct externally on the finite syntax of the standard formula, using atomic formulas, conjunction, negation, and existential quantification. The atomic case is Equations (45) and (46); atomic symmetric forcing agrees with ordinary forcing. Conjunction uses a common strengthening of two conditions in \(G\) and monotonicity.

For negation, the set of conditions deciding the particular formula is an internally definable dense subset of \(\mathbb Q\). It belongs to \(M\) by the Separation instance for its defining forcing predicate. Genericity gives a deciding condition in \(G\). The induction hypothesis excludes the wrong decision, and directedness excludes conditions in \(G\) forcing opposite answers.

Suppose \(p\in G\) symmetrically forces an existential statement. The set of local witness conditions in Equation (44), together with the conditions incompatible with \(p\), is another internally definable dense set. Genericity meets its first part. The internal witness is an actual element of \(|M|\) which \(M\) regards as an HS name. Its equivalence class is a witness in \(W\) by induction. Conversely, a witness in \(W\) has an internal HS representative; apply induction to that representative and the elementary existential forcing rule.

This proves the truth equivalence for every standard formula. Lemma 34, applied in \(M\) to each standard \(\mathsf{ZF}\) axiom instance, now gives \(W\models\mathsf{ZF}\). The proof never evaluates a name by external recursion over \(E^M\). Nor does it require a truth predicate in \(M\) for all formulas, including its possible nonstandard formula codes. ◻

Proof of Theorem 1. Assume \(\operatorname{Con}(\mathsf{ZF})\). By Lemma 33, \(\mathsf{ZFC}+V=L\) is consistent. Completeness and downward Löwenheim–Skolem give a countable model \(M\) of this theory. No transitivity or external well-foundedness is asserted.

Interpret the construction inside \(M\) and choose an external \(M\)-generic filter on its internal poset as above. Form the symmetric quotient \(W\) using Equations (45) and (46). Lemma 35 gives full \(\mathsf{ZF}\) in \(W\). The same lemma, applied to Equation (43), gives \[W\models\mathsf{ZF}+\mathsf{PP}+\neg\mathsf{AC}+\mathsf{AC}_{\mathrm{WO}}.\] Soundness therefore yields \(\operatorname{Con}(\mathsf{ZF}+\mathsf{PP}+\mathsf{AC}_{\mathrm{WO}}+\neg\mathsf{AC})\), as required.

Equivalently, one can extract the consistency implication directly from finite proofs. A purported contradiction proof from the target theory uses only finitely many \(\mathsf{ZF}\) instances. Translate its lines into symmetric forcing. The logical forcing rules preserve its inferences; Lemma 34 supplies its \(\mathsf{ZF}\) axioms; and Equation (43) supplies \(\mathsf{PP}\), \(\mathsf{AC}_{\mathrm{WO}}\), and \(\neg\mathsf{AC}\). This would make a nonempty poset force a contradiction, contrary to its atomic forcing laws. It therefore gives a contradiction proof in \(\mathsf{ZFC}+V=L\), which the constructible interpretation translates into one in \(\mathsf{ZF}\). This argument uses no stronger model-existence assumption. ◻

Proof of Theorem 2. Work in a \(\mathsf{ZFC}\) metatheory, and let \(V\) be the given countable transitive model of \(\mathsf{ZFC}\). Carry out Theorem 32 inside \(V\), using its parameters \[\kappa=\omega_1^V,\qquad \mu=\bigl((2^{\aleph_0})^+\bigr)^V,\qquad I=(\mu^+)^V.\] These are the arbitrary-choice-ground parameters of the construction.

Enumerate externally the dense subsets of the constructed poset which belong to \(V\), and recursively choose a descending sequence meeting them. Its upward-generated filter \(G\) is \(V\)-generic. Here genuine well-founded recursion on ground names is available, since \(V\) is transitive. Define \[W=\{\tau^G:\tau\in\mathrm{HS}^V\}.\] The set symmetric-extension theorem gives transitive models \(V\subseteq W\subseteq V[G]\) with the same ordinals, and gives all of \(\mathsf{ZF}\) in \(W\). Theorem 32 supplies \(\mathsf{PP}\), \(\neg\mathsf{AC}\), and \(\mathsf{AC}_{\mathrm{WO}}\) in this same \(W\), together with its stated preservation of countable sequences from any fixed ground set. To obtain the last assertion of Theorem 2, let \(f\in W\) be a countable sequence of elements of \(V\). Its rank in \(V[G]\) is bounded by a ground ordinal \(\alpha\), since forcing preserves the ordinals. Ranks of ground sets are absolute between these transitive models, so the range of \(f\) lies in the ground set \((V_\alpha)^V\). The preservation assertion of Theorem 32 applied to this set gives \(f\in V\). This proves the stated transitive-model conclusion.

This is a separate model-existence deduction. The ordinary consistency proof permits an externally ill-founded ground and does not itself assert the existence of a transitive model. ◻