Proof. Apply refinement with common color names to the disjoint union of the two tuple tables \(V(G)^k\) and \(V(H)^k\), taking replacements within the corresponding graph. Since each update retains the old color, these common partitions refine. If one update causes no splitting, it only renames the existing classes. All subsequent updates then have the same property, so the common partition has stabilized.

We use two consequences of the update rule. First, if two tuples have equal colors at a round, applying the same coordinate permutation to both preserves color equality. This follows by induction from the initial types: a common permutation permutes the components of a replacement vector and applies the corresponding coordinate permutation to each replacement tuple. Second, for two tuples in the same stable class, stability provides a vertex bijection matching their entire vectors of stable replacement colors. Indeed, the two multisets of such vectors agree, so we may match the vertices within each vector class.

Suppose \(G\equiv_k H\). Choose a pair of equally colored stable \(k\)-tuples; one exists because the color histograms agree and the graphs are nonempty. Use the preceding bijection to append one vertex to each tuple. The resulting pair of \((k+1)\)-tuples has the following property: deleting any common slot leaves equally colored stable \(k\)-tuples. Deleting the appended slot gives the original pair; every other deletion gives a matched replacement pair, up to a common coordinate permutation.

Duplicator maintains a pair of fully specified \((k+1)\)-tuples with this property, treating entries in vacant slots as virtual. To fill slot \(j\), apply the stable-class bijection to the projection deleting slot \(j\). Whichever vertex Spoiler chooses, the projection deleting \(j\) remains unchanged, while every other deletion projection becomes a matched replacement pair, up to a common permutation. Thus the property persists. Discarding a pair only makes that entry virtual. Every two slots occur together in some deletion projection because \(k\ge 2\). The initial types in these projections therefore preserve all equalities and adjacencies among occupied slots, proving that this strategy wins.

Conversely, fix a winning strategy with \(k+1\) slots. We prove by induction on \(s\) that, at every history ending with exactly \(k\) occupied pairs, the two tuples have equal round-\(s\) colors in any common ordering of those slots. The case \(s=0\) is partial isomorphism. For the induction step, fill the spare slot. The strategy announces a bijection before Spoiler chooses the new vertex. After any such choice, Spoiler may discard any one of the old slots. The induction hypothesis at these resulting histories matches all \(k\) replacement colors for that same vertex bijection. Hence the entire joint vector is matched, and Equation (1) gives the next-round equality.

Fill \(k\) slots from empty in a fixed order. This procedure induces a bijection from \(V(G)^k\) to \(V(H)^k\), even when the strategy depends on the history. To recover the preimage of a target tuple, invert the first announced vertex bijection, thereby recover the first source choice and history, and continue successively. Since each resulting tuple pair has equal colors at every round, the color histograms agree.

For the final assertion, use induction on the ordinary color-refinement round at all one-pair histories. From such a history fill another slot. The announced bijection preserves adjacency to the retained pair for every possible choice. After discarding the old pair, the induction hypothesis matches the previous-round colors of the new vertices. Thus the same bijection matches the neighbor-color multisets of the retained vertices. Their next colors agree. The first announced bijection, from the empty history, then proves equality of all vertex-color histograms. ◻

Proof. Equal histograms imply equal graph orders, since their total sizes are \(|V(G)|^k\) and \(|V(H)|^k\). Empty graphs cause no difficulty, so assume that this common order is positive. A winning strategy can be restricted to a smaller number of slots. For \(k\ge j\ge 2\), apply Lemma 2 in both directions. For \(k\ge 2\) and \(j=1\), use its final assertion; the remaining case is immediate. If some \(j\le k\) identifies \(G\), then \(k\)-equivalence to \(G\) implies \(j\)-equivalence and hence isomorphism. The converse follows from the definition of dimension. ◻

Proof. Retain only a suspect pair \((v,w)\) and fill another slot. To preserve adjacency for every vertex choice, the announced bijection must map \(N_G(v)\) onto \(N_H(w)\), so their cardinalities agree. This applies to every candidate pair created by any announced bijection, proving the second assertion as well. ◻

Proof. Malformed encodings, including matrices outside the specified graph domain and nonpositive parameters, can be rejected in polynomial time. Let \(n\ge 1\) be the order of a valid input graph \(G\).

First compare the binary parameter with \(n\). If \(k\ge n\), accept. For \(n\ge 2\), a \(k\)-tuple listing all vertices, with repetitions if needed, has an initial equality and adjacency type that determines an isomorphism to any matching tuple in a graph of order \(n\). Different orders are distinguished by histogram sizes. Order one is immediate under ordinary color refinement. This comparison is performed before constructing a tuple table, regardless of how large the integer encoded by \(k\) may be.

It remains to consider \(1\le k<n\). Enumerate all labeled simple graphs \(H\) on \(n\) vertices, and reject exactly when one satisfies \(G\equiv_k H\) but \(G\not\cong H\). This is the desired test by Lemma 3. There are \(2^{\binom n2}\) candidates, and testing all \(n!\) vertex permutations per candidate suffices for isomorphism.

For equivalence, maintain integer identifiers for the common color classes of the two tuple tables. There are \(2n^k\) entries and at most \(2n^k\) refinement rounds before stabilization. Each signature contains the old identifier and at most \(n\) vectors of length \(k\); sorting and renaming these signatures costs a fixed polynomial in \(n^k,n,k\). Recursive color expressions need not be expanded. For \(k=1\) use the neighbor signatures instead. Agreement of the histograms through stabilization is sufficient, since later rounds only rename stable classes. Finally, \(n^k\le n^n\), so enumeration, refinement, and permutation testing together take time exponential in a polynomial of the explicit input length. ◻

Proof. The two graphs have the same positive order, and Lemma 2 supplies a winning strategy from \(G(0)\) to \(H\) with \(K=r+1\) pair slots. We first recover the forgotten colors and the private leaves, and then recover each block.

A base vertex of color \(j\) in \(G(0)\) has degree in the interval \[I_j=[j(N+1),\ j(N+1)+N-1].\] These intervals are pairwise disjoint and lie above degree one. Every other vertex has degree one. By Lemma 4, the first announced bijection preserves degrees for every possible vertex choice. It follows that \(H\) has precisely the same number of vertices in each \(I_j\), the same number of degree-one vertices, and no vertices of other degrees. Call its vertices in \(I_j\) base vertices of color \(j\).

Any chosen base vertex of \(H\) can be reached in the first placement, by taking its inverse under the announced bijection. The next announced bijection must preserve both degrees and adjacency to that vertex. Its number of degree-one neighbors is therefore exactly \(j(N+1)\). Summing these required counts over all base vertices accounts for the full number of degree-one vertices in \(H\). Since such a vertex has only one neighbor, all are private leaves on bases; none remain in a separate component. The degree intervals continue to preserve base colors throughout every winning play.

There can be no base edge between two color classes whose vertices are never adjacent in \(G(0)\). Indeed, two arbitrary target vertices can be reached through two successive placements, using the inverse of each announced bijection. Their preimages have the prescribed colors, and partial isomorphism preserves the edge test. This also rules out edges within either side of the original bipartition and edges to unrelated bit coordinates.

Fix a block. Mark every one of its valuation vertices in \(G(0)\) and both bit-value vertices of each coordinate it uses. For a square there are at most \(16+2\cdot 5=26\) such vertices. A site has at most four valuations and four bit-value vertices, so is smaller. All these placements fit within \(K\ge 33\) slots. Their images are distinct, preserve their colors, and exhaust the corresponding classes in \(H\), since the class sizes agree. Thus the entire colored incidence piece for this block is isomorphic to its intended piece.

Label the two vertices in every bit pair of \(H\) by \(0\) and \(1\), once for the whole graph. In a local colored isomorphism, each bit coordinate is either kept or flipped; different coordinates cannot be exchanged because they have different colors. The valuation vertices of a site are therefore precisely all valuations in these labels. For a square, translating the homogeneous equation by its coordinate flips changes only the right-hand side, to some bit \(\beta_B\). Its valuation vertices are exactly the legal valuations of Equation (2) with that bit.

No agreement between the flips used in different local isomorphisms is being assumed. What is shared is the single labeling already assigned to each target bit pair, so every block uses the same coordinates for its incidences. Combining the resulting block descriptions, the exclusion of other base edges, and the private leaves gives \(H\cong G(\beta)\). ◻

Proof. An isomorphism preserves degrees, hence every named base-color class. Its action on each bit pair is a fixed flip. Assemble these flips into an offset vector for each horizontal name and an offset scalar for each vertical name. Each block of \(G(0)\) has its all-zero valuation vertex. Its image is adjacent to the bit-value vertices specified by these same offsets, so its valuation is exactly their restriction to that block. Legality of the image yields Equation (2) with right-hand side \(\beta_B\). Because a bit pair is shared by all blocks using it, the resulting offsets form one global assignment.

Conversely, suppose such an assignment exists. Translate each bit pair by its offset, and translate each block valuation by the offsets on that block’s coordinates. Linearity and Equation (2) make the latter a bijection from the homogeneous legal valuation set to the shifted legal set. Shared offsets preserve all valuation–bit incidences and nonincidences. The resulting color-preserving base-graph isomorphism extends to the private leaves, whose numbers depend only on the preserved base color. ◻

Proof. Fix a winning \((r+1)\)-pair strategy, supplied by Lemma 2. We will define \(Q\) using histories in which Spoiler selects only zero-valuation vertices of blocks in \(G(0)\). Their responses are valuations of the same blocks in \(G(\beta)\): Lemma 4 and the degree intervals preserve every base color.

We first record a consequence of winning that holds at every such history. If two marked blocks share a readout, their responses agree on that readout. Otherwise some shared bit has different values. Discard all pairs except those two and select the zero vertex of the shared bit pair. It is adjacent to both source blocks, whereas no vertex of the corresponding target bit pair is adjacent to both inconsistent target valuations. This contradicts winning. The test is a hypothetical continuation: it establishes consistency of the current responses without being performed in the histories used below. It needs only three pairs after the discards.

For a type \(t\) and a full allowed address \(a\) at that type, its site ring consists of the \(r\) site blocks with readouts \(x_{i,t,a_i,a_{i+1}}\). When their zero valuations are marked, let \(h_t\) be the sum of the response vectors on these readouts. Starting with this ring and one spare pair, we can transfer the sum across any incident link with matching addresses.

For each row, place its square’s zero valuation before discarding the old site pair. This uses at most \(r+1\) slots, and consistency copies the horizontal readout at the departure type. After all rows are replaced, adjacent square responses agree on their shared vertical readout. Summing Equation (2) around this square ring cancels every vertical value twice. Thus, for the two horizontal sums \(h_t,h_u\) on a link \(\ell=tu\), \[ L_{\ell,t}h_t+L_{\ell,u}h_u =\Delta_\ell(a). \tag{5}\] Now replace each square by its arrival-side site, again placing before discarding. The arrival sum is copied exactly. The procedure works in either direction. Along a complete wire, the internal sums are scalars and cancel between consecutive links. We obtain the endpoint equality with shift \(\Delta_e(a)\).

Define \(Q_{P,a}\) to be the set of sums obtained from all zero-block-only histories ending with exactly the site ring at \((P,a)\) marked. These sets are nonempty because the ring can be queried from the empty position. They include histories with every slot ordering. If desired, an ordering can be changed using the spare slot: duplicate a marked zero-site vertex before discarding its former pair. Equality forces the duplicate response to agree, so successive relocations do not change the ring values.

Continue any history realizing a value in \(Q_{P,a}\) along the wire to obtain one image inclusion in Equation (4). Starting from any history realizing a value in \(Q_{R,\sigma_e(a)}\) and traversing backward gives the reverse inclusion. In the backward traversal the coordinate injections are inverted only on their images. All resulting histories still consist of zero-block choices. No memorylessness or common simultaneous vector choice has been used. This remains true for a loop: returning to the same ring may produce a different member of its set. ◻

Proof. Fix a base address \(b\). Taking the rectangular difference in coordinates \(i\) and \(i+1\) of Equation (7) eliminates all terms except \(g_i\), because \(r\ge3\). Consequently, with \[\begin{align*} c_i&=g_i(b_i,b_{i+1}),\\ \alpha_i(u)&=g_i(u,b_{i+1})+c_i,\\ \gamma_i(v)&=g_i(b_i,v)+c_i, \end{align*}\] we have \(g_i(u,v)=c_i+\alpha_i(u)+\gamma_i(v)\). Varying coordinate \(i\) alone from the base address gives \(\alpha_i(u)=\gamma_{i-1}(u)\). Evaluation at \(b\) gives \(\sum_i c_i=0\).

Choose constants \(C_i\in\mathbb F_2\) with \(C_i+C_{i+1}=c_i\) cyclically: choose \(C_1\) arbitrarily and recurse, the final equation holding precisely because the \(c_i\) sum to zero. Set \(Y_i(u)=\alpha_i(u)+C_i\). Then \[Y_i(u)+Y_{i+1}(v) =c_i+\alpha_i(u)+\gamma_i(v)=g_i(u,v).\] For a singleton factor the corresponding deviations vanish, so the same argument includes that case. ◻

Proof. Given global offsets, sum their horizontal readouts around every real-type site ring to define \(h_P\). These functions have row-sum form by definition. Summing the square equations around a link gives Equation (5), now for the assigned offsets rather than game responses. Summing along the wire cancels the internal scalar sums and gives Equation (8).

Conversely, suppose the displayed functions exist. At each internal type \(s\) of a wire \(e:P\to R\), define a scalar function on \(D_e\) by \[ h_s(a)=\lambda_{e,0}(h_P(a)) +\sum_{\ell\text{ from }P\text{ through }s}\Delta_\ell(a), \tag{9}\] where the sum includes the link arriving at \(s\). Every \(h_s\) has row-sum form. Along the first and internal links, the link identity (5) follows immediately by cancellation. It holds also on the last link by Equation (8), with \(h_R\) evaluated at \(\sigma_e(a)\). The latter function remains of row-sum form in \(a\) because the transmission acts coordinatewise.

Choose a row decomposition of each real-type function on the full binary product, and of each internal-type function on its allowed product. Assign the chosen row terms to all horizontal readout names of that type. Each choice is made once per type, so readouts shared between different incident wires already have consistent values.

Fix a link \(\ell=tu\) on wire \(e\). For its matched addresses, denote the two chosen row-\(i\) horizontal values by \(x_t\) and \(x_u\). The residual \[g_i(a_i,a_{i+1})= \beta_{B(i,\ell,a)}+L_{\ell,t}(x_t)+L_{\ell,u}(x_u)\] is a function of those two source coordinates, and the link identity proves \(\sum_i g_i(a_i,a_{i+1})=0\) on \(D_e\). Lemma 10 supplies functions \(Y_i:D_{e,i}\to\mathbb F_2\) whose consecutive sums equal \(g_i\). Assign \(Y_i(a_i)\) to the vertical readout of this link indexed by the match corresponding to \(a_i\).

This assignment is well defined: on every link, including the last, its matches are indexed bijectively by source-domain labels. Every square uses an adjacent pair of such labels that extends to a full address because all other product factors are nonempty. Thus every square equation is satisfied, not just equations from a selected collection of addresses. Different links have distinct vertical readout names, so their assignments are independent. Site blocks impose no additional constraint. We have obtained the desired global offsets.

The final equivalence with graph isomorphism is Proposition 7. ◻

Proof. The support is connected, because it is the image of a connected corner graph. Each square contributes at most one distinct layout link, while sites contribute none, so the support has at most \(K\) links. Internal types are private to their wires and have layout degree two. Consequently a cycle, or a path between distinct real types, must traverse a complete wire of \(4K+1\) links. Neither fits into the support. The remaining description follows by removing its possible real type.

The same argument allows loops and parallel comparison schemas. In particular, two arms of one loop-wire may meet at its real endpoint, but cannot meet again inside that wire without completing its long cycle. ◻

Proof. For a closed walk, let \(c_i\in\mathbb F_2\) be its horizontal traversal count in row \(i\), reduced modulo two. Summing incidences at all corners with boundary index \(i\) gives \(c_{i-1}=c_i\): vertical traversals contribute twice. An odd marker means \(c_r=1\), so every row has an odd horizontal traversal count. Since a block supplies horizontal edges in only its own row, at least \(r\) blocks are needed.

If there are exactly \(r\) blocks, there is one in each row, and the walk meets every block. Thus all blocks lie in its component. The horizontal edge of a site, or the two horizontal edges of a square, prescribes one pair of aligned labels for that row. In the square case the two edges give the same pair because vertical edges preserve alignment. Now sum the walk’s incidences separately at each aligned label of boundary index \(i\). Vertical contributions again cancel. The odd horizontal traversal counts in the adjacent rows force their prescribed labels at this boundary to agree. Doing this at every boundary gives the full address.

Two \(r\)-subcollections of \(U\) share at least \(r-1\) blocks. For wrapping subcollections these common blocks belong to distinct rows and put both subcollections in the same component. The common rows, all but at most one row, touch every boundary index because \(r\geq3\). Hence they force the two addresses to agree at every coordinate. ◻

Proof. The assertion is immediate for \(V=U\). Assume \(V\subsetneq U\), so \(|V|\leq r\). Each component \(D\) of \(\Gamma_V\) lies in a component \(C\) of \(\Gamma_U\), and its type support is a subtree of that of \(C\).

Restriction of admissible shifts. If \(D\) is nonwrapping, it has no \(Q\) requirement, so restriction causes no problem. If \(D\) wraps, its blocks form a wrapping \(r\)-collection by Lemma 14; in particular they exhaust \(V\). The address imposed on \(C\) restricts to the same address on \(D\). When \(D\) contains a real type, it is the same real type as in \(C\) and has the same \(Q\) requirement. When \(C\) has no real type, both supports are in one wire interior and require the same common scalar.

The remaining case is that \(D\) lies inside a wire and \(C\) reaches one of its real endpoints. The address \(a\) read inside \(D\) belongs to the actual product domain \(D_e\). Consequently its expression at the real endpoint uses actual endpoint matches: it is \(a\) at the first endpoint and \(\sigma_e(a)\) at the second. By Equation (12), the permitted internal scalar set is exactly the image of the permitted real-vector set under the endpoint form, translated by the end-link constant if present. Restriction is therefore admissible. The same equality shows that any permitted internal scalar has a permitted real-vector preimage.

Extension from a wrapping old component. These cases also show that admissible shifts on a wrapping old component extend to admissible shifts on its containing new component: retain its real vector if already present, retain its scalar if the new support remains internal, or choose the real preimage just described. Then extend along the remaining arms. Only one arm is constrained in the preimage case. Since a wrapping old component consumes all \(r\) old blocks, there is never a second old wrapping choice to lift simultaneously. This remains true for loop-wires whose two original endpoints are the same real type.

Preservation of every old readout. Restricting the potentials as well now proves that every restriction of an element of \(\mathcal H_U\) lies in \(\mathcal H_V\). For surjectivity, fix a representation of an element of \(\mathcal H_V\) by old shifts and potentials. Choose admissible shifts on \(U\), agreeing with the old shifts on the possible wrapping old component; the preceding argument shows this is possible. We will adjust potentials to preserve the old readouts on every nonwrapping component \(D\).

On such a component, the marker is a difference of corner labels: there are \(s_v\in\mathbb F_2\) with marker \(s_v+s_w\) on each edge \(vw\). Indeed, choose path sums from one fixed corner. They are well-defined because every closed walk has marker sum zero. Let \(g_t\) be the sum of the new and old shifts at type \(t\) in this component. Their identical inhomogeneous link equations imply \[L_{\ell,t}(g_t)+L_{\ell,u}(g_u)=0 \qquad(\ell=tu\text{ in the support of }D).\] Replace the old potential at \(v\) of type \(t\) by \(M_v+s_vg_t\). For a horizontal edge in row \(i\), the resulting change in its offset, including the change of shift, is \[(s_v+s_w+\delta_i)g_t=0.\] For a vertical edge, \(s_v=s_w\), and the homogeneous link equation makes its offset change zero as well. Hence every old readout is preserved.

Different old components have disjoint corners, so their potential adjustments are compatible even if they merge in \(\Gamma_U\) or contain the same type. Retain the old potentials on a wrapping old component and choose arbitrary potentials at all new corners. Together these choices give an element of \(\mathcal H_U\) extending the prescribed element of \(\mathcal H_V\). ◻

Proof of Theorem 12. Duplicator maintains an assignment in \(\mathcal H_U\), where \(U\) is the set of owners of the currently marked vertices. Marked base vertices are matched by translation using the offsets on their owners: translate each block valuation and each bit-value coordinate. A marked leaf is sent to the leaf with the same private index at the translated parent. Since \(|U|\) is at most the number of occupied slots, the family \(\mathcal H_U\) is always defined.

For any fixed assignment, translation is bijective on every base vertex class with owner in \(U\): it maps homogeneous legal valuations onto the legal valuations for the twist, and permutes each bit-value pair. Parent translation also gives a bijection on the corresponding leaves, since translated parents have the same color and hence the same number of attached leaves.

These translations give a partial isomorphism on the marked vertices. The only possible base incidence is between a block valuation and a bit-value vertex for a coordinate used by that block. When both are marked, their owners belong to \(U\) and the common readout receives one offset. Equality or inequality of the two bits is therefore preserved, so both adjacency and nonadjacency are preserved. All other pairs of base classes have no edges in either graph. Leaf attachments are preserved by parent translation and private indices. Translation within each class is injective, distinct classes remain distinct, and leaf indices are preserved, so equality of marked vertices is preserved as well.

Discarding pairs simply restricts the maintained assignment to the remaining owners, which is allowed by Proposition 15. Suppose now that a slot is vacant. There are at most \(K-1=r\) current owners. For each possible owner \(B\) of the next vertex, choose an extension of the current assignment to \(\mathcal H_{U\cup\{B\}}\). This is possible before any vertex is selected, by exact projection. If \(B\in U\), use the current assignment itself.

On the part of the vertex set owned by \(B\), use the chosen extension to translate the base classes and their leaves. These parts partition the vertex set, and each maps bijectively onto the identically owned part in the other graph. They therefore combine into a single vertex bijection, which Duplicator announces. Its parts for the current owners agree with the maintained assignment, so in particular it extends all currently marked pairs, including repeated occurrences of a vertex.

After Spoiler selects a vertex, retain the extension chosen for its owner \(B\). It agrees with every old marked pair and with the newly selected pair. The preceding partial-isomorphism check applies to this enlarged position. Thus the strategy wins with \(K=r+1\) slots, which proves \(G(0)\equiv_r G(\beta)\). ◻

Proof. By Proposition 6, write \(H\cong G(\beta)\) for some square bits \(\beta\). Transporting equivalence through this isomorphism, apply Proposition 8 to obtain nonempty sets \(Q_{P,a}\) satisfying (4). No restriction to the special twists of Theorem 12 is made here: all wire sums \(\Delta_e(a)\) may depend on the address.

First consider a buffered connection \(l\) at \(a\in D_l\). If the source image \(o(Q_{P,a})\) is a singleton, the first two comparisons force both coordinate images of \(Q_{B_l,a}\) to be singletons, possibly translated by different shifts. As this set is nonempty, it contains exactly one vector. Its sum image is therefore a singleton, and the third comparison makes \(s(Q_{R,\sigma_l(a)})\) a singleton. Thus a buffered connection propagates singletonness from its source form to its destination form. We do not need these singletons to have value zero.

At each seed, comparison with the dummy’s zero form gives a singleton scalar image. Induction in the acyclic circuit order now shows that every true gate has a singleton output image. For a true scalar, use its seed comparison or one true incoming source. For a true AND gate, each port receives a true source, so both coordinate images become singletons and their sum is a singleton as well.

By Proposition 16, at least one test is true. Its added connection forces \(A\) to have a singleton image at that address. Flipping individual coordinates connects all addresses in \(\{0,1\}^r\), so the broadcast connections propagate this property to every address of \(A\). The connections from \(A\) to every gate coordinate then imply that all primary sets are singletons. Write \[Q_{P,a}=\{h_P(a)\} \qquad(P\text{ primary},\ a\in\{0,1\}^r).\]

To use Proposition 11, it remains to prove that these functions have row-sum form and to supply the functions at the remaining real types. Fix a coordinate form \(s\) of a primary type \(P\), and take its identity self-connection \(l\). At each address, the first two comparisons give buffer coordinates \[z_1=s(h_P(a))+\Delta_{l1}(a),\qquad z_2=s(h_P(a))+\Delta_{l2}(a).\] Their sum cancels the two copies of \(s(h_P(a))\) over \(\mathbb F_2\). The third comparison, with destination the same coordinate at the same address, gives \[ s(h_P(a))=\Delta_{l1}(a)+\Delta_{l2}(a)+\Delta_{l3}(a). \tag{18}\] Each term on the right has row-sum form on the full product. Hence every coordinate of every primary \(h_P\) has row-sum form, and therefore so does the vector function itself. Either self-connection copy suffices for \(A\).

For each private buffer \(B_l\), prescribe on \(D_l\) its coordinates \[h_{B_l,j}(a)=o(h_P(a))+\Delta_{lj}(a),\qquad j=1,2.\] These are the unique coordinates of its image-consistency set on that domain. They have row-sum form there. Extend each adjacent-coordinate term arbitrarily from its allowed pair of factors to \(\{0,1\}^2\); their sums define row-sum functions on the full address product. This extension changes no comparison, because the buffer occurs only in its three schemas on \(D_l\). Give the dummy the zero function.

On each comparison domain, every scalar form appearing in a comparison now has the singleton value prescribed by Equation (4); the dummy’s zero form also has its required singleton image. Thus these row-sum functions satisfy all identities in (8). Proposition 11 supplies global offsets, and Proposition 7 gives \(G(\beta)\cong G(0)\). Therefore \(H\cong G(0)\), as required. ◻

Proof. Choose comparison constants \(b_e\in\mathbb F_2\) as follows. All are zero except the constant of the third comparison of one of the two identity self-connections at \(A\), which is one. Form the special twist of Theorem 12: on each wire put \(b_e\) on its last link and zero on its other links, and on a square in row \(i\) use that link constant multiplied by \(\delta_i\), where \(\delta_r=1\) and all other \(\delta_i=0\). Then \(\Delta_e(a)=b_e\) on every comparison domain.

We first rule out an isomorphism. In a hypothetical solution of (8), the first two comparisons of either broadcast self-connection would copy \(h_A(a)\) into both coordinates of that connection’s buffer. Their sum would be zero. The unshifted copy’s third comparison would force \(h_A(a)=0\), whereas the shifted copy’s third comparison would force \(h_A(a)=1\). This contradiction holds at every address. Propositions 11 and 7 therefore show that \(G(\beta)\not\cong G(0)\).

To prove equivalence, it suffices by Theorem 12 to construct nonempty image-consistency sets. Evaluate truth only in the original acyclic circuit. At a scalar gate use \(\{0\}\) if it is true and \(\mathbb F_2\) if it is false. At an AND gate, use the product subset of \(\mathbb F_2^2\) whose coordinate is fixed to zero if its corresponding port is true and is free otherwise. Its output sum image is \(\{0\}\) exactly when both ports are true, and is \(\mathbb F_2\) otherwise. Thus every gate output has image \(\{0\}\) if true and \(\mathbb F_2\) if false. Give both \(A\) and the dummy the full set \(\mathbb F_2\) at every address. The seed comparisons hold, since a seed is true and the image of the zero form at the dummy is \(\{0\}\).

Consider any unshifted directed connection \(l\). A singleton source image is necessarily \(\{0\}\), and its destination image is then also \(\{0\}\). For an original circuit edge this follows because a true source makes the destination scalar or input port true. For an identity self-connection it is immediate. All tests are false in the present case, and all broadcast sources have full images, so those added connections produce no further singleton-source case. In the singleton-source case choose \[Q_{B_l,a}=\{(0,0)\}.\] Its two coordinate images and its sum image satisfy all three comparisons.

In every other case, including the shifted broadcast self-connection, the source image is \(\mathbb F_2\). Let \(D'=s(Q_{R,\sigma_l(a)})\) be the nonempty destination image, and choose \[ Q_{B_l,a}=\{(u,v)\in\mathbb F_2^2:u+v\in D'+b_{l3}\}. \tag{19}\] Both coordinate projections of this set are \(\mathbb F_2\), and its sum image is exactly \(D'+b_{l3}\). Since \(b_{l1}=b_{l2}=0\) throughout, all three comparisons again hold. This includes a full source image and a singleton destination image: the buffer may have two correlated coordinates without either projection being a singleton. That possibility is why image consistency does not imply a global pointwise solution here.

These choices define each private buffer on its active domain. Extend it by arbitrary nonempty sets outside that domain, where it occurs in no comparison. We have obtained nonempty sets at every real type and address satisfying (4) with shifts \(b_e\). Theorem 12 therefore gives \(G(\beta)\equiv_r G(0)\). ◻

Proof of Theorem 1. Proposition 5 gives membership in \(\mathrm{EXPTIME}\). For hardness, fix any language in \(\mathrm{EXPTIME}\) and its machine \(M\) as above. The construction (17) is a deterministic polynomial-time map from its input words to graph–parameter pairs. If \(M\) accepts, Proposition 17 says that \(r\)-WL identifies \(G(0)\), so its dimension is at most \(r\). If \(M\) does not accept, Proposition 18 supplies an equivalent nonisomorphic graph, so \(r\)-WL does not identify \(G(0)\). By monotonicity of identification in the dimension, the dimension of \(G(0)\) is then greater than \(r\). Thus acceptance maps exactly to the YES instances of the dimension problem. Since the language was arbitrary, the problem is \(\mathrm{EXPTIME}\)-hard under deterministic polynomial-time many-one reductions, and hence \(\mathrm{EXPTIME}\)-complete. ◻

Proof. For membership, convert the unary dimension to binary and apply Proposition 5. For hardness, the reduction above outputs \(r=2p(m)+4\), whose value is polynomial in the source input length \(m\). Writing \(r\) in unary therefore preserves polynomial-time constructibility and the same acceptance equivalence. ◻