The separating query

Throughout, let \(\mathbb F=\mathbb F_3\). Fix the binary relational vocabulary \[\tau=\{\mathsf{Ed},\mathsf{Cf},\mathsf{EB},\mathsf{VB}, \mathsf I,\mathsf Z_0,\mathsf Z_1,\mathsf Z_2\}.\] The subscripts on the last three relation symbols denote elements of \(\mathbb F\). For a finite \(\tau\)-structure \(A\), set \[Y=\{y\in A:\mathsf{Ed}(y,y)\},\qquad X=\{a\in A:\mathsf{Cf}(a,a)\},\qquad X_t=\{a\in X:\mathsf{VB}(t,a)\}\quad(t\in X).\] No disjointness or equivalence-relation assumption is imposed here. In particular, \(X\) and \(Y\) may overlap. Define, in \(\mathbb F\), \[ C(y,a)=\sum_{\substack{x\in Y\\\mathsf I(a,x)}} \ \sum_{\substack{\delta\in\mathbb F\\ \mathsf Z_\delta(y,x)}}\delta \qquad(y\in Y,\ a\in X). \tag{1}\] If several of the relations \(\mathsf Z_\delta(y,x)\) hold, all their contributions are included.

Introduce two separate families of unknowns, \((\lambda_a)_{a\in X}\) and \((\mu_y)_{y\in Y}\). Thus even when \(a=y\), \(\lambda_a\) and \(\mu_y\) are different unknowns. The system defining our query has the equations \[ \sum_{a\in X_t}\lambda_a=1\qquad(t\in X) \tag{2}\] and, for every \((t,y)\in X\times Y\) for which \[ \text{there exist $a\in X_t$ and $x\in Y$ with $\mathsf I(a,x)$ and $\mathsf{EB}(y,x)$,} \tag{3}\] the equation \[ \mu_y=\sum_{a\in X_t}\lambda_a C(y,a). \tag{4}\] Let \(Q(A)\) mean that this system is consistent over \(\mathbb F\). Repeated identical equations are harmless; they remain equations and are not added together. An empty sum is zero, and a system with no equations is consistent. These conventions make \(Q\) a query on all finite \(\tau\)-structures.

Main result

Theorem 1 confirms the noncapture conjecture of Blass, Gurevich and Shelah for the full counting formalism; its historical formulation is discussed below. We first record the ordinary algorithmic upper bound. The rest of the paper proves the choiceless lower bound.

The same query is expressible in two standard linear-algebraic logics. Following Grädel and Pakusa (Grädel and Pakusa 2019, sec. 2), write \(\mathrm{FPS}_3\) for fixed-point logic with counting (FPC) extended by the solvability operator over \(\mathbb F_3\), and \(\mathrm{FPR}_3\) for FPC extended by the rank operator over \(\mathbb F_3\). Their two-sorted syntax allows bounded number variables alongside the unordered input elements. We state the consequence for nonempty structures, so that the matrix index sets in its proof are nonempty.

FPC defines the coefficient predicates and the row test for \(Q\). Section 8 gives the resulting solvability formula and compares the ranks of the coefficient and augmented matrices. The nonempty witnesses constructed below give both noncontainments.

Background and the obstruction to rank-dependent arguments

The ordered case provides the starting point. Immerman and Vardi showed that first-order logic with a least fixed-point operator expresses exactly the polynomial-time queries on finite structures supplied with a linear order (Immerman 1982; Vardi 1982). For unordered structures, Chandra and Harel asked whether polynomial-time queries admit an effective enumeration (Chandra and Harel 1982, sec. 5, p. 118). Gurevich formulated the question in terms of a logic capturing polynomial time and conjectured that no such logic exists (Gurevich 1988, sec. 7). Excluding CPT with counting as a candidate leaves this broader question open.

Blass, Gurevich and Shelah introduced choiceless polynomial time to study computation on unordered structures using hereditarily finite sets rather than arbitrary choices of an ordering (Blass et al. 1999). Their original 1997 preprint explicitly conjectured that the extension by counting is still a proper fragment of polynomial time (Blass et al. 1999, 1997 version, Introduction, p. 3). Their later study of unordered computation examined CFI instances and finite-field linear algebra as possible sources of separation, carefully distinguishing representations with common and independent row and column index sets (Blass et al. 2002, sec. 4 and 6). The query here is a particular linear-consistency problem over \(\mathbb F_3\), defined without a promise on the input structure.

Shelah’s early work claimed noncapture for counting extensions of choiceless computation (Shelah 2000, Introduction and Section 4). Later accounts continued to state the capture problem as open, from Blass, Gurevich and Shelah (Blass et al. 2002, sec. 7) through the 2025 work of Dawar, Grädel, Kullmann and Pago (Dawar et al. 2025, sec. 2.2). We give a separate proof for the explicit query above; Shelah’s claim is not a theorem input to this argument.

The construction of Cai, Fürer and Immerman established the central example of a polynomial-time graph query beyond fixed-point logic with counting (Cai et al. 1992). Its local gadgets conceal a global parity obstruction from bounded-variable counting formulas. This is an antecedent of our charge-based witnesses, not an identification of those witnesses with the original CFI graphs. The passage from counting logic to choiceless computation is substantial: Dawar, Richerby and Rossman showed that the preordered CFI query obtained from ordered base graphs is definable without counting, while even counting does not suffice if set rank is restricted to \(o(\log n/\log\log n)\), where \(n\) is the input size (Dawar et al. 2008, Theorems 17 and 40, 2007 author version). In particular, their lower bound for every fixed rank cannot by itself yield a separation for the full formalism. Pakusa, Schalthöfer and Selman extended the positive result to connected preordered base graphs whose colour classes have logarithmic size in the number of base vertices (Pakusa et al. 2016, Theorem 1). The preorder orders classes of base vertices, rather than all vertices of the resulting CFI structure.

Positive algebraic results also go beyond the original CFI family. Abu Zaid, Grädel, Grohe and Pakusa obtained choiceless canonization, that is, construction of canonical ordered copies, when a supplied preorder has bounded classes whose induced substructures have Abelian automorphism groups (Abu Zaid et al. 2014, Corollary 19). Their procedure uses specially structured cyclic systems of equations, not arbitrary unordered linear systems (Abu Zaid et al. 2014, Definition 6 and Theorem 14). Lichter and Schweitzer obtained analogous canonization for graphs when these induced groups are dihedral or cyclic (Lichter and Schweitzer 2021, Theorem 1). These results show why the lower-bound argument must exploit the particular action of its nonabelian group, rather than noncommutativity alone.

Functional lower bounds expose different limits. Rossman proved that CPT with counting cannot construct the set of hyperplanes of an input finite vector space over a fixed finite field (Rossman 2010, Theorem 6.1, author version). Pago proved that no such program constructs, on every hypercube with \(N\) vertices, a total preorder with classes of size \(O(\log N)\) (Pago 2021, Theorem 2 and Corollary 3, full version). The latter statement also excludes encodings from which the preorder can be recovered in CPT. It obstructs the route of first constructing a fine preorder and then applying the preordered CFI algorithm. These are functional obstructions, not nondefinability of a Boolean query.

Pago’s symmetric-XOR-circuit approach relates restricted classes of choiceless CFI algorithms to circuit families (Pago 2023, Theorems 2, 31 and 33, full version). The translation permits polynomially many circuit images under automorphisms of the base graph; the circuit lower bound assumes an invariant circuit and different bounds on connections between gates. These hypotheses differ, so that argument does not establish nondefinability for the entire restricted algorithm class.

The support-and-transfer architecture has older roots. Blass, Gurevich and Shelah developed supports and representations by forms evaluated at supporting tuples, called molecules (Blass et al. 1999, secs. 8–9, published version). Dawar, Richerby and Rossman developed rank-sensitive support bounds and a counting transfer for hereditarily supported objects (Dawar et al. 2008, secs. 7–8, 2007 author version). Using the group-relative homogeneity from Section 4, we adapt that representation method in Section 5 and prove the required exact counting statements. The support estimate in Section 3 instead uses a larger nonabelian group to obtain small supports for its central subgroup, independently of HF rank. Its standard class-two group and alternating-form ingredients, as well as the projection and counting-game methods used for the atom comparison, are credited at their respective proofs. The grid-specific estimate and the quantitative transfer are proved here.

Finally, the connection to arbitrary programs uses the interpretation characterization of Grädel, Pakusa, Schalthöfer and Kaiser (Grädel et al. 2015, Theorem 1). We use the binary, two-dimensional formulation of Grohe, Schweitzer and Wiebking (Grohe et al. 2021, sec. 6, Theorem 18, arXiv version 1), including its generated-equivalence and existential-representative quotient convention. This characterization is an external input. Section 6 proves the further facts needed here: a polynomial bound on the complete hereditary encoding of a run, and exact formulas for its states whose variable bound is independent of the number of stages. Thus neither a bound on HF rank nor a restriction to a particular algorithmic construction is imposed on the programs excluded by the theorem.

Proof overview

For each side length \(L\), we build two structures from the three-dimensional box grid. Each edge carries states consisting of a bounded collection of \(\mathbb F_3^2\) face coordinates and one scalar. A vertex configuration chooses incident edge states that agree on their shared face coordinates and whose scalars have a prescribed signed sum, called its charge. Both kinds of states become input atoms, linked only by the fixed binary relations. The two structures have all charges zero, or one charge equal to one. Their size is \(N=\Theta(L^3)\). The query’s normalization equations assign field-valued weights summing to one to the configurations at each vertex. Its consistency equations make the weighted scalar value of an edge agree at its two endpoints. Summing the vertex divergence equations then forces the total charge to be zero, since each edge enters one vertex and leaves another. This argument allows arbitrary field-valued weights; it does not assume that a solution selects one configuration per vertex. The all-zero configurations give a solution in the zero-charge structure, so the query has opposite answers on the pair.

The challenge is to show that every fixed full \(\mathrm{CPT}\) program eventually gives the same answer on this pair. Three steps connect the symmetries of these atoms to the complete computation.

Grid orientations and edge groups

For an integer \(L\ge2\), let \(G=(V,E)\) be the box grid with \[V=\{0,\ldots,L-1\}^3.\] Each edge is oriented in its positive coordinate direction. Put \(\epsilon_{ve}=1\) if \(v\) is the head of \(e\), \(\epsilon_{ve}=-1\) if it is the tail, and \(\epsilon_{ve}=0\) otherwise. The incidence map is \[\partial:\mathbb F^E\longrightarrow\mathbb F^V, \qquad (\partial z)_v=\sum_{e\in E}\epsilon_{ve}z_e.\] Let \(F\) be the set of unit square faces. A face parallel to coordinate directions \(i<j\) is traversed first in direction \(+i\), then \(+j\), then \(-i\), then \(-j\). Its edge vector \(c^f\in\mathbb F^E\) has coefficient \(1\) when this traversal follows an edge orientation, \(-1\) when it opposes that orientation, and zero off the face. At each vertex of the face one traversed edge enters and one leaves, so \[ \partial c^f=0. \tag{5}\] Write \(F(e)=\{f\in F:c^f_e\ne0\}\), and let \(F(v)\) be the set of faces containing \(v\). We shall use \[|F(e)|\le4,\qquad f(v):=|F(v)|\le12, \qquad d(v):=|\{e:e\ni v\}|\le6.\] In particular, \(d(v)\ge1\).

For vectors in \(\mathbb F^2\), define the alternating form \[\omega((a,b),(a',b'))=ab'-ba'.\] The edge groups use the standard finite Heisenberg multiplication (Gurevich and Hadani 2009, sec. 2.1), with the face-boundary signs specifying its alternating form. The group \(P_e\) attached to an edge \(e\) has underlying set \((\mathbb F^2)^{F(e)}\times\mathbb F\). Its elements are written \((u,z)\), where \(u=(u_f)_{f\in F(e)}\), and its product is \[ (u,z)(u',z')= \left(u+u',\ z+z'+\frac12 \sum_{f\in F(e)}c^f_e\omega(u_f,u'_f)\right). \tag{6}\] Here \(1/2=2\) in \(\mathbb F_3\). To verify the group law, denote the bilinear correction term by \(B_e(u,u')\). Bilinearity gives \[B_e(u,u')+B_e(u+u',u'') =B_e(u',u'')+B_e(u,u'+u''),\] which is exactly associativity. Alternation gives \(B_e(u,u)=0\); hence \((0,0)\) is the identity and \((u,z)^{-1}=(-u,-z)\). In particular, the last coordinate of \((u,z)^{-1}(u',z')\) is \[ z'-z-\frac12\sum_{f\in F(e)}c^f_e\omega(u_f,u'_f). \tag{7}\]

Atoms and binary relations

Fix \(b=(b_v)_{v\in V}\in\mathbb F^V\). The universe of \(A_b\) is the disjoint union of two kinds of atoms. There is an edge atom \((e,u,z)\) for each edge \(e\) and each \((u,z)\in P_e\). At each vertex \(v\) there is a configuration atom for every tuple \[a=\bigl(v,((u_e,z_e))_{e\ni v}\bigr)\] satisfying \[ \begin{aligned} u_{e,f}&=u_{e',f} &&\text{for the two edges $e,e'$ of each face $f\in F(v)$ at $v$},\\ \sum_{e\ni v}\epsilon_{ve}z_e&=b_v. \end{aligned} \tag{8}\] The coordinates in these descriptions label atoms; they are not members of the atoms as sets. The two kinds of atoms are tagged so they are disjoint.

Figure 2 illustrates the signed face boundary in (5) and the shared-coordinate condition in (8).

The vocabulary \(\tau\) is interpreted as follows; each relation is false on all pairs not specified below.

• \(\mathsf{Ed}\) and \(\mathsf{Cf}\) are the diagonals of the edge atoms and configuration atoms, respectively.

• \(\mathsf{EB}\) relates edge atoms on the same edge. The relation \(\mathsf{VB}\) relates configuration atoms at the same vertex.

• \(\mathsf I(a,x)\) holds when \(a\) is a configuration at a vertex \(v\) and \(x=(e,u_e,z_e)\) is the state selected by \(a\) on an incident edge \(e\).

• For \(\delta\in\mathbb F\), the relation \(\mathsf Z_\delta((e,u,z),(e,u',z'))\) holds precisely when (7) equals \(\delta\).

Thus \(\mathsf I\) goes from configurations to edge atoms; it is not made symmetric. The coordinate labels used to construct \(A_b\) are not extra symbols in its input vocabulary. In particular, no ordering of the grid or of its blocks is supplied to a program.

Opposite answers

Fix any vertex \(v_*\in V\), and put \[b^0=0,\qquad b^1=\mathbf1_{v_*}.\] These two charge vectors give structures of the same size by Lemma 4.

The remainder of the argument shows that a fixed choiceless computation cannot distinguish these two structures when \(L\) is sufficiently large. The equality of their universe sizes and the fixed binary vocabulary will be used throughout that argument.

A central extension acting on the structures

For \(a,a'\in C_F\), define an edge vector \[B(a,a')=\frac12\sum_{f\in F}\omega(a_f,a'_f)c^f\in K.\] On the set \(H=C_F\times K\), define \[ (a,k)(a',k')=(a+a',k+k'+B(a,a')). \tag{10}\] Bilinearity gives \(B(a,a')+B(a+a',a'')=B(a',a'')+B(a,a'+a'')\), proving associativity. The identity is \((0,0)\); since \(B(a,a)=0\), the inverse of \((a,k)\) is \((-a,-k)\). Thus \(H\) is a finite group. The subgroup \(\{0\}\times K\), identified with \(K\), is central, and the projection \(H\to C_F\) is a surjective homomorphism with kernel \(K\). With the convention \([h,h']=hh'h^{-1}(h')^{-1}\), its commutator is \[ [(a,k),(a',k')]=\left(0,\sum_{f\in F} \omega(a_f,a'_f)c^f\right). \tag{11}\]

Recall that an edge atom on \(e\) has a state \((u,z)\) in \(P_e\), with \(u=(u_f)_{f\in F(e)}\). The element \((a,k)\in H\) sends that state to \[ \left(u+(a_f)_{f\in F(e)},\; z+k_e+\frac12\sum_{f\in F(e)}c^f_e\omega(a_f,u_f)\right). \tag{12}\] It acts on a configuration by applying this map to every incident edge state. This is an action because restricting \((a,k)\) to an edge is a homomorphism from \(H\) to \(P_e\), and the edge action is left multiplication.

Every permutation of the atoms extends to hereditarily finite objects by \(h\cdot x=\{h\cdot y:y\in x\}\) for sets \(x\), recursively in their rank. Atoms remain distinct from sets. We always use this extension of the \(H\)-action. A tuple \(\alpha\) of atoms is a \(K\)-support of an object \(x\) if every element of the pointwise stabilizer \[K_\alpha=\{k\in K:k\cdot\alpha_i=\alpha_i\text{ for every }i\}\] fixes \(x\). The empty tuple is permitted and has stabilizer \(K\).

A sparse representative for an edge functional

A central element \(k\in K\) fixes an edge atom on \(e\) exactly when \(k_e=0\). To obtain a short support for an object \(x\), it suffices to find a small edge set \(T\) such that every \(k\in K\) vanishing on \(T\) fixes \(x\). The stabilizer of \(x\) in \(K\) is a vector subspace, so it can be described by linear equations on \(K\). We will represent these equations using few edge coordinates.

An edge cochain is a vector \(\ell\in\mathbb F^E\). Its face curl is \[(D\ell)(f)=\sum_e c^f_e\ell_e.\] A vertex function \(\varphi\in\mathbb F^V\) has gradient \(\partial^{\mathsf T}\varphi\), whose value on an edge from \(v\) to \(w\) is \(\varphi(w)-\varphi(v)\). Adding a gradient does not change the curl, because \(\partial c^f=0\). It also does not change the linear functional \(k\mapsto\sum_e\ell_e k_e\) on \(K\). The next lemma shows that a cochain with few nonzero face curls can be replaced by one using few edges, without changing its functional on \(K\). In the support proof, commutators will supply the bound on the number of these faces.

The support bound

The argument used \(x\) only through its stabilizer subgroup \(S\le H\). Its rank plays no role in the support bound.

A family \(\mathcal X\) is membership-transitive if \(y\in x\in\mathcal X\) implies \(y\in\mathcal X\). Thus it contains every recursive constituent of each of its members.

An expansion for the analysis

Recall that an edge atom has coordinates \((e,u,z)\), whereas a configuration atom at \(v\) specifies the states on all incident edges, subject to the face compatibility equations and the divergence equation with right side \(b_v\). Expand \(A_b\) to a structure \(\bar A_b\) as follows. Partition its universe into classes indexed by \[(e,u)\quad\text{and}\quad(v,(u_f)_{f\in F(v)}).\] Here \(u_f\) is the common face coordinate on the two edges of \(f\) at \(v\). Thus an edge class leaves only \(z\) unspecified, and a configuration class leaves all incident \(z\)-coordinates unspecified. Choose a linear order of these class labels, the same for all charge assignments, and let \(\preceq\) be the resulting total preorder on atoms. Each edge class has size \(3\), and a configuration class at \(v\) has size \(3^{d(v)-1}\); in particular, corresponding classes are nonempty and have the same size. Finally add, for \(\delta\in\mathbb F_3\), the relation \[\mathsf D_\delta((e,u,z),(e',u',z')) \quad\Longleftrightarrow\quad e=e'\ \text{and}\ z'-z=\delta,\] which is false on every other pair. The vectors \(u,u'\) need not agree in this definition. The preorder will let counting formulas identify a block and its face coordinates. The relations \(\mathsf D_\delta\) will compare scalar differences on the same edge, including between different face patterns.

Every element of \(K\) preserves the expansion. The larger group \(H\) need not preserve it. Crucially, the preorder and the relations \(\mathsf D_\delta\) are tools for this proof and are not part of the input to a choiceless program.

Write \(C^h\) for first-order logic with equality, ordinary quantifiers and exact counting quantifiers \(\exists^{=a}x\), using at most \(h\) variable names. Here \(a\) may be any nonnegative integer. Formula length and these integer constants need not be uniform in \(L\). The \(C^h\)-type of an \(r\)-tuple, for \(r\le h\), records all such formulas with free variables among its \(r\) designated positions. Coordinates of a tuple may repeat.

A component that survives edge deletions

Let \(G\) be the undirected graph underlying the oriented box grid on \(V=\{0,\ldots,L-1\}^3\). For \(R\subseteq V\), write \(\delta_G R\) for its edge boundary; this notation distinguishes the boundary of a vertex set from the incidence operator \(\partial\). The projection estimate below is the three-dimensional discrete Loomis–Whitney inequality (Loomis and Whitney 1949). We include its short proof and derive the needed finite-box boundary bound.

Set \[M=\lfloor L^{7/4}\rfloor.\] For all sufficiently large \(L\), deleting any set \(T\) of at most \(6M\) edges leaves a unique component containing more than \(L^3/2\) vertices. Call it the giant component. Indeed, summing the preceding lemma over all components \(R\) of size at most \(L^3/2\) gives \[ \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{15}\] The middle inequality uses \(\sum_R|\delta_G R|\le2|T|\) and \(\sum_i a_i^{3/2}\le(\sum_i a_i)^{3/2}\) for nonnegative \(a_i\). If every component had size at most half, the left side would equal \(L^3\), a contradiction. Two components cannot both have more than half the vertices. Moreover, whenever more edges are deleted within this range, the new giant is contained in the old one: each new component is contained in an old component, and its size identifies that old component as the giant.

Moving the unmatched charge

The counting argument follows the finite-variable counting-game method of Immerman and Lander (Immerman and Lander 1990, Counting Quantifiers) and the charge-moving strategy of the CFI construction (Cai et al. 1992, Lemma 6.2 and proof of Theorem 6.4). Here we construct the required bijections and prove formula preservation directly; no game characterization is needed as a premise.

Recognizing the central-group orbits

For the next step, the two tuples lie in the same expansion. A shift prescribed on their touched edges must extend to a divergence-free vector. The only obstruction is a nonzero net prescribed flow across one of the remaining components.

For the support scale used below, fix \(q,m\) first and put \[s=\left\lceil2L(q\log_3 N+1)^2\right\rceil+1, \qquad N=\Theta(L^3).\] Uniformly for \(1\le r\le\max\{2,m\}s\), the left side of (18) is \[O_{q,m}\bigl(L^{3/2}(1+\log L)^3\bigr)=o(L^{7/4}).\] Consequently Proposition 13 applies throughout that range when \(L\) is sufficiently large. The same choice of \(L\) ensures \(\max\{4,m+1\}s\le M\), the separate width requirement for extending atom types in the hereditary-set comparison below. The exponent \(7/4\) simultaneously ensures \(M^{3/2}=o(L^3)\) for the giant-component estimate and \(L^{3/2}(1+\log L)^3=o(M)\) for homogeneity at the support scale. Any fixed exponent strictly between \(3/2\) and \(2\) would meet these asymptotic requirements. All these conclusions hold for fixed \(q,m\), chosen before \(L\).

Exact extension counts for atom types

All types in the next lemma are realized in \(A_0\) or \(A_1\). Thus there are only finitely many types of any fixed tuple length, even though a type records infinitely many formulas.

A common syntax for supported objects

A molecule is a tuple \(\alpha\in A_i^s\). It records a support, but need not be a minimal support. We describe sets by a common collection of formal expressions, independent of the side \(i\).

There are \(s\) atomic forms \(c_1,\ldots,c_s\). A set form is a finite set of pairs \((\psi,\rho)\), where \(\psi\) is a previously constructed form and \(\rho\) is a realized \(C^M\) type of length \(2s\) in \(A_0\) or \(A_1\). These are syntactic constructors: atomic forms are distinct from every set form, including the empty set form. A form has finite depth; set forms have greater depth than their constituent forms.

For a molecule \(\alpha\in A_i^s\), define the value of a form recursively: \[\begin{align*} c_j*\alpha&=\alpha_j, \tag{19}\\ \phi*\alpha&= \{\psi*\beta: (\psi,\rho)\in\phi, \ \beta\in A_i^s, \ \operatorname{tp}_M^{A_i}(\beta,\alpha)=\rho\} \quad\text{if $\phi$ is a set form}. \tag{20}\end{align*}\] This produces a finite set because both the form and the base universe are finite. The empty set form evaluates to the empty set.

Representation reduces arbitrary finite rank to finite syntax. We next show that the syntax can be evaluated on either base structure without changing equality or membership, provided the supporting molecules have the same joint type.

Matching entire domains while retaining parameters

An object may have several representations \(\phi*\alpha\). Thus equal counts of molecules do not by themselves give equal counts of objects. We will group represented values into stabilizer orbits and account for the number of molecules representing each value. This will give a bijection between the two domains after fixing the values of at most \(m-1\) variables. The construction is a mathematical comparison; it is not required to be definable or executable by a choiceless program.

Call paired assignments represented alike if their values have representations \[x_j=\phi_j*\alpha_j,\qquad x'_j=\phi_j*\alpha'_j \quad(1\leq j\leq r),\] using common forms, and the concatenated tuples \(P=(\alpha_1,\ldots,\alpha_r)\) and \(P'=(\alpha'_1,\ldots,\alpha'_r)\) have the same \(C^M\) type. Dropping a position preserves this condition by projection. Empty assignments are represented alike by the sentence-equivalence assumption.

Theorem 14 imposes no bound on the rank of an object or the depth of its representing form. The type-extension arguments require \(4s\leq M\) for equality transfer and \((m+1)s\leq M\) for the domain bijections. Orbit homogeneity is used at length \(2s\) for representation and at length at most \(ms\) when extending a retained assignment. These requirements are independent of rank. In the next section, the support theorem places every code and recursive constituent of a polynomial computation inside \(D_i\). We then construct bounded-variable halt and output sentences evaluated on \(D_i\), to which the transfer theorem applies.

The interpretation characterization

We use the binary-vocabulary formulation of the interpretation characterization of choiceless polynomial time with counting, due to Grohe, Schweitzer and Wiebking (Grohe et al. 2021, sec. 6 and Theorem 18, arXiv version 1), building on Grädel, Pakusa, Schalthöfer and Kaiser (Grädel et al. 2015, Theorem 1). Here counting includes the cardinality operation on hereditarily finite sets. We spell out the exact direction and interpretation convention used below.

An interpretation from one fixed binary relational vocabulary to another consists of fixed, parameter-free formulas \[\delta(x_1,x_2),\qquad \eta(x_1,x_2,y_1,y_2),\qquad \rho_R(x_1,x_2,y_1,y_2)\] in first-order logic with the Härtig quantifier. This quantifier compares the cardinalities of two sets of elements defined by formulas; the two formulas may have free variables in addition to their respective counted variables. On a finite structure with universe \(V\), the interpretation first forms \[D=\{(a_1,a_2)\in V^2:\delta(a_1,a_2)\}.\] Let \(\sim\) be the least equivalence relation on \(D\) containing every pair \((\bar a,\bar b)\) satisfying \(\eta(\bar a,\bar b)\). The new universe is \(D/{\sim}\), and \[R([\bar a],[\bar b]) \quad\Longleftrightarrow\quad \text{some }\bar a'\sim\bar a,\ \bar b'\sim\bar b \text{ satisfy }\rho_R(\bar a',\bar b').\] Thus the interpretation is defined even when \(\eta\) itself is not an equivalence relation or \(\rho_R\) is not constant on classes. This is the convention in (Grohe et al. 2021).

An interpretation program has one such initialization interpretation, one step interpretation, and fixed halt and output sentences in first-order logic with the Härtig quantifier. Write \(A_0=A\) for the input, \(A_1=I_{\rm init}(A_0)\), and \(A_{j+1}=I_{\rm step}(A_j)\) for \(j\ge1\). The halt sentence is first tested at \(A_1\). A deciding program halts at a stage \(h\ge1\), outputs the truth value of its output sentence there, and has \[h+\sum_{j=1}^{h}|V(A_j)|\] bounded by a fixed polynomial in \(|V(A)|\). The characterization says, in the direction needed here, that every property of finite binary relational structures definable in full choiceless polynomial time with counting is decided by such a program. The absence of parameters means that the fixed interpretations have no additional input-dependent distinguished tuple; it does not prohibit free tuple variables in their defining formulas.

Fix a deciding interpretation program \(P\). On our two inputs of the same size \(N\), choose a common integer \(B\ge2\) bounding \(N\), both halt stages, and every state size up to halt. We may take \(B\) to be a fixed polynomial bound depending only on \(P\).

A polynomial hereditary encoding

For objects \(a,b\) in the universe of hereditarily finite sets over the input atoms, use the Kuratowski pair \[\langle a,b\rangle=\{\{a\},\{a,b\}\}.\] This coding is injective in the ordered pair, including when \(a\) or \(b\) is an atom. Indeed the intersection of its members is \(\{a\}\), while their union is \(\{a,b\}\); after recovering \(a\), the latter set determines \(b\), also when \(a=b\).

Encode the vertices of \(A_0\) by the input atoms themselves. Suppose the vertices of \(A_{j-1}\) have already been encoded injectively. A vertex \(C\) of \(A_j\) is an equivalence class of domain pairs from \(A_{j-1}\). Define its payload and code by \[S_C=\{\langle a_1,a_2\rangle: (a_1,a_2)\text{ is a pair of previous codes representing }C\}, \qquad e_j(C)=\langle [j],S_C\rangle,\] where \([j]=\{[0],\ldots,[j-1]\}\) is the von Neumann ordinal. Distinct classes have disjoint, nonempty sets of representing pairs, so their payloads, and hence their codes, are distinct. The payload records the whole class, so its construction does not choose a representative. The ordinal tag distinguishes vertices created at different stages, and stage-zero codes are atoms rather than sets.

Since \(B\) is polynomial in \(N\), fix an integer \(q\ge1\), depending only on \(P\), such that \(9B^3\le N^q\) for all sufficiently large \(N\). Every \(H\)-orbit in the transitive trace family has at most \(N^q\) objects. Corollary 9 therefore gives \(K\)-supports of the common length \(s\) for every code and every recursive constituent. Thus the entire family lies in the corresponding supported domain \(\mathcal D_b\), including the payloads, all pair wrappers, and the ordinal tags. No bound on the rank of a code has been imposed: its nesting depth may grow throughout the computation.

Exact formulas for the encoded states

All formulas in this subsection are evaluated in \(\mathcal D_b\) with its membership relation and its atomic input relations. Its domain is transitive, contains all input atoms and all pure hereditarily finite sets, and consists of atoms and sets. Consequently \[\mathsf{Atom}(x):=\mathsf{Ed}(x,x)\vee\mathsf{Cf}(x,x), \qquad \mathsf{Set}(x):=\neg\mathsf{Atom}(x)\] distinguish these two kinds of objects.

Let \(U_0(x)=\mathsf{Atom}(x)\) and let the stage-zero relation formulas be the input relations. Suppose that the formulas for the preceding stage are exact: \(U(x)\) selects precisely its vertex codes, and its relation formulas describe exactly the state on those codes. Translate a fixed first-order formula with Härtig quantifiers by replacing state relation atoms by their defining formulas, retaining equality, and restricting ordinary quantifiers to \(U\). In particular, equality is equality of the injective vertex codes, including for repeated variable arguments. Replace a Härtig comparison of \(\chi_1(x)\) and \(\chi_2(y)\) by \[ \bigvee_{n=0}^{B} \left[ \bigl(\exists^{=n}x\,(U(x)\wedge\chi_1^*)\bigr) \wedge \bigl(\exists^{=n}y\,(U(y)\wedge\chi_2^*)\bigr) \right]. \tag{21}\] Both counted sets have size at most \(B\), so induction on formulas proves this translation exact, also when the state is empty. The superscript \(*\) will denote this translation.

For the initialization or step interpretation appropriate to the new stage, put \[\mathsf{Dom}(\bar a):=U(a_1)\wedge U(a_2)\wedge\delta^*(\bar a), \qquad \bar a=(a_1,a_2).\] On two domain pairs define \[\mathsf{Link}(\bar a,\bar b):= \mathsf{Dom}(\bar a)\wedge\mathsf{Dom}(\bar b)\wedge \bigl(\bar a=\bar b\vee\eta^*(\bar a,\bar b) \vee\eta^*(\bar b,\bar a)\bigr),\] where tuple equality abbreviates the two coordinate equalities. Define finite formulas recursively by \[\begin{split} \mathsf{Reach}_0(\bar a,\bar b)&:=\mathsf{Link}(\bar a,\bar b),\\ \mathsf{Reach}_{t+1}(\bar a,\bar b)&:= \mathsf{Reach}_t(\bar a,\bar b)\vee \exists\bar d\, (\mathsf{Reach}_t(\bar a,\bar d)\wedge \mathsf{Link}(\bar d,\bar b)). \end{split}\] This expresses paths of length at most \(t+1\) in the reflexive symmetric link graph. There are at most \(B^2\) domain pairs, so \(\mathsf{Reach}_{B^2}\) is exactly the generated equivalence relation, and is false if either endpoint is outside the domain.

The generated quotient is now defined. We next recognize its hereditary codes; transitivity will ensure that membership tests identify the actual sets, not merely their visible members. Write \[\mathsf{Sing}(u,a):=\mathsf{Set}(u)\wedge \forall w\,(w\in u\leftrightarrow w=a),\] and \[\mathsf{Double}(v,a,b):=\mathsf{Set}(v)\wedge \forall w\,(w\in v\leftrightarrow(w=a\vee w=b)).\] Then \[\mathsf{OP}(z,a,b):= \exists u\,\exists v\, (\mathsf{Sing}(u,a)\wedge\mathsf{Double}(v,a,b) \wedge\mathsf{Double}(z,u,v))\] expresses \(z=\langle a,b\rangle\) whenever that pair and its wrappers are present. Conversely every satisfying assignment gives the actual Kuratowski pair: transitivity ensures that the universally quantified membership tests cannot overlook a member outside the domain. Define the ordinal formulas by \[\mathsf{Ord}_i(o):=\mathsf{Set}(o)\wedge \forall w\left(w\in o\leftrightarrow \bigvee_{0\le h<i}\mathsf{Ord}_h(w)\right).\] The empty disjunction for \(i=0\) is false. All pure ordinals belong to \(\mathcal D_b\), and induction using transitivity shows that this formula selects precisely \([i]\).

For stage \(j\ge1\), define \[\begin{align*} \mathsf{Payload}_j(S,\bar a):={}& \mathsf{Set}(S)\wedge\mathsf{Dom}(\bar a)\\[-2pt] &{}\wedge\forall z\left(z\in S\leftrightarrow \exists\bar b\, (\mathsf{Dom}(\bar b)\wedge \mathsf{Reach}_{B^2}(\bar a,\bar b) \wedge\mathsf{OP}(z,b_1,b_2))\right),\\ \mathsf{Rep}_j(x,\bar a):={}& \exists o\,\exists S\, (\mathsf{Ord}_j(o)\wedge\mathsf{Payload}_j(S,\bar a) \wedge\mathsf{OP}(x,o,S)),\\ U_j(x):={}&\exists\bar a\,\mathsf{Rep}_j(x,\bar a),\\ R_j(x,y):={}&\exists\bar a\,\exists\bar b\, (\mathsf{Rep}_j(x,\bar a)\wedge\mathsf{Rep}_j(y,\bar b) \wedge\rho_R^*(\bar a,\bar b)). \end{align*}\] The stage subscripts on the formulas and on their auxiliary definitions are syntactic indices, not additional free variables.

A variable bound independent of the number of stages

The formulas just constructed may be extremely long. What matters for the transfer theorem is a different syntactic bound. For a formula \(\theta\), define \[\operatorname{fw}(\theta) :=\max_{\xi\text{ a subformula of }\theta}|\operatorname{FV}(\xi)|.\] Here free variables are counted relative to the subformula \(\xi\) itself. Thus a variable bound outside \(\xi\) is counted if it occurs freely inside \(\xi\).

Apply the lemma first to the fixed formulas of \(P\). Replacing a Härtig quantifier by (21) may repeat a subformula \(B+1\) times but does not increase its free-variable sets with \(B\); the finitely many program formulas therefore give a uniform bound for the translation templates. Pair coding, payloads, representatives, and domain and relation definitions also have fixed templates, with all free variables among their displayed arguments.

For example, the template for \(\mathsf{Reach}_{t+1}(\bar a,\bar b)\) uses only the endpoint pairs \(\bar a,\bar b\) and the quantified pair \(\bar d\). The inserted copy \(\mathsf{Reach}_t(\bar a,\bar d)\) exposes only its four endpoint arguments; \(\bar b\) occurs in the other conjunct, \(\mathsf{Link}(\bar d,\bar b)\), and is not a free parameter of that copy. Thus expansion takes the maximum of the previous width and the fixed template width, rather than adding the widths at successive levels. The same argument applies when a stage formula is inserted into the next stage’s template. The ordinal recursion has the simpler unary interface. Taking the maximum over these finitely many template widths and the bounds for the fixed formulas of \(P\) gives a constant \(w=w(P)\) for every fully expanded formula above. Unused or identified arguments can only reduce the number of free variables.

Set \(m=\max\{2,w+1\}\). Lemma 21 puts all the expanded state, halt, and output formulas in \(C^m\), independently of \(N\), \(B\), and the stage number. The numerical constants in the counting quantifiers and the lengths of these formulas may depend on \(B\) and the stage. These are formulas used to compare two runs; they are not an additional nonuniform program.