Witnessed symmetric choice is strictly stronger than choiceless polynomial time with counting

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 \F^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 (3.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 (3.7) and nonemptiness. The block bounds follow from Equation (3.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

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 \F, this is Equation (3.10).□

Proof. For each edge e, the restriction map

is a homomorphism: the e-coordinate of B(a,a') is exactly the correction in the product on P_e. Equation (3.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

Here the first term vanishes because k\in K, and every inner sum vanishes by Equation (3.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 \Ed,\Cf,\EB,\VB. The coordinatewise definition on configurations proves preservation of \Inc. For the remaining relations, let g,g'\in P_e be two edge states and p=\rho_e(a,k). The group identity

shows that their corrected scalar difference in Equation (3.4) is unchanged. Thus every \Zrel_\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 (3.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 (3.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

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

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 (4.9) 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 4.2, 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+|\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

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,\Atoms satisfy the bound. The primitive functions \Pair,\Union,\Unique,\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 \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 (4.14) 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 4.2 verifies every required witness using automorphisms of the entire input, including all three \Zrel_\delta relations, and respecting every earlier state. Lemma 4.3 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 (4.12) and Lemma 4.1 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 3.1. 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 ith 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),

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

The coefficient \epsilon_{vh} is 1 or -1, so it is invertible in \F. We have constructed a configuration in X_v incident with both given atoms. This proves Equation (5.1) 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 \F^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 (5.2).□

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

Let \ell=h_{a,0} be the automorphism from Proposition 3.3. 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 (3.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 3.1 give

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 (5.3) 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

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\F. 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\F^{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

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 5.2 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 \Zrel_{\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 3.3, 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 (5.5), 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 (5.4) and (5.5) 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 (5.3). 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

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 5.1, both inputs pass the check and have a nonempty parameter set. Fix any \alpha\in P and any terminal selection x. Proposition 5.3 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\F^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

Every edge contributes once with each sign, and \sum_v b^0_v=0; therefore \sum_v r_v=0. Lemma 5.4 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 4.1, the output test accepts x.

Now work in A_{b^1}. If the output test accepted x, Lemma 4.1 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

a contradiction. Thus every terminal selection is rejected.

The witness and resource conclusions of Proposition 4.4 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

where empty sums are zero. Then r^{(1)}_1=0. The face orientation +1,+a,-1,-a gives

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

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

The function \varphi_3 is independent of i,j, so

All three gradient subtractions preserve curl. On the selected slice the 23 curl identity therefore becomes

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 (6.1) and (6.2) remain valid for r. Consequently

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

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 \F, and hence are vector subspaces. Define

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

Consider the annihilator

where K^* is the linear dual of K. Each \lambda\in K^* extends to a linear functional on \F^E: extend a basis of K to one of \F^E and assign arbitrary values on the additional basis vectors. The standard coordinate pairing thus gives an edge cochain \ell with

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 (3.10) therefore implies

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 [5, Sections 3.1 and 3.3]. Equation (6.4) 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

Lemma 6.2 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

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 (3.11) fixes that atom exactly when k_e=0. Consequently K_\alpha\subseteq K_0\subseteq S, so \alpha supports x and satisfies (6.5). 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 6.3 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 3.1 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

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,

where the last inequality uses |R|\le L^3/2.□

Proof. Sum Lemma 7.1 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

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\F^E and a vertex w in the giant of G\setminus T such that

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 \Zrel_\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 (7.3).

Forgetting an assigned position preserves compatibility. Its touched edges may disappear from T, and Lemma 7.2 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 7.2, both w and w_J lie in the giant of G\setminus T. Choose a signed path vector p_J supported outside T with

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 (7.3) 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

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 (7.4).

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 7.1 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 7.4.

Each preorder class is defined with two variable names. If h is the number of atoms in strictly earlier classes, its predicate is

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 \Inc(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 (7.6). 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 (7.5) 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\F: 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 7.4, a component U of G\setminus T has

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. 1.

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

2. 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. 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 (7.6). 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

Both configurations at v have divergence b_v, so

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

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 (7.5) is

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 7.2 and Proposition 7.3 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

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 (8.2). 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

Every y\in x belongs to \phi*\alpha. Conversely, a member of \phi*\alpha has the form \psi_y*\beta with

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 8.2, the matching prefix (\alpha,\beta) can be extended by \gamma so that

Thus \theta*\gamma\in\phi*\alpha=\psi*\beta. Choose its membership witness (\xi,\sigma)\in\psi and \zeta with

Extend the primed prefix of length 3s once more, obtaining \zeta' such that

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

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

define X_{\phi,\tau}(P') in B_1 similarly. Lemma 8.2 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

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

Projection preserves each label condition, and Lemma 8.4 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 8.2. The map

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

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 8.4 determines the second. By Lemma 8.2, 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

By Lemma 8.3, 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

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 8.4, forces x'=x'_j. This also proves consistency when retained values repeat.□

Proof of Theorem 8.1. 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 8.4. Atomhood is determined by the form. For a repeated variable, x=x is always true and x\in x always false in \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 8.5 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 9.1, 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

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

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.

Ordinals and the elementary operations. There are two-variable formulas O_k(v) defining the pure von Neumann ordinal k, for every fixed nonnegative integer k:

All pure ordinals belong to D. Induction on k, membership transitivity and extensionality show that O_k has exactly the claimed solution. The two names alternate in the recursion: inside O_j(z), the old name v can be bound, since that child formula has only z free.

Variable graphs are equalities with their corresponding arguments. The graphs for \emptyset and \Atoms are respectively E(v) and

For evaluated arguments a,b, the graphs of Pair and Union are

Put

The graph of Unique is

These are graphs of the operations, not assertions that their outputs are atoms or that their inputs are sets. They give the specified defaults on atoms as well.

The graph of Card on the actual argument a is

Every member of a belongs to D, so the quantifier counts its actual members. Its actual cardinality is at most J, and therefore one and only one disjunct yields an output.

For a composite term, existentially bind the outputs of its child terms and apply the appropriate operation graph. By the induction hypothesis, these intermediate outputs are forced to be their genuine values among all elements of D. Membership transitivity then makes each displayed extensional graph exact among all possible proposed outputs. The graph for an input relation applied to terms is obtained in the same way; for equality use equality of their outputs. Translate Boolean connectives by the corresponding Boolean connectives.

Comprehension. Suppose

Its graph is

At an actual parameter tuple, w must be the actual range. Each of its members activates the condition. When the condition is true, that member also activates the body, whose graph has exactly its correct output by induction. When the condition is false, the conjunction is false without any correctness requirement on the body graph at that unused argument tuple. This proves that the right-hand side of the membership biconditional defines exactly the actual collected values. An alternative output set with an extra member is also excluded: that member lies in D and is tested by the universal quantifier. The non-atom condition excludes an atom as a spurious empty output.

The transitive-size guard. For positive integers \ell, define strict downward path formulas

Three variable names suffice for all \ell: the endpoints and one intermediate name, with the former root name recycled inside the child formula. Set

For every actual value a under consideration, its solutions in D are exactly \TC(a). All descendants belong to D, and the chosen depth bound reaches every descendant. The paths have positive length; they do not count the root merely by a path of length zero. Exact counting counts endpoints, not paths, even if a descendant is reached in several ways.

For an iteration bound p, the formula

therefore says exactly |\TC(r)|\le P(n) on every actual candidate. It also handles atoms and \emptyset, whose strict transitive closures are empty. Its behavior on unrelated objects of greater depth is not needed.

Iteration and the empty default. Consider a term t=s[y]^*, with free parameters \bar x, and let S(\bar x,w,v) be the already constructed graph for its step term. At the present input size abbreviate P=P(n) and \operatorname{Ok}=\operatorname{Ok}_{p,n}. Define finite formulas

Let

For P=0 the disjunction has its j=0 term: a single step still tests whether the initial empty state is stationary.

We verify this graph for an actual parameter tuple \bar a. Induction on j shows that before stopping, I_j(\bar a,v) has exactly the genuine state a_j as its solution if all states through that index pass the size guard. At an admitted state, the step activation is actual. Its graph has exactly its actual candidate as output over the whole of D, by the syntax induction hypothesis. This candidate is in D, including when it is the first excessive one. The exact guard either admits that candidate or makes I_{j+1} have no solution. In the latter case all subsequent I’s have no solution, so no unrelated state can enter later.

If an allowed stationary state is reached early, all subsequent I_j repeat that same state. The step graph is still exact there because this argument tuple was already an actual activation. If no earlier stop occurs, the test S(\bar a,a_P,a_P) uses the actual final candidate a_{P+1}, which was included in the evaluation family. It succeeds exactly when stationarity is reached at index P. Thus F is empty when the bounded iteration fails, and otherwise its only output is the genuine stationary value. The final displayed formula returns precisely that value or the typed empty default. This proves the term part of (9.1). In particular, a fixed point at some argument tuple that was never activated cannot supply an extra output: every successful disjunct first requires a state reached from I_0.

One fixed supply of variable names. All formulas above are finite at fixed n. It remains to show that their variable width is bounded independently of n. For each syntax occurrence, reserve its finitely many argument names, an output name when it is a term, and finitely many names for the intermediate outputs and local quantifiers in its displayed construction. Child formulas receive their indicated free interface and a separate working supply, renamed to avoid capture. Since the syntax tree is fixed, the sum of these finite reservations depends only on \psi.

The only repetitions whose depths grow with n are the ordinal, membership-path and iteration expansions. The first two use the recycled interfaces already described. In the iteration recursion, retain \bar x and two state names. When I_j(\bar x,w) is inserted in the formula for I_{j+1}(\bar x,v), its internal quantifier may bind the name v: the later state is not free in that child. This binder has scope only inside I_j, so it does not capture v in the sibling formula S(\bar x,w,v). The step graph uses a separate fixed working supply. Repeating the recursion therefore does not keep a tuple of all previous states. Identified slots such as S(\bar x,v,v) can, if needed, use a fresh local alias constrained equal to v.

This argument applies at every syntax level, including inside step terms that themselves contain iterations. Nesting depth adds only a fixed number of reservations. Let m bound their total number. Taking the translated truth formula at the top sentence gives \widehat\psi_n, and (9.1) at the empty assignment proves the claim.□

Proof. Fix \psi first. Choose the integer q from Lemma 9.1 and the width m from Lemma 9.2. For each L, put

For i\in\{0,1\}, let D_{L,i}^{(s)} consist of the objects of \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 6.4 therefore gives

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 9.2.

For the fixed q,m, Corollary 7.6 supplies all the quantitative hypotheses of Theorem 8.1 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

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 9.2 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.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 4.4 gives a Boolean value on every finite \tau-structure. Let Q be its true-model class. By Theorem 5.5, for every L\ge2,

If a CPT sentence \psi defined Q, it would have opposite truth values on every such pair. This contradicts Theorem 9.3 for large L. Finally, the non-strict inclusion follows from the inclusion of CPT syntax in CPT+WSC. Thus

□