Proof. We realize WL updates by operations on rooted counts, then recover color indicators on the fixed finite targets by interpolation. Equip \(F\) with a list \(\boldsymbol\ell=(\ell_1,\ldots,\ell_k)\) of roots, allowing repetitions, all contained in a designated bag. Let \(h_F(X,\mathbf x)\) count homomorphisms sending \(\ell_i\) to \(x_i\), and let \(\mathcal A_t\) be the rational span of these functions for sources with bag size at most \(t\). Distinct isolated roots give the constant \(1\); repeating a root tests equality, and joining two roots tests adjacency. Complements and products therefore give atomic-type indicators.

Here is the decomposition invariant behind the algebra. To glue rooted graphs along an interface, attach their designated bags to a central bag of formal interface vertices and identify each root with its assigned interface vertex. In each operand, every merged vertex is a root, so its occurrence subtrees meet the designated bag. Their quotient occurrences connect through the central bag. Other vertices retain their connected occurrence subtrees, and taking images of bags never increases their sizes. Parallel edges may be collapsed; a loop gives the zero function on simple targets. The central bag contains the output roots, so this invariant persists under successive operations. In particular, gluing corresponding roots realizes products in \(\mathcal A_t\), with an interface of size at most \(k\).

For joint refinement, the same construction gives closure under \[(f_1,\ldots,f_k)\longmapsto \left[(X,\mathbf x)\longmapsto \sum_{y\in V(X)}\prod_{i=1}^k f_i(X,\mathbf x[i\leftarrow y])\right].\] For rooted counts, use a central bag of formal vertices \(u_1,\ldots,u_k,y\), attach operand \(i\) at its replacement list, and retain \(u_1,\ldots,u_k\) as output roots. This uses \(k+1=t\) vertices; multilinearity handles their linear combinations. Repeated roots can force \(y=u_j\) or merge old positions, precisely enforcing the corresponding equalities in the summation.

For separate refinement only \(f\mapsto\sum_y f(X,\mathbf x[i\leftarrow y])\) is needed. Use adjacent bags \(O=\{u_1,\ldots,u_k\}\) and \(R=\{u_j:j\ne i\}\cup\{y\}\), and attach the operand’s root bag to \(R\). Each has size at most \(k=t\). After the root identifications, a merged class meeting both \(O\) and the operand contains a surviving \(u_j\), so it also meets \(R\). Thus no occurrence gap is created, even when \(y=u_j\). The old \(u_i\) remains a pinned output root in \(O\). A homomorphism of the quotient specifies exactly one allowed image of \(y\) and one operand homomorphism: an identification restricts that image, rather than contributing an additional free choice.

Fix the two finite targets. At each round, every color indicator restricted to tuples of these targets agrees with a function in \(\mathcal A_t\). Indeed the update operations give the multiplicity of each color vector (or each coordinate color). If such a multiplicity \(M\) has attained values \(S\), its value-\(q\) indicator is the polynomial \(\prod_{s\in S\setminus\{q\}}(M-s)/(q-s)\), for \(q\in S\). Products with the old-color indicator give every new-color indicator. The coefficients are common to the two targets. Finally, \(\sum_{\mathbf x\in V(X)^k}h_F(X,\mathbf x)=\hom(F,X)\): each homomorphism specifies one root-image tuple, even with repeated roots. The hypothesis therefore equates all color histograms.

For the union implementation, perform the indicator induction on all tuples of \(U=X_0\sqcup X_1\), including mixed tuples. The interpolation coefficients are then fixed before either pure restriction is summed. For the final quotient source \(F\), let \(\mathcal L\) be its components containing roots and \(\mathcal R\) its rootless components. The exact identity is \[ \sum_{\mathbf x\in V(X_j)^k}h_F(U,\mathbf x) =\prod_{Q\in\mathcal L}\hom(Q,X_j) \prod_{Q\in\mathcal R}\hom(Q,U). \tag{3}\] Connectedness forces each rooted component into \(X_j\); rootless components are unrestricted. Every map still determines one tuple. Different source components may share target images, so their choices remain independent. Components inherit the bag bound, the first product agrees for \(j=0,1\), and the second is common. Applying this identity to each term of a color indicator proves the claim. ◻

Proof. Let \(A_X(v,w)=\mathbf 1_{\{vw\in E(X)\}}\). For main images \(\mathbf z=(z_1,\ldots,z_t)\), put \(q_B(\mathbf z)=|\bigcap_{b\in B}N_X(z_b)|\), for triples \(B\subseteq[t]\). Their number of extensions to \(T\) is \[E_X(\mathbf z)= \prod_{a<b} A_X(z_a,z_b) \prod_{B\in\binom{[t]}3}q_B(\mathbf z)^3.\] The clique factor rejects repeated main images. Helper images may coincide, so their choices are independent and the displayed product is exact.

First consider joint refinement. A round-one color of a \(k\)-tuple determines each triple common-neighbor count on its positions. For one candidate \(w\), its atomic replacement vector reveals adjacency to position \(p\) in any component replacing a coordinate other than \(p\). Thus that one vector tests simultaneous adjacency to the whole triple; summing its multiplicities gives the count.

Now fix \(\mathbf x=(z_1,\ldots,z_k)\) and set \(z_{k+1}=y\). Its old round-one color and the single vector \[\bigl(C_1(\mathbf x[1\leftarrow y]),\ldots, C_1(\mathbf x[k\leftarrow y])\bigr)\] give the round-one colors of all \(k\)-position faces of these \(k+1\) main positions. The old tuple omits \(k+1\); replacement face \(i\) omits \(i\), with its coordinate \(i\) representing position \(k+1\). Every pair and triple lies in a face, since \(k\ge4\). Reading it from, for example, the face omitting the least position outside it determines every factor of \(E_X(\mathbf x,y)\). All faces in this vector refer to the same \(y\). The round-two multiset therefore determines \(\sum_y E_X(\mathbf x,y)\); summing over tuple colors gives \(\hom(T_{k+1},X)\).

For separate refinement, all \(t=k\) main images are already fixed. For a triple \(B\), choose \(i\notin B\). If \(M_i(\sigma)\) is the multiplicity of atomic type \(\sigma\) in the \(i\)-th replacement multiset, then \[q_B(\mathbf x)=\sum_\sigma M_i(\sigma) \prod_{p\in B} A_\sigma(i,p),\] where \(A_\sigma(i,p)\) is its adjacency bit. Thus the round-one color determines \(E_X(\mathbf x)\), and its histogram determines \(\hom(T_k,X)\).

Finally take a pure tuple in \(X_j\) while refining \(U=X_0\sqcup X_1\). In the joint case, a last main image outside \(X_j\) makes the clique factor zero. Once all main images lie in \(X_j\), every common neighbor of a triple lies there too. Hence the same formulas, evaluated in \(U\), count precisely the desired extensions into \(X_j\). ◻

Proof. Fix \(\phi:F\to G\). Its lifts to \(X_b\) correspond to solutions in variables \(z_{x,a'}\), one for each source vertex \(x\) and each \(a'\in N_T(a(x))\), of \[\sum_{a'\in N_T(a(x))}z_{x,a'}=b(a(x)) \quad(x\in V(F)),\qquad z_{x,a(y)}+z_{y,a(x)}=0 \quad(xy\in E(F)).\] Indeed a solution gives the map \(x\mapsto(\phi(x),z_x)\), and a lift uniquely determines these source-indexed vectors. Equality of projected images does not itself identify these source-indexed tag variables; all constraints on them are given by the displayed system.

The coefficient matrix is independent of \(b\). The system for \(b=0\) has its kernel as solution set; for \(b=e_1\) the solution set is either empty or a translate of that kernel. Every homomorphism into \(X_b\) has a unique projection to \(G\), so summing over all \(\phi\) proves the inequality. Since each homogeneous system is nonempty, strictness is equivalent to inconsistency of at least one projected system for \(X_\star\). In particular, contributions from other projections cannot cancel a strict inequality.

A binary system \(Mz=c\) is inconsistent exactly when some linear combination of its rows has left side zero and right side one. For the nontrivial direction, if \(c\notin\operatorname{im}M\), extend a basis of \(\operatorname{im}M\) by \(c\) to obtain a linear functional vanishing on \(\operatorname{im}M\) and taking value one at \(c\). Let \(s(x)\) and \(r(xy)\) be the coefficients of the vertex and edge equations above. The coefficient of \(z_{x,a'}\) in their combination is \(s(x)+\sum_{y:\,xy\in E(F),\,a(y)=a'}r(xy)\), and the right side for \(X_\star\) is \(\sum_{a(x)=1}s(x)\). This gives exactly (4), without any independence assumption on the equation rows.

For adjacent types \(u,v\), sum the first equation of (4) over all vertices of type \(u\), using neighbor type \(v\). The result is the total \(r\)-weight of the edges between these two types. Summing from type \(v\) gives the same total, so \(m_u(V(F))=m_v(V(F))\). Since \(T\) is connected and \(m_1(V(F))=1\), every type mass is one. ◻

Proof. Given a successful choice \((d_i)_{i\in[t]}\), map main vertex \(i\) to \((i,d_i)\) and each \(h_{ij;\ell}\) to \((h_{ij;\ell},\lambda_{ij}^i(d_i))\). The common pair label and the unrestricted edge toward \(\ell\) make this a homomorphism \(\phi:T\to G\) with \(\tau\circ\phi\) the identity. Set every vertex and edge weight to one. Each vertex of \(T\) has exactly one neighbor of each adjacent type, and exactly one source vertex has type \(1\), so (4) holds. Apply Lemma 8 and then Lemma 6. ◻

Proof. All sums in this proof are in \(\mathbb F_2\). We use the type masses \(m_u(Y)\) from (5); in particular, \(m_u(V(F))=1\) for every type \(u\).

Orienting the decomposition. Fix a decomposition tree \(\mathcal D\), and contract edges joining identical bags. Every remaining edge has an intersection \(S\) of size at most \(t-1\): an intersection of size \(t\) would force both incident bags to be that same set. Deleting the tree edge partitions \(V(F)\) into \(S\) and two sides \(A^0,A^1\). Indeed, the occurrence subtree of a vertex outside \(S\) lies in just one of the two tree components. No graph edge joins the two sides, since its endpoints occur together in a bag.

At least one main type is absent from \(S\). If two main types \(u,v\) are absent, all \(uv\)-edges incident with either type on a side stay on that side. Summing (4) over their two endpoint classes gives \(m_u(A^\nu)=m_v(A^\nu)\) for \(\nu\in\{0,1\}\). For any absent main type \(u\), \[m_u(A^0)+m_u(A^1)=m_u(V(F))=1.\] Orient the tree edge toward the side of mass \(1\). This is well defined whether there is one absent main type or several.

Choose a sink of the oriented tree and denote its bag by \(B\). For each incident edge let \(A\) be its outer side and \(S\subseteq B\) its intersection. These outer sides partition \(V(F)\setminus B\). To see this precisely, the occurrence subtree of a vertex outside \(B\) avoids the sink node and lies in exactly one component of \(\mathcal D\) minus that node. A vertex in \(B\) occurring in a branch must belong to that branch’s intersection \(S\), so is excluded from its outer side. Thus vertices are counted once, regardless of how many bags contain them. Moreover, every neighbor of \(A\) outside \(A\) lies in \(S\), and the sink orientation gives \[m_\ell(A)=0 \qquad\text{for every main type \(\ell\) absent from \(S\).}\] If a main type were absent from \(B\), it would be absent from every such \(S\) and have mass zero in the bag and in all outer sides, contrary to its global mass \(1\). Since \(|B|\le t\), the bag therefore consists of exactly one vertex \(x_i\) of each main type \(i\), and no helper vertices. No condition on the individual weights \(s(x_i)\) is needed.

A global mismatch test. Write \(\phi(x_i)=(i,d_i)\), with \(d_i\in D_i\). The bag \(B\) need not induce a clique, so compatibility of these representatives does not follow from \(\phi\) alone. Suppose, for a contradiction, that some pair \(i<j\) has different labels, and put \(\alpha=\lambda_{ij}^i(d_i)\). We choose label predicates that vanish on these representatives and are complementary on matching labels. For source vertices of types \(i,j\), respectively, put \[p_i(x)=\mathbf 1_{\{\lambda_{ij}^i(\phi(x))\ne\alpha\}}, \qquad p_j(x)=\mathbf 1_{\{\lambda_{ij}^j(\phi(x))=\alpha\}}.\] For \(Y\subseteq V(F)\), let \[P(Y)=\sum_{d\in\{i,j\}}\ \sum_{\substack{x\in Y\\a(x)=d}} s(x)p_d(x).\] Each \(ij\)-edge has matching labels under \(\phi\), hence the two endpoint predicates sum to \(1\). Expanding the corresponding coordinates of (4) gives \[ \begin{aligned} P(V(F)) &=\sum_{\substack{xy\in E(F)\\a(x)=i,\ a(y)=j}} r(xy)\bigl(p_i(x)+p_j(y)\bigr)\\ &=\sum_{\substack{xy\in E(F)\\a(x)=i,\ a(y)=j}}r(xy) =m_i(V(F))=1. \end{aligned} \tag{6}\] Here each edge is listed with its \(i\)-endpoint first. On the other hand, \(P(B)=0\).

Vanishing on an outer side. Fix an outer side \(A\) with intersection \(S\), and choose a main type \(\ell\) absent from \(S\); thus \(m_\ell(A)=0\). We show that \(P(A)=0\), retaining the possible boundary edges.

First suppose \(\ell=i\); the case \(\ell=j\) is symmetric. Every \(i\)-neighbor of a \(j\)-vertex in \(A\) lies in \(A\), because an external neighbor would lie in \(S\), which has no \(i\)-vertex. An edge from an \(i\)-vertex in \(A\) may reach a \(j\)-vertex in \(S\), but its \(p_j\)-value is zero. Consequently expansion of (4) yields \[\begin{aligned} P(A) &=\sum_{\substack{x\in A\\a(x)=i}} \ \sum_{\substack{y\in N_F(x)\\a(y)=j}} r(xy)\bigl(p_i(x)+p_j(y)\bigr)\\ &=\sum_{\substack{x\in A\\a(x)=i}} \ \sum_{\substack{y\in N_F(x)\\a(y)=j}}r(xy) =m_i(A)=0. \end{aligned}\]

Now suppose \(\ell\notin\{i,j\}\), and put \(h=h_{ij;\ell}\). Each base vertex of type \(h\) couples the two predicates through its stored \(L_{ij}\)-label. Having this helper type for every possible \(\ell\) makes the calculation available whichever main type \(S\) omits. Since \(S\subseteq B\), neither \(h\) nor \(\ell\) occurs in \(S\). We will show \(P(A)=m_h(A)=m_\ell(A)=0\), using a zero boundary correction to complete the neighbor sums in the first equality. Write \(H_A=\{w\in A:a(w)=h\}\). Every \(h\)-neighbor of an \(i\)- or \(j\)-vertex in \(A\) belongs to \(H_A\): an outside neighbor would have to lie in \(S\). Expanding the \(h\)-coordinate at each tested main vertex therefore gives \[P(A)=\sum_{w\in H_A}\ \sum_{d\in\{i,j\}} \ \sum_{\substack{x\in A\cap N_F(w)\\a(x)=d}} r(wx)p_d(x).\] The boundary correction \[C_S=\sum_{w\in H_A}\ \sum_{d\in\{i,j\}} \ \sum_{\substack{x\in S\cap N_F(w)\\a(x)=d}} r(wx)p_d(x)\] is zero, since \(p_i,p_j\) vanish on their respective vertices of \(S\). Adding it includes all \(i\)- and \(j\)-neighbors of every \(w\in H_A\), because all external neighbors of \(A\) lie in \(S\).

For each such \(w\), let \(q_w\in L_{ij}\) be the label stored at \(\phi(w)\), and write \[R_d(w)=\sum_{\substack{x\in N_F(w)\\a(x)=d}}r(wx) =s(w)\qquad(d=i,j),\] where the equality is the corresponding coordinate of (4). Its \(i\)-neighbors have predicate \(\mathbf 1_{\{q_w\ne\alpha\}}\), and its \(j\)-neighbors have predicate \(\mathbf 1_{\{q_w=\alpha\}}\). Hence \[\begin{aligned} P(A) &=P(A)+C_S\\ &=\sum_{w\in H_A} \bigl(\mathbf 1_{\{q_w\ne\alpha\}}R_i(w) +\mathbf 1_{\{q_w=\alpha\}}R_j(w)\bigr)\\ &=\sum_{w\in H_A}s(w)=m_h(A). \end{aligned}\] These are separate coordinate equations at each source vertex \(w\); its number of neighbors, its label \(q_w\), and its weight \(s(w)\) may vary. An empty neighbor class simply forces \(s(w)=0\). Finally, because neither \(h\) nor \(\ell\) occurs in \(S\), every \(h\ell\)-edge incident to either type in \(A\) stays in \(A\). Summing its coordinate equations at the two endpoint classes gives \(m_h(A)=m_\ell(A)=0\), as required.

The disjoint vertex partition now gives \[P(V(F))=P(B)+\sum_{\text{outer sides }A}P(A)=0,\] contradicting (6); the sum is empty if the decomposition has only one bag. Thus all \(d_i\) have matching pair labels and form a successful choice. ◻

Proof of Theorem 2. The parity lifts in Definition 7 are simple, uncolored and of equal order; their preceding tag count gives \(n\le A M_t\). If a successful choice exists, Lemma 9 gives a strict count difference for \(T_t\). Lemma 6 detects that difference after two joint rounds or one separate round.

Conversely, suppose that no successful choice exists. If a graph \(F\) with bags of size at most \(t\) had different counts into the two lifts, Lemma 8 would give the data \(\phi,s,r\) of Lemma 10. That lemma would produce a successful choice, a contradiction. All such homomorphism counts therefore agree. Lemma 5 gives equivalence in the corresponding convention, including the pure-tuple disjoint-union implementation. ◻

Proof. Partition the clauses into \(t\) groups of size at most \(\lceil m/t\rceil\). Let \(V_i\) be the variables in group \(i\), and let \(D_i\) contain exactly the assignments on \(V_i\) satisfying that group. Set \[L_{ij}=\{0,1\}^{V_i\cap V_j}, \qquad \lambda_{ij}^i(d)=d|_{V_i\cap V_j}, \qquad \lambda_{ij}^j(d)=d|_{V_i\cap V_j}.\] Each scope has size at most \(3\lceil m/t\rceil\), proving the bounds. Pairwise agreement assigns every shared variable one value, so the choices join to an assignment satisfying all clauses; unused variables are free. Conversely, restrict a satisfying assignment to each scope. An empty group has its unique empty assignment, an unsatisfiable group has empty domain, and an empty overlap has one label, the empty assignment. Thus these cases require no exception. ◻

Proof of Theorem 3. Use positive-rate ETH (Impagliazzo and Paturi 2001): for some \(\delta>0\), no deterministic \(3\)-SAT algorithm runs in \(2^{\delta N}\operatorname{poly}(|F|)\) time. Choose \(\epsilon<\delta/4\), and fix \(C=C_\epsilon\) from Lemma 11. For the Turing-machine model set \(q=1\). More generally, suppose the chosen machine model has a simulation taking at most \(A_k(T+\ell+1)^q\) steps, where \(q\ge1\) is fixed by the model, independently of the simulated program and \(k\). Here \(T\) is the program’s running time and \(\ell\) its input length; \(A_k\) may depend on the chosen fixed program and \(k\). Choose \[c=\frac{\delta}{24Cq}, \qquad K\ge4,\qquad K>\frac{4C\max\{B_0,6q\}}{\delta}.\]

Fix any \(k\ge K\) and suppose a solver takes \(O(n^{ck})\) time. Hardcode this solver and \(k\) into a \(3\)-SAT algorithm. Sparsify the input, form the graph pair for every sparse disjunct, and accept exactly when at least one pair is inequivalent. Lemmas 11 and 12, together with Theorem 2, prove correctness.

The matrix input has length \(\ell=O(n^2)\), so the simulated solver takes \(O_k(n^{qck}+n^{2q}+1)\) time. Both terms matter, even when \(ck<2\). By (7) and (8), the total time is bounded, up to polynomial input factors and fixed-\(k\) constants, by \[2^{\epsilon N} \left( 2^{B_0 CN/t} +2^{6qCN/t} +2^{3CqckN/t} \right).\] Since \(t\ge k\), the first two inner rates are below \(\delta/4\), and the third is at most \(\delta/8\). The resulting rate is below \(\delta/2\), contradicting ETH. The solver’s description, its running-time constant, \(A_k\), \(b_k\), and the eventual threshold in \(N\) may all depend on this fixed \(k\); \(c\) and \(K\) do not. Thus the contradiction applies to every fixed \(k\ge K\), without a uniform way of selecting the alleged solvers. ◻