Proof. The edge-block count is immediate from the definition of \(P_e\). At a vertex \(v\), each face \(f\in F(v)\) contributes one freely chosen vector in \(\mathbb F_3^2\), shared by its two sides at \(v\). Coordinates for different faces are distinct, so these choices contribute \(3^{2|F(v)|}\) possibilities. The scalar constraint in Equation (5) is one equation in \(d(v)\) variables, with every coefficient nonzero. Choose the scalars on all but one incident edge arbitrarily; the remaining scalar is then uniquely determined. Hence it contributes \(3^{d(v)-1}\) possibilities for every value of \(b_v\). This proves Equation (7) and nonemptiness. The block bounds follow from Equation (2). Finally, there are \(L^3\) vertices and \(3L^2(L-1)\le3L^3\) edges, which gives the asserted bounds on \(N_L\). ◻

Proof. The map \(B\) is bilinear and alternating. Its bilinearity gives \[B(a,a')+B(a+a',a'')=B(a',a'')+B(a,a'+a''),\] so both associations of a product of three elements in \(H\) agree. The identity and inverse follow from \(B(0,a)=B(a,0)=B(a,-a)=0\). The assertions about the central subgroup and projection now follow directly from the product formula. Finally, multiplying the four factors of the commutator gives \((0,B(a,a')-B(a',a))=(0,2B(a,a'))\). Since \(2(1/2)=1\) in \(\mathbb F_3\), this is Equation (10). ◻

Proof. For each edge \(e\), the restriction map \[\rho_e:H\longrightarrow P_e, \qquad \rho_e(a,k)=((a_f)_{f\in F(e)},k_e)\] is a homomorphism: the \(e\)-coordinate of \(B(a,a')\) is exactly the correction in the product on \(P_e\). Equation (11) is left multiplication by \(\rho_e(a,k)\). It therefore defines a group action on the edge states, with inverse \(h_{-a,-k}\).

Fix a configuration at \(v\). For each \(f\in F(v)\), write \(u_f\) for its common vector on the two incident sides of \(f\). Both copies receive the same addition \(a_f\), so the face equalities remain true. The change in its divergence is \[(\partial k)_v+ \frac12\sum_{f\in F(v)} \left(\sum_{e\ni v}\epsilon_{ve}c^f_e\right)\omega(a_f,u_f)=0.\] Here the first term vanishes because \(k\in K\), and every inner sum vanishes by Equation (1). The image is consequently a configuration with charge \(b_v\). The inverse map gives a bijection of each \(X_v\), and componentwise composition gives the same group law as on edge atoms.

Preservation of sorts and blocks proves preservation of \(\mathsf{Ed},\mathsf{Cf},\mathsf{EB},\mathsf{VB}\). The coordinatewise definition on configurations proves preservation of \(\mathsf I\). For the remaining relations, let \(g,g'\in P_e\) be two edge states and \(p=\rho_e(a,k)\). The group identity \[(pg)^{-1}(pg')=g^{-1}g'\] shows that their corrected scalar difference in Equation (4) is unchanged. Thus every \(\mathsf Z_\delta\) is preserved. These statements also apply to the inverse, so all eight relations are preserved in both directions, including nonrelations. This proves that the action is by automorphisms of \(A_b\).

If \(h_{a,k}\) fixes every atom, apply it to the state \((0,0)\) on each edge. Equation (11) then gives \(k_e=0\) for every \(e\) and \(a_f=0\) whenever \(f\in F(e)\). Every face has an edge, so \(a=0\) and \(k=0\); the action is faithful. The final assertion follows by setting \(a=0\) in Equation (11). ◻

Proof. Suppose first that such atoms exist. Each \(t_v\) is allowed. Inductively, none is deleted: across a tree edge from \(v\) to \(w\), the atom \(t_w\) survives the previous round and shares \(s_e\) with \(t_v\). Thus every block has a survivor.

Conversely, assume every block has a survivor at the fixed point. All survivors are allowed, and every survivor has a surviving support across each adjacent tree edge. Choose any survivor at the root of \(T\). Proceed away from the root, choosing for each child a surviving configuration supporting the one chosen at its parent. This defines one \(t_v\) at every vertex because \(T\) is a finite tree. On each tree edge, the two chosen configurations share an atom \(s_e\). Each configuration has exactly one neighbor in each incident edge block by \(\operatorname{Check}(A)\), so their selected edge atoms agree. On a non-tree edge, allowedness forces both endpoints to use its unique member of \(x\). These atoms give the required completion. This argument does not require configurations within a block to be determined uniquely by their incident neighbors. ◻

Proof. Inductively, the current state \(x\) consists of one selected atom from each edge in an initial segment of the ordered set \(\mathcal E\setminus T\). This holds at the empty state. A real choice lies in the next unselected edge, so the step adds one new atom and extends that initial segment. A dummy choice leaves \(x\) unchanged and hence stabilizes. Thus all earlier states are subsets of the current state. There are at most \(|\mathcal E|\leq n\) strict steps, followed by a stabilizing step.

Fix an actual prefix \(b_0=\emptyset,b_1,\ldots,b_i=x\), and let \[H_i=\operatorname{Aut}(A,\alpha,b_0,\ldots,b_i).\] Every element of \(M(\alpha,x)\) is a full-input automorphism fixing \(\alpha\) and fixing all atoms in \(x\) individually. Since \(b_j\subseteq x\) for \(j\leq i\), it fixes every earlier \(b_j\). Consequently \[M(\alpha,x)\subseteq H_i.\] All terms defining \(D\) and \(M\) are equivariant in their displayed arguments: they use only input relations, bounded set operations, ordinals, and the indicated iterations. An automorphism fixing \(\alpha\) and \(x\) therefore preserves \(D(\alpha,x)\), and it conjugates the family \(M(\alpha,x)\) to itself.

If the first case of Equation (18) applies, fix \(s\in D(\alpha,x)\). Invariance under \(H_i\) gives \(H_i s\subseteq D(\alpha,x)\), while the guard and \(M(\alpha,x)\subseteq H_i\) give \(D(\alpha,x)\subseteq H_i s\). Thus the choice set is exactly this orbit, and the maps in \(M\) witness every ordered pair of its members. If the second case applies, the choice set is \(\{\emptyset\}\), and identity witnesses its only pair. It belongs to \(M\) in every case. At a final state \(z\), the witnessing term evaluated on \((\alpha,z,b_i)\) returns exactly \(M(\alpha,b_i)\), as required. ◻

Proof. We first bound the states of the iterations independently of the annotation. The row families have at most \(n\) members, each a subset of \(A\). Every state of the iteration defining \(R_J\) is a subset of \(\mathcal V^2\times I_n\), with the fixed triple coding from above. It has polynomial hereditary size even on an input failing \(\operatorname{Check}(A)\). An inflationary iteration on this domain has at most \(n^2(n+1)\) strict updates. Every state in the deletion iteration is a subset of \(X\). By Lemma 6, every WSC state is a subset of \(Y\), and a path to first stabilization has at most \(n+2\) state labels. The parameter \(\alpha\) is a fixed-length tuple of blocks, and each supplied choice is an atom or the pure dummy. With the fixed pair coding, all these state and supplied-argument hereditary sizes, and all these iteration lengths, are bounded by \((n+2)^{100}\).

For the remaining terms, use hereditary size \(\rho(a)=1\) for an atom and \(\rho(a)=1+|\operatorname{TC}(a)|\) for a set. An actual activation here means a call to a subexpression with arguments supplied during evaluation of this expanded sentence before resource cutoffs. We include every choice path and every retrospective witness call. We verify by induction on expanded syntax height that a subexpression of height at most \(j\), at any actual activation whose free arguments have hereditary sizes at most \((n+2)^d\), where \(d\geq1\), constructs individual values of hereditary size at most \[(n+2)^{d_jd}.\] This induction includes the evaluations forming all candidates in \(\mathcal L,\mathcal C\), and \(M\), whether or not those candidates pass a subsequent test.

At height zero, variables and the constants \(\emptyset,\mathsf{Atoms}\) satisfy the bound. The primitive functions \(\mathsf{Pair},\mathsf{Union},\mathsf{Unique},\mathsf{Card}\) satisfy the next-height bound: pairing adds only finitely many wrappers to the two hereditary contents, union and unique extraction use their arguments’ contents, and \(\mathsf{Card}\) produces an ordinal no larger than the cardinality of the input set, or zero for an atom.

For a comprehension of height \(j+1\), its range has at most \((n+2)^{d_jd}\) members, and each such member has hereditary size bounded by the same quantity. Thus the condition and body have argument exponent at most \(d_jd\). By induction each body value has hereditary size at most \((n+2)^{d_j^2d}\). The union of their hereditary contents, together with the comprehension itself, is bounded by \((n+2)^{(d_j^2+d_j+2)d}\). The recurrence for \(d_{j+1}\) dominates this exponent and the bounds for all temporary condition and body evaluations. Atomic formulas and Boolean combinations introduce no larger sets.

At an ordinary iteration, its extra state argument has the independent bound \((n+2)^{100}\) proved above. Replacing the argument exponent \(d\) by \(100d\) bounds the step subexpressions by \((n+2)^{100d_jd}\). The returned state has the independent state bound; the recurrence again dominates both estimates. At the WSC operator the same argument applies to its step, choice, witness, and output subexpressions, because the intermediate and final states and the choices have the stated independent bound. In particular it applies when the witness term is reevaluated at any earlier state. The operator supplies a truth value; it does not collect the branching family of paths as one HF object.

This proves the induction. Starting with the sentence’s empty free assignment and using one extra height in Equation (23) gives the asserted common bound. The independent iteration bounds also lie below this polynomial. All these estimates were obtained before imposing resource cutoffs. Therefore the annotated and unbounded evaluations agree at every actual call, and no cutoff is reached. ◻

Proof. All macros use only the permitted finite syntax and bounded iterations. The only WSC calls in the outer comprehension have parameters in \(P\). Lemma 6 verifies every required witness using automorphisms of the entire input, including all three \(\mathsf Z_\delta\) relations, and respecting every earlier state. Lemma 7 excludes exceeded bounds. Hence neither source of \(\dagger\) occurs. Every path reaches a fixed point, so the output semantics applies to a nonempty family of terminal states. Equation (21) and Lemma 5 give the stated characterization.

An isomorphism transports the block families, \(P\), all bounded constructions, and all choice paths to their counterparts. It also preserves the output test. It may permute the parameter tuples, which leaves the outer existential comprehension unchanged. Thus the true-model class is invariant. If the input check fails or \(P\) is empty, the comprehension has empty range and the sentence is false. This includes the empty input. A connected graph with one vertex and no edges is also covered: its repeated four-entry tuple is resolving, the dummy stabilizes immediately, and the tree test asks only for a configuration in its nonempty vertex block. ◻

Proof. The sort and block relations have the required interpretations. Every configuration in \(X_v\) selects exactly one atom from \(Y_e\) for each \(e\ni v\), and none from other edge blocks. Each \(X_v\) is nonempty by Lemma 2. Thus the incidence test between blocks recovers precisely the incidences of the box. This graph is simple and connected, and each edge has its two distinct endpoints, so all the input checks hold.

Let \(o=(0,0,0)\) and, for \(i=1,2,3\), let \(q_i\) be the corner whose \(i\)th coordinate is \(L-1\) and whose other coordinates are zero. Distances in the box are sums of absolute coordinate differences. Indeed each step changes one coordinate by one, giving the lower bound, and changing the coordinates successively attains it within the box. Hence, for \(v=(v_1,v_2,v_3)\), \[d(o,v)-d(q_i,v)=2v_i-(L-1)\qquad(i=1,2,3).\] These are integer identities. The four distances therefore determine all three coordinates of \(v\). The tuple of blocks \((X_o,X_{q_1},X_{q_2},X_{q_3})\) belongs to \(P\). ◻

Proof. The four unit steps of a closed walk have zero sum in each coordinate. They therefore consist either of two positive and two negative steps in one direction, or of opposite pairs in two different directions. The first possibility cannot give a simple cycle: at a greatest or least coordinate reached, a reversal repeats the preceding vertex. In the second possibility no two successive steps can be opposites, since that would also repeat a vertex. The directions consequently alternate, and the four vertices are exactly the corners of an elementary square. Conversely, traversing any elementary square supplies a face description.

First consider adjacent sides \(e,e'\) of \(f\), meeting at \(v\). A configuration containing \(s\in Y_e\) and \(s'\in Y_{e'}\) must satisfy \(u_{s,f}=u_{s',f}\) by the configuration equations. Suppose this equality holds. The two sides share exactly the face \(f\). At \(v\), choose one vector for each face in \(F(v)\), using the vector prescribed by \(s\) or \(s'\) whenever that face meets the respective side; the only common prescription is the assumed equality on \(f\). Assign the chosen vector to both incident sides of each face. This extends all vector coordinates of the two given atoms without conflict.

Every vertex of the box has degree at least three, since \(L\ge2\). There is therefore an incident edge \(h\) other than \(e,e'\). Keep the two prescribed scalars, choose scalars arbitrarily on the remaining edges other than \(h\), and set \[z_h=\epsilon_{vh}^{-1} \left(b_v-\sum_{g\ni v,\ g\ne h}\epsilon_{vg}z_g\right).\] The coefficient \(\epsilon_{vh}\) is \(1\) or \(-1\), so it is invertible in \(\mathbb F_3\). We have constructed a configuration in \(X_v\) incident with both given atoms. This proves Equation (24) for adjacent sides, for every charge and including boundary vertices.

For opposite sides, the definition uses an atom on a side adjacent to both; for two atoms on the same side, it uses an atom on the next side in the description. The adjacent-side case shows that the two required tests hold precisely when this intervening atom has the same \(f\)-vector as both \(s\) and \(s'\). Every vector in \(\mathbb F_3^2\) occurs on the intervening side. The two configuration witnesses are independent, even when their vertex blocks coincide. Thus such an intervening atom exists exactly when \(u_{s,f}=u_{s',f}\). Finally, the descriptions containing \(e\) cover exactly its incident faces, which proves Equation (25). ◻

Proof. Write \(s=(e,u,z)\) and \(s'=(e,u',z')\). We construct a map from the local pool \(\mathcal L\) and then one from the cycle pool \(\mathcal C(\alpha,x)\), in the order used to define \(M\). Figure 1 illustrates the two transformations.

Define \(a\in C_F\) by \[a_f=\begin{cases} u'_f-u_f,&f\in F(e),\\ 0,&f\notin F(e). \end{cases}\] Let \(\ell=h_{a,0}\) be the automorphism from Proposition 4. A nonzero \(a_f\) can occur on at most four faces. Outside the edge and vertex blocks belonging to these faces, \(\ell\) is the identity by Equation (11) and the induced action on configurations. Each face has four sides and four vertices, so \(\ell\) moves atoms in at most sixteen edge blocks and sixteen vertex blocks. The block bounds in Lemma 2 give \[|\{t\in A_b:\ell(t)\ne t\}| \le16(3^9+3^{29})=B.\] Thus \(\ell\) occurs in the local pool: if its support is nonempty, list the moved atoms and their images in the two indexing tuples and pad them with repetitions; if its support is empty, use the explicitly included identity. This represents the whole permutation because it is the identity outside the listed atoms.

For \(f\in F_x(e)\), Equation (26) gives \(a_f=0\). Every face with a nonzero translation therefore contains no previously selected edge. All face coordinates and the scalar of each atom in \(x\) are unchanged, so \(\ell\) fixes \(x\) pointwise. On the current candidate, its value is \[ \ell(s)=(e,u',\widetilde z),\qquad \widetilde z=z+\frac12\sum_{f\in F(e)}c^f_e\omega(a_f,u_f). \tag{27}\] It remains to correct \(z'-\widetilde z\), which is the scalar discrepancy after this translation.

If \(z'=\widetilde z\), take the identity from the cycle pool. Otherwise put \(\eta=z'-\widetilde z\in\{1,-1\}\subseteq\mathbb F_3\). The cycle pool enumerates every auxiliary vertex block \(o\), so it includes the block at the coordinate origin. For this choice of \(o\), the function \(d(o,v)=v_1+v_2+v_3\) increases by one along every positive coordinate edge. Its labels \(1\) and \(2=-1\) consequently agree with signed edge traversal in the fixed coordinate orientations, regardless of the root or shape of \(T\).

Choose the ordering \((U,V)\) of the endpoints of \(e\) so that traversing \(e\) from \(U\) to \(V\) has sign \(\eta\). Follow this edge and then the unique tree path from \(V\) to \(U\). Because \(e\notin T\), this is a simple cycle. Let \(k\in\mathbb F_3^{E_L}\) have coefficient \(1\) or \(-1\) on each edge according to the traversal orientation and coefficient zero elsewhere. At each vertex one traversed edge enters and one leaves, so \[ \partial k=0,\qquad k_e=\eta,\qquad \operatorname{supp}(k)\subseteq T\cup\{e\}. \tag{28}\]

For the indices just chosen, the cycle-pool relation is exactly the graph of \(h_{0,k}\). To check this assertion on an edge of the cycle, Lemma 10 makes its \(\operatorname{baseEq}\) condition equivalent to equality of all vector coordinates. For equal vectors, alternation gives \(\omega(u_f,u_f)=0\), so the \(\mathsf Z_{\delta}\) condition becomes \(z'-z=\delta=k_h\). It therefore pairs each edge atom with precisely its scalar translate by \(k_h\). Off the cycle the relation is the identity, as is \(h_{0,k}\). On a vertex block, its definition pairs a configuration with precisely the tuple of these translated incident states. That tuple is a configuration by Proposition 4, and there is exactly one configuration atom for each permitted tuple. This proves the assertion on the configuration sort as well.

Call this cycle map \(c\). By Equation (28), it fixes every earlier selected atom: all their edges are outside \(T\) and different from \(e\). Both \(c\) and \(\ell\) preserve every block and the full vocabulary, so the composition \(g=c\circ\ell\) passes the filter defining \(M(\alpha,x)\). Equations (27) and (28) give \(g(s)=s'\). The same conclusion holds in the zero-discrepancy case with \(c\) equal to the identity.

We have proved nonemptiness and the witness guard for every compatible prefix with an unprocessed edge. The next real choice extends that prefix by one atom and preserves compatibility by Equation (26). Induction starts at \(x=\emptyset\). After all \(r\) edges have been processed, there is no next edge; the dummy choice leaves the state unchanged and is witnessed by the identity. Finally, fixing each block fixes the tuple \(\alpha\), and fixing all atoms of the current prefix fixes each earlier prefix as a set. Thus the maps satisfy the parameter and history requirements of witnessed symmetric choice. ◻

Proof. For a one-vertex tree, the sum condition says \(r=0\), and the empty edge assignment is the unique solution. Otherwise let \(v\) be a leaf, \(h\) its incident edge, and \(w\) its neighbor. The equation at \(v\) forces \(z_h=\epsilon_{vh}^{-1}r_v\). Delete \(v\) and \(h\); keep all other required divergences except that at \(w\), where set \[r'_w=r_w-\epsilon_{wh}z_h=r_w+r_v.\] The new required divergences still sum to zero. Induction supplies the unique solution on the smaller tree, which together with the forced value on \(h\) solves all the original equations. Each deleted edge was forced, proving uniqueness as well. ◻

Proof. By Lemma 9, both inputs pass the check and have a nonempty parameter set. Fix any \(\alpha\in P\) and any terminal selection \(x\). Proposition 11 says that \(x\) is a complete compatible assignment on the edges outside \(T=T(\alpha)\).

First work in \(A_{b^0}\). For each elementary face \(f\), choose its vector \(v_f\in\mathbb F_3^2\) to be the one already prescribed by \(x\) if an edge of \(f\) was selected, and choose any vector otherwise. Compatibility makes each prescription unambiguous. Give every edge \(e\) the vectors \((v_f)_{f\in F(e)}\). This preserves all selected vector coordinates and satisfies all face agreements at vertices.

Keep the selected scalars \(z_e\) on \(e\notin T\), and define the divergence still required from tree edges by \[r_v=b^0_v-\sum_{e\notin T}\epsilon_{ve}z_e.\] Every edge contributes once with each sign, and \(\sum_v b^0_v=0\); therefore \(\sum_v r_v=0\). Lemma 12 supplies the scalars on \(T\). The resulting full edge assignment has divergence \(b^0\) and satisfies every face agreement. Its incident tuple at each vertex is consequently a configuration atom, and neighboring tuples specify the same edge atom. By Lemma 5, the output test accepts \(x\).

Now work in \(A_{b^1}\). If the output test accepted \(x\), Lemma 5 would supply configurations agreeing on a single atom on every edge. Let \(z_e\) denote the scalar of that common atom. The equations at all vertices would give \[1=\sum_{v\in V_L}b^1_v =\sum_{v\in V_L}\sum_{e\in E_L}\epsilon_{ve}z_e =\sum_{e\in E_L}(1-1)z_e=0 \quad\text{in }\mathbb F_3,\] a contradiction. Thus every terminal selection is rejected.

The witness and resource conclusions of Proposition 8 apply to these calls, so their values are Boolean. The output value just proved is the same for every terminal selection for each parameter. Since \(P\) is nonempty, the outer existential aggregation defining \(\Phi\) is true on \(A_{b^0}\) and false on \(A_{b^1}\), as asserted. ◻

Proof. We first eliminate the cochain in one coordinate direction. We then eliminate a second direction on a slice containing few nonzero curls, and use the remaining curls to bound the support away from that slice.

Write vertices as \((i,j,k)\). The coordinate \(\ell_1(i,j,k)\) belongs to the edge from \((i,j,k)\) to \((i+1,j,k)\), and \(\ell_2,\ell_3\) are defined similarly. A direction-\(a\) edge coordinate is used only when increasing coordinate \(a\) stays in the box. Put \[\varphi_1(i,j,k)=\sum_{u=0}^{i-1}\ell_1(u,j,k), \qquad r^{(1)}=\ell-\partial^{\mathsf T}\varphi_1,\] where empty sums are zero. Then \(r^{(1)}_1=0\). The face orientation \(+1,+a,-1,-a\) gives \[\begin{align*} (D\ell)_{12}(i,j,k) &=r^{(1)}_2(i+1,j,k)-r^{(1)}_2(i,j,k),\tag{29}\\ (D\ell)_{13}(i,j,k) &=r^{(1)}_3(i+1,j,k)-r^{(1)}_3(i,j,k). \tag{30}\end{align*}\] Here \(ab\) indicates the face in directions \(a<b\) with lower corner \((i,j,k)\), and the identity is asserted whenever that face exists.

Let \(t_{ab}\) be the number of nonzero \(ab\) curls, so \(t=t_{12}+t_{13}+t_{23}\). The \(23\) faces are partitioned into the \(L\) slices of fixed first coordinate. Choose a slice \(i=i_0\) containing \(t_0\le t_{23}/L\) nonzero \(23\) curls. Define \[\varphi_2(i,j,k)=\sum_{v=0}^{j-1}r^{(1)}_2(i_0,v,k), \qquad r^{(2)}=r^{(1)}-\partial^{\mathsf T}\varphi_2.\] Because \(\varphi_2\) is independent of \(i\), we still have \(r^{(2)}_1=0\), and now \(r^{(2)}_2(i_0,j,k)=0\). Finally put \[\varphi_3(i,j,k)=\sum_{w=0}^{k-1}r^{(2)}_3(i_0,0,w), \qquad r=r^{(2)}-\partial^{\mathsf T}\varphi_3.\] The function \(\varphi_3\) is independent of \(i,j\), so \[r_1=0,\qquad r_2(i_0,j,k)=0,\qquad r_3(i_0,0,k)=0.\] All three gradient subtractions preserve curl. On the selected slice the \(23\) curl identity therefore becomes \[r_3(i_0,j+1,k)-r_3(i_0,j,k)=(D\ell)_{23}(i_0,j,k).\] For each fixed \(k\), every nonzero value of \(r_3(i_0,j,k)\) has a nonzero curl earlier on its \(j\)-line. One nonzero curl can affect at most \(L\) positions on that line. Thus at most \(Lt_0\) direction-\(3\) edge coordinates on the slice are nonzero. Direction \(2\) is zero there.

Copy these direction-\(2\) and direction-\(3\) slice values to every first coordinate \(i\), obtaining a reference cochain supported on at most \(L^2t_0\) edges, with direction \(1\) zero. Identities (29) and (30) remain valid for \(r\). Consequently \[r_2(i,j,k)-r_2(i_0,j,k)\] is the signed sum of the \(12\) curls between \(i_0\) and \(i\) on that line. A nonzero \(12\) curl occurs in at most \(L\) such sums, so at most \(Lt_{12}\) direction-\(2\) coordinates differ from the reference cochain. The same reasoning bounds the differing direction-\(3\) coordinates by \(Lt_{13}\). A coordinate in the support of \(r\) must either belong to the reference support or differ from its reference value. Hence \[|\operatorname{supp}(r)| \le L^2t_0+L(t_{12}+t_{13})\le Lt\le2Lt.\] Taking \(\varphi=\varphi_1+\varphi_2+\varphi_3\) proves the claim. The same construction gives \(r=0\) when \(t=0\). ◻

Proof. Let \(S=\{h\in H:h\cdot x=x\}\) be the stabilizer of \(x\). Let \(U\) be its image under the projection \(H\to C_F\), and put \(K_0=S\cap K\). Both \(U\) and \(K_0\) are subgroups of additive groups over the prime field \(\mathbb F_3\), and hence are vector subspaces. Define \[a=\operatorname{codim}_{C_F}U,\qquad d=\operatorname{codim}_{K}K_0,\qquad h=\log_3[H:S].\] The restriction of the projection to \(S\) has image \(U\) and kernel \(K_0\). Every fibre has size \(|K_0|\), so \(|S|=|U|\,|K_0|\). Since \(|H|=|C_F|\,|K|\), orbit–stabilizer gives \[ a+d=h=\log_3|H\cdot x|\le q\log_3N. \tag{31}\]

Consider the annihilator \[W=\{\lambda\in K^*: \lambda(k)=0\text{ for all }k\in K_0\}, \qquad \dim W=d,\] where \(K^*\) is the linear dual of \(K\). Each \(\lambda\in K^*\) extends to a linear functional on \(\mathbb F_3^E\): extend a basis of \(K\) to one of \(\mathbb F_3^E\) and assign arbitrary values on the additional basis vectors. The standard coordinate pairing thus gives an edge cochain \(\ell\) with \[\lambda(k)=\sum_{e\in E}\ell_e k_e\quad(k\in K).\] Two representatives differ by an element of \(K^\perp=\operatorname{im}\partial^{\mathsf T}\). Indeed the latter space is contained in \(K^\perp\), and both have dimension \(\operatorname{rank}\partial\). In particular, their curls agree.

Fix \(\lambda\in W\) and a representative \(\ell\). For any \(u,u'\in U\), choose lifts in \(S\). Their commutator belongs to \(K_0\); the commutator formula (10) therefore implies \[ 0=\sum_{f\in F}(D\ell)(f)\,\omega(u_f,u'_f). \tag{32}\] The right-hand side defines an alternating bilinear form \(\beta_\ell\) on \(C_F\). If \(t\) of the coefficients \((D\ell)(f)\) are nonzero, its rank is \(2t\): each nonzero coefficient multiplies a nondegenerate two-dimensional alternating block, and the face coordinates are independent summands of \(C_F\). Relations among the boundary vectors \(c^f\) do not identify these summands.

We use the standard dimension bound for isotropic subspaces of an alternating form, after quotienting by its radical (Cameron 2000, sec. 3.1 and 3.3). Equation (32) says that \(U\) is totally isotropic for \(\beta_\ell\), meaning that the form vanishes on \(U\times U\). Put \(n_F=\dim C_F\), and let \(R=\{v\in C_F:\beta_\ell(v,w)=0\text{ for every }w\in C_F\}\) be the radical of this form. The quotient \(C_F/R\) is nondegenerate of dimension \(2t\). The image \(\overline U\) of \(U\) is isotropic, so \(\overline U\subseteq\overline U^{\perp}\) and \(\dim\overline U\le t\). The radical has dimension \(n_F-2t\), whence \[\dim U\le(n_F-2t)+t=n_F-t, \qquad t\le a.\] Lemma 15 now replaces \(\ell\) by a representative of the same functional \(\lambda\) supported on at most \(2La\) edges.

We have obtained a sparse representative for every functional detecting the quotient \(K/K_0\). Choose such representatives for a basis of \(W\), and let \(T\subseteq E\) be the union of their supports. Then \[ |T|\le2Lad\le2Lh^2\le2L(q\log_3N)^2. \tag{33}\] When \(d=0\), use the empty basis and \(T=\emptyset\). If \(k\in K\) vanishes on \(T\), every member of that basis vanishes on \(k\). Thus all of \(W\) vanishes on \(k\), and finite-dimensional duality gives \(k\in K_0\). For each \(e\in T\), choose one edge atom on \(e\), and list the chosen atoms in a tuple \(\alpha\). The central action in (11) fixes that atom exactly when \(k_e=0\). Consequently \(K_\alpha\subseteq K_0\subseteq S\), so \(\alpha\) supports \(x\) and satisfies (33). This argument concerns the stabilizer of \(x\) alone and makes no induction on its rank. ◻

Proof. \(H\)-invariance places the orbit of each \(x\in\mathcal X\) inside \(\mathcal X\). Proposition 16 therefore gives the claimed support for every member. Membership transitivity gives the same conclusion for all recursive members. Adding coordinates to an atom tuple can only shrink its pointwise stabilizer, so it preserves the support property. Since \(L\ge2\), the base has an edge atom; append copies of any one such atom to reach length \(s\), including when the original support is empty. Finally Lemma 2 gives \(N=\Theta(L^3)\), which yields the displayed asymptotic bound. ◻

Proof. Let \(a_{ij},b_{ik},d_{jk}\) be the indicators of the three projections of \(R\) onto coordinate pairs, and let their sizes be \(A,B,D\), respectively. Every point of \(R\) contributes to the product of these indicators. Twice applying Cauchy–Schwarz gives \[\begin{align*} |R| &\le\sum_{i,j,k}a_{ij}b_{ik}d_{jk}\\ &\le A^{1/2} \left(\sum_{i,j}\left(\sum_k b_{ik}d_{jk}\right)^2\right)^{1/2} \le (ABD)^{1/2}. \end{align*}\] For the last step, bound each squared inner sum by \((\sum_k b_{ik}^2)(\sum_k d_{jk}^2)\) and then sum over \(i,j\). At least one projection consequently has size at least \(|R|^{2/3}\). It indexes that many nonempty coordinate lines meeting \(R\). At most \(|R|/L\) of these lines lie wholly in \(R\). Each of the remaining lines is a path meeting both \(R\) and its complement, and hence contains a boundary edge. The lines are disjoint, so these edges are distinct. Finally, \[|\delta_G R|\ge |R|^{2/3}-\frac{|R|}{L} \ge (1-2^{-1/3})|R|^{2/3},\] where the last inequality uses \(|R|\le L^3/2\). ◻

Proof. Sum Lemma 18 over the components \(R\) of \(G\setminus T\) having at most \(L^3/2\) vertices. Every boundary edge belongs to \(T\) and is counted at most twice. Thus \[ \sum_R |R| \le c^{-3/2}\sum_R|\delta_G R|^{3/2} \le c^{-3/2}(2|T|)^{3/2} \le c^{-3/2}(12M)^{3/2}=o(L^3). \tag{36}\] Here \(\sum_j a_j^{3/2}\le(\sum_j a_j)^{3/2}\) for nonnegative \(a_j\), and \(M^{3/2}=O(L^{21/8})=o(L^3)\). If every component had at most half the vertices, the left side would be \(L^3\), a contradiction for large \(L\). Two components cannot both contain more than half the vertices. After further deletion each component is contained in an old component; its size forces the new large component to lie in the old large one. ◻

Proof. An assigned edge atom touches its edge. An assigned configuration atom at \(v\) touches every edge incident with \(v\). The edges touched by at most \(M\) assigned positions form a set \(T\) of size at most \(6M\).

Call paired assignments in the two structures compatible if they have matching block and vector labels and there exist \(t\in\mathbb F_3^E\) and a vertex \(w\) in the giant of \(G\setminus T\) such that \[ \partial t=b^1-b^0-\mathbf1_w, \tag{37}\] and each atom in the first assignment is paired with the atom obtained by adding \(t_e\) on every incident scalar coordinate. The empty assignments are compatible: take \(t=0\) and \(w=v_*\).

Compatible assignments preserve atomic formulas. On any fixed edge, common addition of \(t_e\) preserves raw scalar differences, and also the corrected differences defining each \(\mathsf Z_\delta\), since vector coordinates do not change. It preserves whether the assigned edge atom is the state specified by an assigned configuration. Blocks, sorts, the preorder, and equality are likewise preserved, including when positions have repeated values. An assigned configuration cannot be at \(w\): deleting its whole star isolates its vertex, whereas \(w\) lies in a component with more than half the vertices. Thus the shift at every assigned configuration satisfies the appropriate change of divergence in (37).

Forgetting an assigned position preserves compatibility. Its touched edges may disappear from \(T\), and Lemma 19 places the old giant inside the new one. Suppose now that at most \(M-1\) positions remain. We construct a bijection of universes which retains their pairings and gives a compatible extension for every possible next atom.

Partition the atoms into whole edge blocks and whole configuration blocks. For each such block \(J\), let \(T_J\) be \(T\) together with the edge of \(J\), or the star of its vertex, respectively. Then \(|T_J|\le6M\). Choose a vertex \(w_J\) in the giant of \(G\setminus T_J\). By Lemma 19, both \(w\) and \(w_J\) lie in the giant of \(G\setminus T\). Choose a signed path vector \(p_J\) supported outside \(T\) with \[\partial p_J=\mathbf1_w-\mathbf1_{w_J};\] one may traverse a path from \(w_J\) to \(w\), or use zero if they agree. The vector \(t_J=t+p_J\) agrees with \(t\) on \(T\) and satisfies (37) with \(w_J\) in place of \(w\).

On the block \(J\), map every atom by its \(t_J\)-shift. For an edge block this is plainly a bijection to the corresponding block. For a configuration block at \(v\), deleting its star isolates \(v\), so \(v\ne w_J\). Therefore \[(\partial t_J)_v=b^1_v-b^0_v,\] which is exactly the condition making translation a bijection between the two configuration blocks. All their vector constraints stay the same. Taking the union over the disjoint blocks gives a bijection of the whole universes. On every retained assignment it agrees with the old pairing because \(p_J\) vanishes on \(T\). If the next atom belongs to \(J\), the extended assignment has witness \(t_J,w_J\): its touched set is \(T_J\), and all retained coordinates still have the right images.

Induct on formulas to show that compatible assignments agree on every \(C^M\) formula with their designated free positions. Atomic formulas were checked above; Boolean connectives preserve agreement. At a quantifier, forget the old value, if any, of its bound variable. At most \(M-1\) positions remain. The universe bijection just constructed pairs extensions with compatible assignments, so induction makes the body true on equally many extensions. It preserves ordinary quantifiers and every exact counting quantifier, including count zero. Apply this conclusion to the empty assignments. ◻

Proof. Extend \(\sigma\) by zero to all of \(E\). An extension is equivalent to a vector on \(E\setminus T\) having divergence \(-\partial\sigma\). On a connected graph, an incidence vector always has total sum zero. Conversely, any specified vertex vector of total sum zero is an incidence vector: choose a spanning tree, give nontree edges value zero, and remove leaves successively. The equation at a leaf determines its tree-edge value uniquely because its coefficient is \(1\) or \(-1\). The total-sum condition makes the last root equation hold. This also handles a one-vertex component, where the only possible divergence is zero. Applied separately to each component of \(G\setminus T\), this argument gives exactly the conditions (38).

The sum of all \(R_U\) is zero, since the two incidence signs of each edge cancel. If one component fails, at least two fail. Hence one failing component has at most \(L^3/2\) vertices. Its boundary is contained in \(T\), so Lemma 18 yields \(c|U|^{2/3}\le|\delta_G U|\le|T|\). ◻

Proof. Write the tuples as \(\bar a,\bar a'\). The proof first extracts a consistent scalar shift on the touched edges, then uses a formula to exclude every obstruction from Lemma 21.

Each preorder class is defined with two variable names. If \(h\) is the number of atoms in strictly earlier classes, its predicate is \[ \theta_h(x):=\exists^{=h}y\, (y\preceq x\land\neg(x\preceq y)). \tag{40}\] Different classes have different \(h\) because every class is nonempty. Equality of types therefore places \(a_i\) and \(a_i'\) in the same class for every \(i\). In particular, their blocks and complete vector patterns agree. The two tuples touch the same set \(T\) of edges, with \(|T|\le6r\).

An occurrence on \(e\in T\) is either an edge atom in a tuple position, or the state on \(e\) specified by a configuration in a tuple position. In the latter case this state is the unique atom \(y\) such that \(\mathsf I(a_i,y)\) holds and \(y\) has its specified edge-class label. The label includes \(e\) and the vector pattern, so it is expressed by one of the predicates (40). Corresponding occurrences for \(\bar a\) and \(\bar a'\) consequently have the same edge and vector coordinates.

For two occurrences on the same edge, their raw scalar difference is testable using \(\mathsf D_\delta\), introducing their uniquely specified neighbors when necessary. Such a test uses at most the \(r\) tuple names, two neighbor names, and one further name reused in class predicates. Inequality (39) supplies these \(r+3\) names. The raw differences of corresponding occurrences are therefore equal. It follows that for every \(e\in T\) there is a single well-defined value \(\sigma_e\in\mathbb F_3\): the scalar change from an occurrence in \(\bar a\) to its counterpart in \(\bar a'\). The value is independent of the chosen occurrence.

Suppose this partial shift \(\sigma\) does not extend to \(K\). By Lemma 21, a component \(U\) of \(G\setminus T\) has \[R_U\ne0,\qquad |U|\le(6r/c)^{3/2}.\] We construct a formula distinguishing \(\bar a\) from \(\bar a'\) within the stated variable bound.

Choose, for each \(v\in U\), an arbitrary configuration atom \(g_v^0\) in \(\bar A_b\), and denote its state on an incident edge \(e\) by \(h_{v,e}^0\). Such configurations exist for every \(v\). On each boundary edge \(e\in\delta_G U\subseteq T\), choose one tuple occurrence and write its state as \(o_e^0\). Let \(z(s)\) denote the scalar coordinate of an edge state \(s\); in the following construction it is only used to specify one of the three relation symbols \(\mathsf D_\delta\).

The formula existentially quantifies a configuration variable \(g_v\) for each \(v\in U\), a state variable \(h_{v,e}\) for every edge incident with \(v\), and, when \(o_e^0\) comes from a tuple configuration, one additional neighbor variable \(y_e\). Write \(o_e\) for this \(y_e\) or for the selected tuple variable when the occurrence is already an edge atom. The conjunction under these quantifiers imposes the following conditions:

1. Each \(g_v\) and \(h_{v,e}\) has the class of its reference atom \(g_v^0\) or \(h_{v,e}^0\), and \(\mathsf I(g_v,h_{v,e})\) holds.

2. On every edge \(e\) with both endpoints \(v,w\in U\), choose one ordering of the endpoints and impose \[\mathsf D_{z(h_{w,e}^0)-z(h_{v,e}^0)} (h_{v,e},h_{w,e}).\]

3. On every boundary edge \(e\) with endpoint \(v\in U\), impose \[\mathsf D_{z(h_{v,e}^0)-z(o_e^0)}(o_e,h_{v,e}).\] When \(o_e=y_e\), also require its reference edge class and its incidence with the chosen tuple configuration.

All class conditions use (40). Thus this is a finite formula in the expansion’s vocabulary, with \(\bar a\) as its free assignment. Its length and counting constants may depend on the chosen reference atoms. The reference configurations and states witness that it is true at \(\bar a\).

The internal-edge condition also applies when \(e\in T\) has both endpoints in \(U\). It does not link that edge to a tuple occurrence; the two contributions of such an edge to \(R_U\) already cancel. Also, the reference configurations need not have matching vector patterns on their common edge. This is why \(\mathsf D_\delta\) was defined between all states on the same edge, irrespective of their vectors.

If the formula were true at \(\bar a'\), compare its state witnesses to the reference states and put \[d_{v,e}=z(h_{v,e})-z(h_{v,e}^0).\] Both configurations at \(v\) have divergence \(b_v\), so \[\sum_{e\ni v}\epsilon_{ve}d_{v,e}=0.\] The constraints on an internal edge give \(d_{v,e}=d_{w,e}\). On a boundary edge, the tuple occurrence has scalar change \(\sigma_e\); its uniqueness also gives this change when it is represented by \(y_e\). The boundary constraint therefore forces \(d_{v,e}=\sigma_e\). Summing the displayed vertex equations over \(U\) cancels every internal edge and leaves \(R_U=0\), a contradiction.

To count variable names, retain the \(r\) tuple names, use \(|U|\) configuration names and at most \(6|U|\) incident-state names, and use at most \(|\delta_G U|\le6r\) extra occurrence names. One additional name can be reused inside every class predicate without capturing any of these names. The total is at most \[r+7|U|+6r+1 \le7r+7(6r/c)^{3/2}+1\le M.\] We have obtained a \(C^M\) formula distinguishing the tuples, contrary to their type equality. Hence \(\sigma\) extends to some \(k\in K\). Its action maps each edge occurrence, and thus every tuple configuration as well, to its counterpart. For empty tuples, take \(k=0\). ◻

Proof. By \(N=\Theta(L^3)\), \(s=O_q(L(1+\log L)^2)\). Uniformly for \(1\le r\le(m+4)s\), the left side of (39) is \[O_{q,m}\bigl(L^{3/2}(1+\log L)^3\bigr)=o(L^{7/4}).\] The floor in \(M\) does not affect this eventual inequality. Also, \(\max\{4,m+1\}s=o(L^{7/4})\). Increasing \(L\) if necessary supplies Lemma 19 and Proposition 20 as well. The threshold may depend on the fixed \(q,m\). ◻

Proof. Projection and reordering follow by renaming variable positions: an injection from the selected positions to the original positions extends to a permutation of the \(M\) variable names. This renames bound variables as well, so it avoids capture. Repeated atom values cause no difficulty, because equality formulas record them.

For \(d=1\), choose a tuple realizing \(\rho\). For every tuple in either finite structure whose type differs from \(\rho\), choose a formula distinguishing it from this representative, and negate that formula if necessary so that the representative satisfies it. The conjunction of these finitely many formulas, denoted \(\theta_\rho\), holds exactly on the tuples of type \(\rho\) in the two structures. It has free variables among the first \(a+1\) positions and uses the same \(M\) variable names. If there are no other types, take a tautology. If \(P\) has exactly \(h\) extensions realizing \(\rho\), then \[\exists^{=h}x_{a+1}\, \theta_\rho(x_1,\ldots,x_a,x_{a+1})\] holds at \(P\) and hence at \(P'\). This includes \(h=0\). For empty prefixes in different structures, agreement of the types means exactly the assumed agreement on \(C^M\) sentences.

For \(d>1\), let \(\sigma\) be the projection of \(\rho\) to the first \(a+d-1\) positions. By induction the numbers of extensions from \(P,P'\) to \(\sigma\) agree. The one-coordinate case, applied both within one structure and between the two structures, shows that each realization of \(\sigma\) has the same number of extensions to \(\rho\). Multiplying the two finite counts proves the assertion. ◻

Proof. Automorphisms preserve \(C^M\) types. Induction on the form proves the displayed identity, using the change of witness molecule \(\beta\mapsto g\beta\) in Equation (42). It follows that \(\alpha\) supports \(\phi*\alpha\). The same induction shows that every member of a set-form value, and all of its recursive members, has a support of length \(s\). Thus every form value belongs to \(D_i\).

Conversely, use induction on the hereditary construction of an object \(x\in D_i\). If \(x\) is an atom, choose a molecule with first coordinate \(x\) and use \(c_1\). If \(x\) is a set, choose a supporting molecule \(\alpha\). For every \(y\in x\), induction gives \(y=\psi_y*\beta_y\). Set \[\phi=\{(\psi_y,\operatorname{tp}^{B_i}_M(\beta_y,\alpha)):y\in x\}.\] Every \(y\in x\) belongs to \(\phi*\alpha\). Conversely, a member of \(\phi*\alpha\) has the form \(\psi_y*\beta\) with \[\operatorname{tp}^{B_i}_M(\beta,\alpha) =\operatorname{tp}^{B_i}_M(\beta_y,\alpha).\] Homogeneity for tuples of length \(2s\) gives \(g\in K_i\) sending \((\beta_y,\alpha)\) to \((\beta,\alpha)\). Thus \(g\) fixes \(\alpha\), so \(gx=x\), and equivariance gives \(\psi_y*\beta=gy\in x\). Hence \(\phi*\alpha=x\). For the empty set, \(\phi\) is the empty set form. ◻

Proof. For equality, induct on the sum of the depths of \(\phi,\psi\). If both forms are atomic, equality compares two molecule coordinates and is recorded by the joint type. If exactly one is atomic, equality is false on both sides.

Suppose now that both are set forms and \(\phi*\alpha=\psi*\beta\). Take a member of \(\phi*\alpha'\), witnessed by \((\theta,\rho)\in\phi\) and \(\gamma'\) such that \(\operatorname{tp}_M(\gamma',\alpha')=\rho\). By Lemma 25, the matching prefix \((\alpha,\beta)\) can be extended by \(\gamma\) so that \[\operatorname{tp}_M(\alpha,\beta,\gamma) =\operatorname{tp}_M(\alpha',\beta',\gamma').\] Thus \(\theta*\gamma\in\phi*\alpha=\psi*\beta\). Choose its membership witness \((\xi,\sigma)\in\psi\) and \(\zeta\) with \[\operatorname{tp}_M(\zeta,\beta)=\sigma, \qquad \theta*\gamma=\xi*\zeta .\] Extend the primed prefix of length \(3s\) once more, obtaining \(\zeta'\) such that \[\operatorname{tp}_M(\alpha,\beta,\gamma,\zeta) =\operatorname{tp}_M(\alpha',\beta',\gamma',\zeta').\] This uses \(4s\leq M\). Projection preserves the membership-witness types. Since \(\theta\) and \(\xi\) have smaller depths than \(\phi\) and \(\psi\), the induction hypothesis gives \(\theta*\gamma'=\xi*\zeta'\). Therefore the chosen member lies in \(\psi*\beta'\). Interchanging \(\phi,\psi\) proves the other inclusion; interchanging the primed and unprimed data proves the reverse implication. Empty set forms are included because their inclusions are vacuous.

For membership, if the right-hand form is atomic then membership is false. Otherwise a witness for \(\phi*\alpha\in\psi*\beta\) consists of \((\theta,\rho)\in\psi\) and a molecule \(\gamma\) with \[\operatorname{tp}_M(\gamma,\beta)=\rho,\qquad \phi*\alpha=\theta*\gamma .\] Extend \((\alpha',\beta')\) to match \((\alpha,\beta,\gamma)\), using \(3s\) positions. The equality transfer already proved transfers the equality to this witness, and hence transfers membership. The converse is symmetric.

A form evaluates to an atom exactly when it is atomic. Base relations are false if any argument is a set. Otherwise, each argument is a specified molecule coordinate, so the truth of a base relation is recorded by the joint type. ◻

Proof. Fix the representing tuples \(P,P'\). A label is a pair \((\phi,\tau)\) consisting of a form and a realized type of length \((r+1)s\). Its value set on the first side is \[X_{\phi,\tau}(P)= \{\phi*\gamma:\gamma\in B_0^s,\ \operatorname{tp}_M(P,\gamma)=\tau\};\] define \(X_{\phi,\tau}(P')\) in \(B_1\) similarly. Lemma 25 shows that these value sets are either both empty or both nonempty.

Write \(K_{0,P}\) for the pointwise stabilizer of the coordinates of \(P\) in \(K_0\), and \(K_{1,P'}\) for the corresponding stabilizer in \(K_1\). Every nonempty \(X_{\phi,\tau}(P)\) is a single \(K_{0,P}\)-orbit. Indeed, homogeneity for \[(r+1)s\leq\max\{2,m\}s\] shows that the molecules of the specified type over \(P\) form a single \(K_{0,P}\)-orbit. Equivariance of form evaluation makes their value set one orbit as well. The same holds on the second side. In particular two nonempty label sets on either side are equal or disjoint.

We compare first their overlaps and then their cardinalities. Suppose two labels overlap on the first side, with molecules \(\gamma,\zeta\) witnessing equal form values. Extend \(P'\) to match the type of \((P,\gamma,\zeta)\). This uses \[(r+2)s\leq(m+1)s\leq M.\] Projection preserves each label condition, and Lemma 27 preserves equality of the two values. Thus the labels overlap on the second side. The converse follows by interchanging the sides.

Equal numbers of molecules do not yet give equal numbers of represented objects: several molecules may evaluate to the same value. We will show that evaluation has constant fibre size on each label and that this size agrees in the two structures.

Fix a nonempty label \((\phi,\tau)\). Let \(n\) be the number of its molecules over \(P\); the corresponding number over \(P'\) is also \(n\), by Lemma 25. The map \[\gamma\longmapsto\phi*\gamma\] from these molecules onto \(X_{\phi,\tau}(P)\) has fibres of a common positive size. To see this, choose preimage molecules of any two values. An element of \(K_{0,P}\) taking the first molecule to the second maps the first fibre bijectively onto the second by equivariance.

Choose molecules \(\gamma,\gamma'\) realizing \(\tau\) over \(P,P'\). The fibre containing \(\gamma\) has size \[h= \bigl|\{\zeta\in B_0^s: \operatorname{tp}_M(P,\zeta)=\tau,\ \phi*\gamma=\phi*\zeta\}\bigr|.\] Partition the possible \(\zeta\) by the finitely many realized types of \((P,\gamma,\zeta)\). On each type, the two displayed conditions have a constant truth value, within either structure and between the structures: projection determines the first, and Lemma 27 determines the second. By Lemma 25, each such type has equally many extensions over \((P,\gamma)\) and \((P',\gamma')\). Again the required length is only \((r+2)s\). Summing these finite extension counts shows that the corresponding fibre on the second side has the same size \(h\). Consequently \[|X_{\phi,\tau}(P)| =\frac{n}{h} =|X_{\phi,\tau}(P')|.\]

By Lemma 26, the label sets cover the respective domains. Partition the nonempty labels by overlap on the first side. The same equivalence relation is obtained on the second side. For each label class, its value set in \(D_0\) and its value set in \(D_1\) are finite sets of the same size. Choose a bijection between them. Different classes have disjoint value sets, so the union of these bijections is a bijection \(f:D_0\to D_1\).

This construction does not require either domain to be finite. There are countably many labels, since there are finitely many base types of each relevant length and every form is a finite expression. For an explicit set-theoretic choice of the bijections, fix external enumerations of the labels and of the two countable HF universes. Use the first label in each class, and match the members of its two finite value sets in enumeration order. These external enumerations are used only in this proof.

If \(x\) is matched with \(x'\), the class’s representative label \((\phi,\tau)\) supplies molecules \(\gamma,\gamma'\) with \[x=\phi*\gamma,\quad x'=\phi*\gamma',\quad \operatorname{tp}_M(P,\gamma) =\operatorname{tp}_M(P',\gamma')=\tau .\] Thus the extended assignments are represented alike. If \(x=x_j\) for a retained position, projection onto the molecules for \(x_j\) and \(x\), followed by Lemma 27, forces \(x'=x'_j\). This also proves consistency when retained values repeat. ◻

Proof of Theorem 24. We prove by induction on \(C^m\) formulas that represented-alike assignments to their free variables agree on truth. For atomic formulas involving two distinct variables, project onto their two molecules and apply Lemma 27. Atomhood is determined by the form. For a repeated variable, \(x=x\) is always true and \(x\in x\) always false in \(\operatorname{HF}(B_i)\); a diagonal base relation is false on a set and is otherwise determined by a coordinate in the molecule type. Unary base relations are treated in the same way. Boolean connectives preserve agreement.

For a quantifier binding \(x\), retain only the assignments to the other free variable names, dropping the previous value of \(x\) if present. There are at most \(m-1\) retained positions. Lemma 28 supplies a bijection of the domains for which every extension by \(x\) is represented alike. By the induction hypothesis, this restricts to a bijection between the sets of values satisfying the quantified body. It preserves existence and, for every natural number \(h\), the assertion that there are exactly \(h\) satisfying values. This remains valid when the satisfying sets are infinite: a bijection preserves finiteness and every finite cardinality. Universal quantification follows as well, or follows by negation. The empty assignments are represented alike, which proves the theorem. ◻

Proof. We first prove a polynomial bound for an arbitrary fixed subexpression evaluated on arguments of polynomial hereditary size. More precisely, if the sum of the sizes of the families \(\langle a\rangle\) for its arguments is at most \(R\), syntax induction bounds both its number of recursive activations and the total number of hereditary objects in these activations by a polynomial in \(n+R+2\). The polynomial may depend on the subexpression and on the annotation.

Variables and constants satisfy this assertion directly. Pair and Union add or collect only polynomially many existing objects. Unique returns a member or \(\emptyset\). Card returns the finite ordinal equal to the number of members of its argument, or zero on an atom. An ordinal \(k\) and all its recursive members comprise \(k+1\) objects, so this operation also satisfies the assertion. Composition uses the child bounds a fixed number of times.

For a comprehension, the induction hypothesis bounds the hereditary size of its range by a polynomial in \(n+R+2\), hence bounds its number of members. Each condition is evaluated on the parameters and one such member. Each required body evaluation has arguments of the same polynomial hereditary bound. Applying the child estimates at this enlarged bound and multiplying by the number of range members gives a polynomial total. Taking the set of body values adds one object and does not increase this estimate beyond another polynomial.

For an iteration, every state supplied to the next step has passed the guard and has hereditary size at most \(P(n)+1\). The parameters retain their original bound \(R\). By the induction hypothesis, a step on these arguments uses polynomially many hereditary objects. There are at most \(P(n)+1\) step evaluations before the stopping rule applies. This includes the first candidate violating the size guard: it is the output of a child evaluation on the preceding, bounded state, so it still has a polynomial hereditary bound, possibly larger than \(p(n)\). It also includes the last candidate needed to compare \(a_{P(n)+1}\) with \(a_{P(n)}\). The empty default adds only a constant. This argument applies to a nested iteration by the same syntax induction; it does not assume that the step is iteration-free. Boolean and atomic formula evaluations only combine these bounds. At the sentence, \(R=0\), and a fixed integer exponent \(q\) absorbs the resulting polynomial for all sufficiently large \(n\).

Every operation commutes with automorphisms of the input. The full comprehension range is used, the truth condition is invariant under the corresponding action on parameters, and the iteration stopping tests use only equality and cardinality. Thus an automorphism sends every activation to an activation at the same syntax occurrence and sends its value to the corresponding value. Starting with the empty assignment makes the whole family invariant. Closing it under membership preserves invariance and gives membership transitivity by definition. ◻

Proof. Choose a common integer \(J=J(n)\ge1\), depending only on the polynomial bounds in the proof of Lemma 29, which bounds the hereditary size of every argument and value in the evaluation. In particular it bounds all cardinalities passed to Card and all descending membership depths of tested candidates. Increasing \(J\) to an integer polynomial bound is harmless.

For each term occurrence \(t\), with free argument tuple \(\bar x\), we construct a relational formula \(G_t(\bar x,v)\). For each formula occurrence \(\theta\), we construct a truth formula \(F_\theta(\bar x)\). Write \(\operatorname{val}_A(t,\bar a)\) for the bounded semantic value of \(t\) at \(\bar a\). Our simultaneous induction assertion is \[ \begin{split} D\models G_t(\bar a,v) &\quad\Longleftrightarrow\quad v=\operatorname{val}_A(t,\bar a) \qquad\text{for every }v\in D,\\ D\models F_\theta(\bar a) &\quad\Longleftrightarrow\quad \theta\text{ is true at }\bar a, \end{split} \tag{43}\] whenever the displayed argument tuple is an activation of the indicated occurrence. Every genuine term value belongs to \(D\) by the trace assumption. No assertion is made about an argument tuple which never occurs.

Write \(\operatorname{At}(v)\) for the atom predicate and define the typed empty-set predicate \[E(v):=\neg\operatorname{At}(v)\ \land\ \forall z\,\neg(z\in v).\] It has exactly the empty set as its solution in \(D\). Indeed a nonempty set in \(D\) has a member in \(D\) by membership transitivity, while the non-atom conjunct excludes urelements.

Proof. Fix \(\psi\) first. Choose the integer \(q\) from Lemma 29 and the width \(m\) from Lemma 30. For each \(L\), put \[s=\left\lceil2L(q\log_3N+1)^2\right\rceil+1, \qquad M=\lfloor L^{7/4}\rfloor.\] For \(i\in\{0,1\}\), let \(D_{L,i}^{(s)}\) consist of the objects of \(\operatorname{HF}(A_{b^i})\) such that the object and each recursive member have a \(K\)-support of length at most \(s\). Give this domain membership, the atom predicate, and the original input relations, false whenever any argument is not an atom.

The family \(\mathcal T_\psi(A_{b^i})\) is \(H\)-invariant, membership-transitive and of size at most \(N^q\), for large \(L\). Corollary 17 therefore gives \[\mathcal T_\psi(A_{b^i})\subseteq D_{L,i}^{(s)}.\] The domain is membership-transitive and contains all atoms and pure HF sets: an atom supports itself, and a pure set is fixed by every atom permutation. Thus it satisfies all the domain requirements of Lemma 30.

For the fixed \(q,m\), Corollary 23 supplies all the quantitative hypotheses of Theorem 24 on sufficiently large grids: the two analytical expansions are \(C^M\)-equivalent, equal \(C^M\) types of tuples of length at most \(\max\{2,m\}s\) determine \(K\)-orbits, and \(\max\{4,m+1\}s\le M\). These are nonempty finite structures in the same binary vocabulary, and \(K\) acts by automorphisms of both expansions.

The supported domains computed from the expansions have the same underlying sets \(D_{L,i}^{(s)}\), since supports depend on the atom action of \(K\), which did not change. The theorem gives \(C^m\) equivalence with the additional analytical relations; forgetting those relations gives \[D_{L,0}^{(s)}\equiv_{C^m}D_{L,1}^{(s)}.\] The larger group \(H\) was used only on the original input and its evaluation family. No assertion that \(H\) preserves the analytical expansion is needed.

Both inputs have size \(N\), so the same formula \(\widehat\psi_N\), with the same numerical cutoffs and ordinal predicates, describes their evaluations. Lemma 30 and the displayed \(C^m\) equivalence therefore give equal truth values for \(\psi\) on the two inputs. All inequalities hold eventually in \(L\) after fixing \(\psi,q,m\), which proves the quantified assertion. ◻

Proof of Theorem 1. Let \(\Phi\) be the single sentence constructed in Section 4, over the eight-relation vocabulary \(\tau\) and with its fixed polynomial annotation. It has one syntactic WSC occurrence, and Proposition 8 gives a Boolean value on every finite \(\tau\)-structure. Let \(Q\) be its true-model class. By Theorem 13, for every \(L\ge2\), \[A_{b^0}\in Q,\qquad A_{b^1}\notin Q.\] If a CPT sentence \(\psi\) defined \(Q\), it would have opposite truth values on every such pair. This contradicts Theorem 31 for large \(L\). Finally, the non-strict inclusion follows from the inclusion of CPT syntax in CPT+WSC. Thus \[\operatorname{Def}_{\mathrm{CPT}}(\tau) \ \subsetneq\ \operatorname{Def}_{\mathrm{CPT}+\mathrm{WSC}}(\tau).\] ◻