Weisfeiler-Leman refinement is a canonical procedure for testing
whether two finite graphs admit the same k-tuple color histogram.
The one-dimensional version was introduced by Weisfeiler and Leman
as a route to canonical forms, and its higher-dimensional
generalizations are the standard symmetric analogues of the
arc-consistency relaxation for constraint satisfaction.
./pdfs/wl1968.pdf
Fix an integer $k\ge2$. The $k$-dimensional refinement starts with
the atomic color of a $k$-tuple $\bar v=(v_1,\ldots,v_k)$: the
coordinate equalities $v_i=v_j$, the adjacency indicators
$E(v_i,v_j)$, and any pre-existing vertex colors. Under the joint
convention the recursive rule is
$$\chi_{t+1}(\bar v)
= \Bigl(\chi_t(\bar v),
\bigl\{\!\bigl\{(\chi_t(\bar v[i\leftarrow z]))_{i=1}^{k}
: z\in V\bigr\}\!\bigr\}\Bigr),$$
where the multiset is over $z\in V$ and records at each $z$ the
common-$z$ $k$-vector of replacement colors. Under the separate
convention the recursive rule is instead
$$\chi_{t+1}(\bar v)
= \Bigl(\chi_t(\bar v),
\bigl(\bigl\{\!\bigl\{\chi_t(\bar v[i\leftarrow z])
: z\in V\bigr\}\!\bigr\}\bigr)_{i=1}^{k}\Bigr),$$
in which each coordinate has its own replacement multiset. Either way
the partitions of $V^k$ induced by the common color names refine
monotonically, and stabilization is reached in polynomially many
rounds.
The direct algorithm runs in time $n^{O(k)}$. There are $n^k$
tuples, polynomially many refinement rounds, and each round
costs a polynomial in $n^k$. The main theorem excludes any
sequential algorithm that lowers the exponent to $O(1)$.
Main theorem. There are absolute constants $c_0>0$ and $k_0$ such
that for every integer $k\ge k_0$ and every correct deterministic
sequential algorithm $A$ for $k$-Weisfeiler-Leman equivalence, there
is a threshold $n_0=n_0(A,k)$ with
$$T_A(n)\ge n^{c_0 k}$$
for every integer $n\ge n_0$.
The bound holds both for multitape Turing machines with a fixed
input alphabet and for sequential logarithmic-word RAMs with fixed
polynomial-bit-time instructions. Inputs are pairs of adjacency
matrices of simple, undirected, uncolored graphs of the same order
$n$; the time $T_A(n)$ is the worst case over such input pairs of a
run that halts and produces the correct answer. Algorithms may
perform arbitrary deterministic computation, and the input is the
$2n^2$-bit adjacency matrix; the constant $c_0$ does not depend on
$k$ and is not absorbed by any input-independent additive term.
Four features of the statement are decisive. It is unconditional:
no hypothesis about $\mathrm{P}$, $\mathrm{NP}$, or
$\Sigma_2^{\mathrm{P}}$ is used. It holds at every sufficiently
large order: the threshold $n_0(A,k)$ may be enormous, but past it
the bound holds at every single integer $n$. The exponent is
absolute: the constant $c_0>0$ is independent of $k$ and of $A$,
so the main theorem, taken over all $k\ge k_0$, rules out every
running-time bound $f(k)n^{g(k)}$ with $g(k)=o(k)$. It is
promise-robust: since it is a lower bound for all inputs, the same
bound holds on any restricted input class, in particular on simple
connected graphs of diameter at most two, and the restriction only
matters because it makes the upper-bound construction smaller.
Both conventions appear in the literature and give the same
stable-equivalence relation: two graphs are $k$-Weisfeiler-Leman
equivalent under either convention exactly when their $k$-tuple
color histograms agree at every round. The pair budget in the
bijective game differs by one; joint equivalence needs $k+1$
pairs, separate equivalence needs $k$.
The lower bound is not a corollary of the Cai-Furer-Immerman
construction. That family, for each $k$, gives a pair of graphs
that is $k$-Weisfeiler-Leman equivalent but distinguishable under
$(k+1)$ colors. CFI rules out the existence of a smaller invariant
than the refined one; it does not rule out a faster algorithm that
computes the refined invariant.
./pdfs/cfi1992.pdf
Compressed variants of the CFI construction show that within
restricted description families, the same equivalence reduces
to separators of bounded size on suitably chosen subgraphs.
The constructions just described are designed to avoid such separators,
because a bounded separator would give the algorithm a shortcut.
./grohe-lichter-neuen-schweitzer-2025-cfi-compression.pdf
The lower bound is also not a corollary of the pebble-game lower
bounds of Berkholz or of Atserias-Dalmau-Kolaitis. Those results
give n^{Omega(k)} time for the existential pebble game, under
promise classes or restricted algorithm models. The bound just described
is stronger in scope (any deterministic sequential algorithm)
and weaker in parameter (exponent linear in $k$, not unbounded).
./berkholz-2013-existential-pebbles.pdf
Three further results place the picture in context but are not
ingredients of the proof.
Weisfeiler-Leman 1968 introduced the one-dimensional refinement
as a canonization heuristic and is the origin of the higher-
dimensional variants used above. Everything in the proof is
new, but the object of study has that paper as its source.
Grohe 1999 proved that equivalence in fixed-variable counting
logic is complete for polynomial time under the bijective pebble
game of the classical (rather than the joint) convention. The
game correspondence used below is in the same spirit, and the
convention choices are made explicit rather than absorbed.
./pdfs/grohe1999.pdf
Lichter, Rassmann, and Schweitzer 2024 and 2025 control the
Weisfeiler-Leman dimension of restricted graph classes; among
other things, on bounded-treewidth or bounded-genus graphs,
equivalence with counting logic is decidable with a much smaller
color budget than $k = \Theta(r)$. Those upper bounds do not
contradict the lower bound just described because the classes involved have
unbounded degree or exponential treewidth.
./pdfs/lrs2024.pdf
./pdfs/lrs2025.pdf
Doring and Neuen 2026 proved that the classical refinement
stabilizes in $O(n)$ rounds for every fixed $k$. The round count
is not the object of the lower bound: the round count can be
polynomial while the time complexity remains $n^{\Omega(k)}$
because each round costs a polynomial in the tuple count $n^k$.
./2609.17364v1.pdf
Seppelt 2024 gave an algorithmic meta theorem for homomorphism
indistinguishability which shows that a broad family of relaxation
procedures, including refined Weisfeiler-Leman hierarchies,
collapse in polynomial time. The result is orthogonal to a polynomial
time lower bound on the refined procedure itself.
./pdfs/seppelt2024.pdf
Description shape. A finite type set $T$, a finite link set $L$,
per-type one-coordinate label alphabets $A_{t,i}\subseteq[m]$, and
per-link local affine comparisons over the two-element field
$\mathbb{F}_2$ form a description shape. The construction below
realizes each description shape by a pair of vertex-colored graphs
of order $O_{S}(m^6)$, where the exponent six comes from two vector
readouts per type, two scalar vertical readouts per boundary, and
$O_S(m^2)$ blocks per pair. The relevant arc-consistency notion is
that of Mackworth, whose individual-edge form underlies both the
constraint-satisfaction and the two-variable-per-type descriptions
of the kind described above.
./pdfs/mackworth1977.pdf
Two obstacles lie between this description and a bounded-degree
Weisfeiler-Leman hardness witness.
Address hiding. A natural description indexes variables by all
$r$-tuples $(a_1,\ldots,a_r)\in[m]^r$. Exposing all $r$ coordinates
to the game at once forces a search over $m^r$ assignments, which
is far larger than the $O_S(m^6)$ budget. The construction exposes
only two adjacent coordinates per block, keeps the remaining
coordinates in the cyclic structure of a ring of $r$ blocks, and
recovers one full address at a time from a size-$r$ collection.
One-way propagation. Encoding a scalar Boolean value directly into
a graph readout allows the underlying graph to enforce both the
forward and the backward direction of propagation. That is wrong
semantically: a circuit gate whose output is true does not imply
that its inputs are true. A two-coordinate buffer, familiar from
constrained simulation of circuits, separates a source from its
destination so that a constrained destination never constrains its
source.
The proof proceeds through five stages.
1. The bijective game and its pair-count exactness. A two-player
correspondence is proved between joint and separate $k$-fold
refinement and the pebble game with the corresponding pair budget.
Joint equivalence corresponds to $k+1$ pairs and separate
equivalence to $k$ pairs.
2. Compression of arc consistency. A description shape $S$ of the
individual-edge form is realized by graphs of order $O_S(m^6)$,
exactly preserving the non-emptiness of arc-consistent sets.
3. Circuit simulation. Finite monotone circuits are encoded as
arc-consistency instances with the same shape, using two-coordinate
buffers for one-way propagation, and with explicit sequential
bounds for the construction.
4. Diagonal language. An explicit language is defined whose fixed
universal decider runs in polynomial time and whose one-tape
deciders cannot run within $m^s$ time at every sufficiently long
length.
5. Cutoff transfer. For each large $k$ and each fixed algorithm,
the padded graph pairs of orders in a polynomial interval past
$m^{20}$ are tried in a single diagonal machine. A single fast
trial at any order in the interval contradicts the diagonal
lower bound, so no order in the interval can be fast. This
transfers the diagonal bound to every sufficiently large order.
Two refinement conventions govern the correspondence. Under the
joint convention a single replacement step chooses a common vertex
and simultaneously replaces all $k$ coordinates by that vertex.
Under the separate convention each coordinate is replaced
independently, at its own chosen vertex.
Refinement, formally. Fix $k\ge 2$. Each finite vertex-colored
graph $X$ is $k$-tuple-colored by the atomic data of $k$-tuples. The
initial color $\chi_0^X(\bar v)$ of $\bar v=(v_1,\ldots,v_k)$
records the equality pattern $\{v_i=v_j\}_{i,j}$, the adjacency
pattern $\{E(v_i,v_j)\}_{i,j}$, and the sequence of vertex colors.
The update rule is joint or separate, as given above. Two graphs
$G,H$ are $k$-Weisfeiler-Leman equivalent under the chosen
convention if the color multisets on $V(G)^k$ and on $V(H)^k$
agree at every round $t$.
Stabilization. Under either rule the partition of each $V(X)^k$ by
the common color names refines monotonically and reaches a fixed
partition in finitely many rounds. Write $\bar u\sim\bar v$ for
stable equality of colors. Joint stability gives the extension
property that, for a stably equal pair $\bar u\sim\bar v$, a
bijection $f:V(G)\to V(H)$ exists satisfying
$$\bar u[i\leftarrow z]\sim\bar v[i\leftarrow f(z)]
\qquad\text{for every }z\in V(G)\text{ and every }i.$$
Separate stability gives, for every fixed coordinate $i$, a
bijection $f_i:V(G)\to V(H)$ satisfying
$\bar u[i\leftarrow z]\sim\bar v[i\leftarrow f_i(z)]$ for every $z$.
The two bijections $f_i$ for different coordinates may be
different. Under either rule, $\sim$ is invariant under
simultaneous permutation of the coordinates: if
$\bar u\sim\bar v$ and $\pi$ is any permutation of
$\{1,\ldots,k\}$, then $\pi\bar u\sim\pi\bar v$.
Bijective game. The bijective game with $K$ pairs on the pair
$(G,H)$ is a two-player game. There are $K$ pair slots. A slot is
either marked, by a pair $(u,v)\in V(G)\times V(H)$, or vacant.
Spoiler may remove any marked pairs. Spoiler then chooses a vacant
slot. Duplicator announces a bijection $f:V(G)\to V(H)$. Spoiler
chooses $z\in V(G)$ and marks that slot with $(z,f(z))$.
Duplicator loses if the currently marked pairs fail to preserve
vertex color, coordinate equality with other marked pairs, or
adjacency. The two conventions differ only in the bijections their
Duplicator is required to announce. Under the joint convention the
announced $f$ matches the joint replacement multiset of the
presently marked $k$-tuple of $G$-vertices with that of the
$H$-vertices. Under the separate convention, when slot $i$ is
refilled, the announced $f_i$ matches the separate replacement
multiset in coordinate $i$.
The following lemma is classical. The joint form is the pebble-game
formulation of Cai-Furer-Immerman; the specific pair budget $k+1$
under the joint convention appears in Kiefer-Neuen.
./pdfs/cfi1992.pdf
./pdfs/kn2019.pdf
Lemma (pair-count exactness). Let $G,H$ be finite graphs of equal
positive order. Put $K=k+1$ under the joint convention and $K=k$
under the separate convention. Then:
(i) Two $k$-tuples $\bar u\in V(G)^k$ and $\bar v\in V(H)^k$ have
equal stable colors iff Duplicator wins the $K$-pair game from the
position marking one pair per coordinate.
(ii) The stable $k$-tuple color histograms of $G$ and $H$ agree iff
Duplicator wins the $K$-pair game from the empty position.
Proof of (i), joint case, forward direction. The argument maintains
$K$ pair slots whose every $k$-element subfamily gives a stably
equal pair of $k$-tuples, with vacant slots treated as virtual and
admissible by a private invariant.
Base case. Duplicator starts from the position marking
$(\bar u,\bar v)$ on all $k$ coordinates plus one vacant spare. By
assumption the marked $k$-tuple has equal stable color, so the
invariant holds: the unique $k$-subset is the stated one.
Maintaining the invariant. Suppose the invariant holds at some
position with marked set $S$ of size $k$. Spoiler removes any
number of marked pairs and opens one vacant slot. Let $T\subseteq
S$ be any $k$-element subset of the remaining marked coordinates.
The joint extension property of the stably equal pair $T$ gives a
bijection $f:V(G)\to V(H)$ matching the joint replacement multisets
at every shared vertex. Duplicator announces $f$. Spoiler chooses
$z\in V(G)$ and the new slot is marked with $(z,f(z))$.
The invariant survives. Let $S'=S\cup\{\text{new slot}\}$ be the
new marked set, of size $k+1$. Take any $k$-subset $T'\subseteq
S'$. If $T'$ omits the new slot, $T'=T$ and joint stability of
$T$ was already established. If $T'$ contains the new slot, let
$T''\subseteq S$ be the $k$-element subset obtained by replacing
the new pair with any one pair of $S\setminus(T'\cap S)$; then
$T''$ is stably equal by the inductive invariant, and by choice of
$f$ the replacement multiset of $T''$ at the new position matches
the replacement multiset of $T$ at the new position, so $T'$
inherits stable equality of $T''$ at all shared positions and equal
replacement multisets at the new one. Hence $T'$ is stably equal.
Duplicator loses only if the currently marked pairs fail
coordinate-equality, adjacency, or vertex-color at some move.
Stable equality of any $k$-subset implies partial isomorphism on
that subset by induction on the round. So the invariant rules out
loss. This proves the forward implication in (i).
Proof of (i), joint case, reverse direction. Assume Duplicator wins
the $K$-pair game from a position marking $(\bar u,\bar v)$. Induct
on $t$ to prove $\chi_t^G(\bar u)=\chi_t^H(\bar v)$.
Base $t=0$. The winning initial position preserves vertex colors,
coordinate equality, and adjacency on the marked pairs. This is
exactly the initial atomic color.
Inductive step. Suppose $\chi_{\tau}^G(\bar u)=\chi_{\tau}^H(\bar
v)$ for $\tau\le t$. Spoiler opens the spare $K$-th pair. Duplicator
announces a bijection $f$. Spoiler may choose $z\in V(G)$ freely,
and Spoiler may remove any pair and reopen it, still on the same
spare slot. By the induction hypothesis continued over the
resulting positions, the marked set $\{z\}$ at the newly marked
position together with the previously marked $(k-1)$ pairs is
still a stably equal $k$-subset at round $t$. Varying $z$
therefore gives the equality
$$(\chi_t^G(\bar u[i\leftarrow z]))_{i=1}^{k}
= (\chi_t^H(\bar v[i\leftarrow f(z)]))_{i=1}^{k}$$
for each $z$, and consequently
$$\bigl\{\!\bigl\{(\chi_t^G(\bar u[i\leftarrow z]))_{i=1}^{k}
: z\in V(G)\bigr\}\!\bigr\}
= \bigl\{\!\bigl\{(\chi_t^H(\bar v[i\leftarrow z]))_{i=1}^{k}
: z\in V(H)\bigr\}\!\bigr\}.$$
Hence $\chi_{t+1}^G(\bar u)=\chi_{t+1}^H(\bar v)$.
Reverse case for the separate convention is the same with $K=k$
pairs and the per-coordinate bijections $f_i$ replacing the single
common $f$. In the forward direction, the separate extension
property supplies $f_i$ one slot at a time. The invariant is that
the full $k$-tuple is stably equal, and each refill of slot $i$
uses $f_i$ from the current tuple's separate replacement multiset.
Proof of (ii). Fix a stable color $\theta$ on the $G$-side. Suppose
the histogram of $\theta$ in $V(G)^k$ is $\mu$. Claim the histogram
of $\theta$ in $V(H)^k$ is also $\mu$. Lay out $k$ pair slots.
Sequentially, for a chosen $G$-tuple $\bar u$ of color $\theta$,
fill slot 1 using any $f$, slot 2 using the $f$ announced after
slot 1 is filled, and so on. The composition of the sequentially
announced bijections is a bijection $\Phi:V(G)^k\to V(H)^k$ with
$\chi_\infty^H(\Phi(\bar u))=\chi_\infty^G(\bar u)$ for every
$\bar u$. Hence histograms agree in both directions.
Conversely, if the two histograms agree, then Duplicator can play a
strategy based on matching histogramed colors at each round: given
a currently marked $k$-tuple $\bar u$ of color $\theta$, extend to
a $G$-tuple $\bar u'$ of color $\theta'$ using the same $\Phi$, and
pad with virtuals. This never loses. So Duplicator wins from the
empty position.
This proves (ii) and completes the pair-count exactness.
./pdfs/grohe1999.pdf
Disjoint unions. The following lemma isolates the conventions under
which pure tuples behave like direct comparisons between $G$ and
$H$ even when the two graphs are placed in one disjoint union.
Lemma (pure tuples in a disjoint union). Suppose $k\ge 3$ and
$G,H$ are connected graphs of diameter at most two. Let
$D=G\sqcup H$ and run either refinement convention on $D$,
including mixed $k$-tuples. The stable color histograms restricted
to $V(G)^k$ and $V(H)^k$ are equal iff the separate-input histograms
of $G$ and $H$ are equal.
Proof. Stable colors on $D$ determine, for each pair of coordinates
$u,v$, the three relations
$$u=v,\qquad E(u,v),\qquad
\exists z\,\bigl(E(u,z)\wedge E(z,v)\bigr).$$
The existential clause is recovered from stable colors by replacing
a third coordinate and inspecting its two adjacencies in the
replacement colors. This works under both update conventions. By the
diameter-two assumption the displayed condition is exactly
membership in the same component of $D$. Hence stable colors
identify the component of every pure tuple.
Take two related pure tuples, one in $V(G)^k$ and one in $V(H)^k$.
Suppose they are stably equal. The witness bijection on $D$ (joint
or per-coordinate) maps replacement vertices in the $G$-component
into the $H$-component and vice versa; a replacement of any
coordinate is anchored by the other coordinates, so no replacement
vertex can stay in the wrong component. The restriction of that
witness is a bijection $V(G)\to V(H)$. Equal pure histograms supply
an initial related $k$-tuple, and the resulting invariant matches
the joint or separate invariant of the pair-count lemma applied to
$G,H$ directly. Hence Duplicator wins between $G$ and $H$
separately.
Conversely, if Duplicator wins between $G$ and $H$, then on $D$
against itself play the component swap: use the $G,H$ strategy on
$G$-chosen vertices and the inverse strategy on $H$-chosen
vertices. Cross-component entries have neither equality nor
adjacency on either side, so the swap is legal. This is a winning
strategy on $D$, and the successive-bijection argument of the
pair-count lemma, applied to $D$, implies that pure histograms on
$V(G)^k$ and $V(H)^k$ are equal.
Parameter choice. The remainder of the argument uses $K=r+1$ pair
slots and assumes $r\ge 3$. Under the joint convention $r=k$; under
the separate convention $r=k-1$. Thus a query ring occupying $r$
slots has exactly one spare slot for transporting an answer. The
final graphs constructed in the compression step have a universal
hub, so the pure-tuple lemma applies to the disjoint-union
convention on the final graphs.
Compression. The construction below converts individual-edge arc
consistency for a description shape into equality of two graphs, in
the sense of the (r+1)-pair bijective game.
Throughout this step fix an integer $r\ge 3$, put $K=r+1$, and
work over the two-element field $\mathbb{F}_2$.
Real types and edge schemas. Let $\mathcal{P}$ be a finite set of
real types, each with a vector dimension $d_P\in\mathbb{N}$ over
$\mathbb{F}_2$. Variables of type $P$ are indexed by full addresses
$\mathbf{a}=(a_1,\ldots,a_r)\in[m]^r$, with
$[m]=\{0,\ldots,m-1\}$ and $m\ge 2$, and take values in
$\mathbb{F}_2^{d_P}$. An edge schema $e$ specifies ordered endpoint
types $P,R$ (possibly equal); per-coordinate label sets
$A_{e,i}\subseteq[m]$ and injections $\sigma_{e,i}:A_{e,i}\to[m]$
for $i=1,\ldots,r$; and two affine forms
$$\phi_{e,0}(u)=\lambda_{e,0}u+d_{e,0}, \quad
\phi_{e,1}(u)=\lambda_{e,1}u+d_{e,1},$$
with linear parts $\lambda_{e,0}\in(\mathbb{F}_2^{d_P})^\ast$,
$\lambda_{e,1}\in(\mathbb{F}_2^{d_R})^\ast$, and constants
$d_{e,0},d_{e,1}\in\mathbb{F}_2$; the linear parts may vanish.
Put $A_e=\prod_{i=1}^{r}A_{e,i}$ and
$\boldsymbol\sigma_e(\mathbf{a})=(\sigma_{e,1}(a_1),\ldots,
\sigma_{e,r}(a_r))$.
Individual comparisons. For every $\mathbf{a}\in A_e$ the schema
imposes exactly one individual comparison
$$\phi_{e,0}\bigl(h_P(\mathbf{a})\bigr)
=\phi_{e,1}\bigl(h_R(\boldsymbol\sigma_e(\mathbf{a}))\bigr),$$
where $h_P(\mathbf{a})\in\mathbb{F}_2^{d_P}$ is the variable of type
$P$ at address $\mathbf{a}$, and $h_R$ is defined analogously.
Parallel comparisons are kept separate and are not combined.
Individual-edge arc consistency. The instance has individual-edge
arc consistency if nonempty sets
$Q_{P,\mathbf{a}}\subseteq\mathbb{F}_2^{d_P}$ exist, one per real
type and per address, with
$$\phi_{e,0}(Q_{P,\mathbf{a}})
=\phi_{e,1}(Q_{R,\boldsymbol\sigma_e(\mathbf{a})})
\qquad\text{for every }e\text{ and every }\mathbf{a}\in A_e.$$
The equalities are imposed separately. The support of one endpoint
value depends on that value and on the schema $e$ alone.
This is Mackworth's local-support condition for arc consistency, in
a two-variable-per-comparison form. It is not a global constraint
satisfaction: parallel comparisons at the same address do not need
a common solution, only a common supporting image.
Description shape. A description shape $S$ fixes the finite real-type
set, the per-type dimensions, the finite schema set and its
incidence, and the number of coordinate tables. The coordinate sets
$A_{e,i}\subseteq[m]$ and injections $\sigma_{e,i}$ may depend on
$m$, and are given by one-coordinate tables of size $O(m)$ each. The
affine forms are bounded in number. The whole instance is therefore
specified from $O_S(m)$ bits of tables together with the affine
forms.
The compression theorem. For every fixed $r\ge 3$ and every fixed
description shape $S$, there are two equally large simple uncolored
connected graphs $G^0,G^1$ of diameter at most two and order
$O_{S,r}(m^6)$, with the property that Duplicator wins the
$(r+1)$-pair bijective game on $(G^0,G^1)$ under the joint
convention if and only if the underlying instance has
individual-edge arc consistency. The construction uses only the
coordinate tables and the affine forms, never looping over full
addresses. An arbitrary common number of additional vertices can be
attached to both graphs at a universal hub while preserving the
equivalence conclusion, connectedness, and the diameter bound.
Two refinements of the construction ease the exposition. An unused
real type of dimension one may be introduced at the outset without
affecting arc consistency; this guarantees at least two distinct
valuation vertices. Subdividing each schema by a long wire keeps
every small block collection near at most one original real type.
Wire subdivision. Replace each schema $e$ by a path with $4(r+1)$
private internal types of dimension one. This subdivided path is a
wire; its endpoints are the original real types, and its segments
are links. At an internal type of $e$, the allowed labels in
coordinate $i$ are $A_{e,i}$; at a real type every label in $[m]$ is
allowed. Along the wire the coordinate matches are identity matches
on the allowed labels, except at the second real endpoint, where the
match is $p\mapsto\sigma_{e,i}(p)$.
Local comparison. Each link $\ell$ with endpoints $t,u$ carries a
scalar comparison
$$L_{\ell,t}h_t+L_{\ell,u}h_u=b_\ell.$$
An internal link has $L_{\ell,t}=L_{\ell,u}=\text{identity}$ and
$b_\ell=0$. A link with a real endpoint uses the linear part of that
real endpoint's affine form, identity at the other endpoint, and the
constant term of the real endpoint's affine form as $b_\ell$. The
internal scalar readout records one application of that affine form.
For analysis only, each coordinate injection is extended to a
permutation of $[m]$; the links themselves use only the allowed
matches.
Corners and boundaries. Boundary indices $i=1,\ldots,r$ are cyclic,
with $r+1$ identified with $1$. Put $\delta_i=1$ for $i=r$ and
$\delta_i=0$ otherwise. A corner is a triple $(i,t,p)$ with $p$ an
allowed label at boundary $i$ of type $t$. Two kinds of blocks are
used.
Site block. A site block at type $t$, row $i$, and allowed labels
$p,p'$ carries one vector readout $x\in\mathbb{F}_2^{d_t}$, named by
the horizontal edge from $(i,t,p)$ to $(i+1,t,p')$. All values are
legal.
Square block. A square block at link $\ell=tu$, row $i$, and
allowed matches at boundaries $i,i+1$ carries two horizontal
readouts $x_t,x_u$ and two scalar vertical readouts $y_i,y_{i+1}$;
a vertical readout is named by its boundary, link, and matched
label pair. In version $\varepsilon\in\{0,1\}$ the legal valuations
satisfy
$$L_{\ell,t}x_t+L_{\ell,u}x_u+y_i+y_{i+1}=\varepsilon\delta_i b_\ell.$$
Version $0$ is homogeneous; version $1$ is affine. The legal
valuations of any block form a linear space in version zero and a
nonempty affine coset of a linear space in version one. For a
square this follows from the coefficient one of $y_i$.
Readout sharing. Two occurrences of a readout with the same name
denote the same vector or scalar. A valuation of a block specifies
all its horizontal and vertical readouts. The legal valuations of
each block form a nonempty affine solution coset over
$\mathbb{F}_2$.
Valuation graphs. Construct vertex-colored graphs as follows. The
vertices are all legal block valuations, one color per block.
Between two distinct blocks $B,B'$ sharing at least one readout
name, place an edge exactly when the two valuations agree on every
shared name. No other edges exist. Corresponding blocks have
equally many vertices on both sides.
Necessity. The following lemma converts a winning $(r+1)$-pair
strategy on the valuation graphs into arc consistency.
Lemma (necessity). A block-preserving winning strategy with $r+1$
pairs on the colored valuation graphs implies individual-edge arc
consistency.
Proof. Fix a version-zero graph on the source side and a version-one
graph on the target side. Spoiler always picks the all-zero valuation
on the source side; every source-side block is homogeneous, so
all-zero is legal there. Whenever two marked distinct blocks share
readouts, their zero readings agree there, so the marked readings
pass every shared-name test. A winning strategy for Duplicator
therefore exists in plays consistent with this zeroing. Winning
positions are closed under removal, so the whole argument may be
restricted to positions with no more than $r+1$ marked pairs at a
time.
Fix a real type $P$ and an allowed full address
$\mathbf{a}=(a_1,\ldots,a_r)$. The site ring at $(P,\mathbf{a})$
consists of the $r$ site blocks using the address labels at
consecutive boundaries. Let $Q_{P,\mathbf{a}}$ consist of all sums of the $r$ horizontal
readouts on the target-side site ring at $(P,\mathbf{a})$, taken
over plays consistent with the winning strategy in which the
source side is zeroed and all other pairs are discarded. The sets
are nonempty: Spoiler can ask for such a ring from the empty
position, and the winning strategy then supplies target-side
readings whose sum lies in $Q_{P,\mathbf{a}}$.
Take a schema $e$ from $P$ to $R$ and an address $\mathbf{a}\in A_e$.
Starting from a marked, source-zeroed site ring at $(P,\mathbf{a})$,
replace each site block by the corresponding square block along
the wire for $e$, one row at a time: place the square while
retaining the old site, then discard the old site. Each move
occupies the spare pair and then frees it again, so at most $r+1$
slots are ever in use. While both the site and its square are
marked, the winning strategy forces agreement at their shared
horizontal readout, so the sum of target-side square readouts
equals the sum already collected at the site ring. Once all $r$
squares are marked on the target side, adjoining vertical readouts
agree, and summing the version-one square equation over the $r$
rows gives $L_{\ell,t}h_t+L_{\ell,u}h_u=b_\ell$ for the two side
sums of horizontal readouts. Replace the squares by sites at $u$ in the same
manner, preserving the $u$-side horizontal sum. Repeating along the
subdivided wire for $e$ transmits the affine comparison to the
second real endpoint $R$ at the matched address
$\boldsymbol\sigma_e(\mathbf{a})$. The same construction runs in
reverse: any admissible sum at
$(R,\boldsymbol\sigma_e(\mathbf{a}))$ transmits back to
$(P,\mathbf{a})$.
Therefore
$$\phi_{e,0}(Q_{P,\mathbf{a}})
=\phi_{e,1}(Q_{R,\boldsymbol\sigma_e(\mathbf{a})})$$
for every schema $e$ and every $\mathbf{a}\in A_e$. This is exactly
individual-edge arc consistency, and it completes the proof.
Corner graphs. For a set $U$ of blocks, let $\Gamma_U$ be the graph
on all corners of blocks in $U$, with their named horizontal and
vertical edges. Every block is connected in $\Gamma_U$ and therefore
belongs to a single component. The type support of a component is
the set of types and links of its blocks, viewed in the subdivided
type multigraph indexed by the $r$ rows.
Reference type. Choose a reference type inside a component support.
At each boundary, extend the coordinate matches along tree paths
inside the support to permutations of $[m]$ (as already permitted in
the analysis) and align all corner labels to labels at the
reference type. Vertical edges preserve the aligned label. On a
connected subtree the alignments restrict consistently, up to the
choice of reference type.
Support lemma. If $|U|\le r+1$, every component's type support is a
tree containing at most one real type. With no real type, the
support lies inside one wire interior. With a real type, it consists
of that type together with short arms of incident wires.
Proof. Each square block contributes one link, so a support of
$|U|\le r+1$ blocks is connected and uses at most $r+1$ distinct
links. Each subdivided wire has $4(r+1)+1$ links. Reaching both real
endpoints of a wire, or closing a cycle in the support, requires
traversing an entire wire and hence at least $4(r+1)+1$ blocks. With
$|U|\le r+1<4(r+1)+1$, this is impossible. This also handles a
subdivided original loop and any cycle arising from parallel
schemas. Internal types are private to their wires, giving the
remaining claims.
Wrapping. A collection of blocks is wrapping if its corner graph
has a closed walk traversing an odd number of horizontal edges in
row $r$, counted with multiplicity. The site ring is one example of
a wrapping witness.
Address recovery lemma. For block sets contained in a set $U$ of
size at most $r+1$:
(i) Every wrapping collection has at least $r$ blocks.
(ii) A wrapping collection of size $r$ has one block in every row,
all in one component, and determines a consistent full address in
the aligned coordinates of that component.
(iii) All wrapping subcollections of $U$ of size $r$ lie in one
component and determine the same aligned full address.
Proof. For any closed walk, the parity of its horizontal traversals
is the same in every row: at each boundary, the total incidence
parity is zero, while vertical traversals contribute twice at that
boundary. Odd seam parity therefore requires an odd number of
traversals in every row and hence at least one block per row.
With exactly $r$ blocks, there is one per row and the witnessing
walk meets them all. All horizontal edges of the block in a given
row share the same pair of aligned labels. At boundary $i$, apply
parity conservation separately at each aligned label, combining
different types. Vertical edges preserve the label. Since both
incident rows have odd traversal parity, the labels so specified at
boundary $i$ must agree. These labels give the full address of the
size-$r$ collection.
Two size-$r$ subcollections of $U$ share at least $r-1$ blocks in
distinct rows, lie in one component, and can differ only in the
remaining row. Every boundary has an incident common row when
$r\ge3$, so the recovered addresses agree in every coordinate.
Full-address restrictions. A full-address restriction is imposed
only when a size-$r$ subcollection wraps. This is the only
information that can persist in at most $r$ occupied blocks before a
new game move. A collection that first wraps at $r+1$ blocks gets no
such restriction: its proper subsets are nonwrapping, and the
potential adjustment below lets their shifts change without altering
their readouts.
Compatible families of offsets. Assume arc consistency. For an
internal type of wire $e$ and an allowed address $\mathbf{a}\in A_e$,
define its scalar set to be
$$Q_{t,\mathbf{a}}
= \phi_{e,0}(Q_{P,\mathbf{a}})
= \phi_{e,1}(Q_{R,\boldsymbol\sigma_e(\mathbf{a})}).$$
By the arc consistency equation, this is nonempty and equal at
every internal type of that wire, whose labels use its first address
system.
Fix a set $U$ of blocks with $|U|\le r+1$. A compatible family
$\mathcal{H}_U$ of affine valuations of the blocks in $U$ is
constructed below. Each member serves as an offset assignment for
translations later; it need not be an actual vertex currently marked
by Spoiler or Duplicator. Each member is represented by component
shifts and corner potentials, and two representations may give the
same readouts.
Component shifts. For each component $C$ of $\Gamma_U$,
independently choose a shift vector $h_t\in\mathbb{F}_2^{d_t}$ for
each type of its support, satisfying the link equation
$$L_{\ell,t}h_t+L_{\ell,u}h_u=b_\ell$$
on every support link. If $C$ contains a wrapping subcollection of
size $r$, impose one additional $Q$ condition at its address from
the address recovery lemma. If the support has a real type $P$,
require $h_P\in Q_{P,\mathbf{a}}$, expressing the address at $P$.
If the support lies in a wire $e$ with no real type, require the
common internal scalar to belong to $Q_{t,\mathbf{a}}$, expressing
the address in that wire's system. In the second case the address
is allowed for the entire wire, because every coordinate is read by
a block of the wrapping collection at an internal type. Real
addresses are unrestricted, so an incomplete arm out of a real
type $P$ need not allow the full address.
Existence and parametrisation. Call a shift family satisfying the
link equations and the applicable $Q$ condition admissible. On an
interior support it is parametrised by one common scalar. On a
support with a real type, it is parametrised by one real vector,
and the scalar on each arm is the corresponding endpoint affine
form of that vector, constant down the arm. Admissible shifts
exist, since the required $Q$ sets are nonempty, and, when no $Q$
condition is imposed, the parameter is arbitrary. For an original
loop, its two short arms are treated separately, and the support
cannot traverse the interior connecting them.
Corner potentials. Choose an arbitrary vector
$M_v\in\mathbb{F}_2^{d_t}$ at each corner $v$ of type $t$. Define
the readouts by
$$x_{vw} = M_v+M_w+\delta_i h_t
\quad\text{on a horizontal edge in row }i\text{ at type }t,$$
$$y_{vw} = L_{\ell,t}M_v+L_{\ell,u}M_w
\quad\text{on a vertical edge of link }\ell=tu.$$
Let $\mathcal{H}_U$ be the family of all readout assignments obtained
this way. Substituting in a square, every potential term cancels,
leaving
$\delta_i\bigl(L_{\ell,t}h_t+L_{\ell,u}h_u\bigr)=\delta_i b_\ell$,
which holds by the link equations. Every assigned valuation is
therefore legal, and readouts with the same name agree. The family
is nonempty, including for $U=\emptyset$.
Site ring sum. For a site ring at type $t$ and address
$\mathbf{a}$, write $M_i=M_{(i,t,a_i)}$ and $M_{r+1}=M_1$. The
compatible offset readouts satisfy
$$\sum_{i=1}^r x_i
= \sum_{i=1}^r\bigl(M_i+M_{i+1}+\delta_i h_t\bigr) = h_t.$$
Each corner potential appears twice, and row $r$ contributes the
component shift $h_t$.
Projection lemma. For every $V\subseteq U$ with $|U|\le r+1$,
$$\mathcal{H}_U\big|_V = \mathcal{H}_V.$$
Proof. If $V=U$ the claim is trivial. Assume $V\subsetneq U$, so
$|V|\le r$. If a component of $\Gamma_V$ wraps, the address
recovery lemma requires at least $r$ blocks, so it uses all $r$
blocks of $V$; at most one such component can occur.
Admissible shifts on a retained wrapping component. Let $D$ be a
wrapping component of $\Gamma_V$ contained in a component $C$ of
$\Gamma_U$. Compare all recovered addresses in the alignment of
$C$'s support. The size-$r$ witness in $D$ is also in $C$, so the
address recovery lemma gives the same address for $D$ and for the
$Q$ condition on $C$. Restricting admissible shifts from $C$ to $D$
gives exactly all admissible shifts on $D$. Three cases cover the
possibilities.
Case (both supports contain a real type). It is the same type, with
the same $Q$ restriction. Its real vector determines every arm
scalar in either support. Every allowed vector therefore extends by
assigning the newly present arm scalars.
Case ($C$ has no real type). Both supports lie in the same wire
interior. They are parametrised by the same common scalar, subject
to the same $Q$ restriction, so restriction is exact.
Case (only $C$ contains a real type). Then $D$ lies inside one arm
of a wire $e$ with ordered real endpoints $P,R$. Write its internal
address as $\mathbf{a}\in A_e$. The internal coordinates use the
first endpoint's system. Since $a_i\in A_{e,i}$ for every $i$, the
permutation extending $\sigma_{e,i}$ sends $a_i$ to the matched
label $\sigma_{e,i}(a_i)$, and its inverse returns that label to
$a_i$. All other matches along the wire are identities. The
recovered address is therefore $\mathbf{a}$ at the first endpoint
$P$ and $\boldsymbol\sigma_e(\mathbf{a})$ at the second endpoint
$R$. The definition of the internal scalar set gives
$$\phi_{e,0}(Q_{P,\mathbf{a}}) = Q_{t,\mathbf{a}}
= \phi_{e,1}(Q_{R,\boldsymbol\sigma_e(\mathbf{a})}).$$
Using the equality for the endpoint reached by $C$, every
admissible old scalar has an admissible real preimage, and every
admissible real vector restricts to an admissible old scalar.
Choose the real preimage, then assign the scalars on the other
arms from that vector. The remaining endpoint statements stay
separate when $P=R$.
These cases exhaust the possibilities, since any real type in $D$
also belongs to $C$.
Restriction of readouts. Take a member of $\mathcal{H}_U$ and one
representation by shifts and potentials. Restrict both to each
component $D$ of $\Gamma_V$. The link equations remain valid. If
$D$ wraps, the shift fact just proved preserves its $Q$ condition;
if $D$ does not wrap, no $Q$ condition is imposed. The formulas for
$x$ and $y$ give the same readouts on $V$. Hence
$\mathcal{H}_U|_V\subseteq\mathcal{H}_V$.
Extension of retained readouts. Fix $a_V\in\mathcal{H}_V$, and
choose one representation: shifts $h_t^D$ on each old component
$D$, and corner potentials $M_v$. On each new component $C$ choose
admissible shifts $\widehat h_t^C$. If $C$ contains the wrapping
old component, choose these shifts to agree with $h_t^D$
throughout that support, which the shift restriction fact makes
possible. Since a wrapping old component uses all $r$ blocks of
$V$, no new real shift interferes with two independently prescribed
old arm scalars.
The new shifts already agree on a wrapping old component. On each
nonwrapping $D$, adjust the potentials so the new shifts produce
the original readouts $a_V$. Mark each horizontal edge in row $i$
with $\delta_i$ and each vertical edge with zero. Every closed walk
in $D$ has mark sum zero. Summing marks along paths from a root
therefore gives bits $s_v$ with $s_v+s_w$ equal to the mark of
every edge $vw$.
For a type $t$ of $D\subseteq C$, put $g_t=h_t^D+\widehat h_t^C$,
the difference of the old and new shifts over $\mathbb{F}_2$.
Both shift families satisfy the same affine link equations, so
$$L_{\ell,t}g_t = L_{\ell,u}g_u$$
on every support link. Replace the old potentials of type $t$ by
$M'_v=M_v+s_v g_t$. Including the change of shift, the change in a
horizontal readout is $(s_v+s_w)g_t+\delta_i g_t=0$. For a vertical
edge, $s_v=s_w$, and the change in its readout is
$s_v L_{\ell,t}g_t+s_w L_{\ell,u}g_u=0$. Every retained readout is
preserved.
The adjustment is performed independently on each nonwrapping
component, and the old potentials are kept on a wrapping component.
Distinct old components have disjoint corner sets, even if their
supports share types or the new blocks merge them. Potential
assignments therefore do not conflict. Assign arbitrary potentials
to new corners of $\Gamma_U$. Together with the chosen shifts, they
represent a member of $\mathcal{H}_U$ whose readouts on $V$ are
exactly $a_V$. This proves $\mathcal{H}_V\subseteq\mathcal{H}_U|_V$.
This also covers a set $U$ that first wraps at size $r+1$. Such a
$U$ has no size-$r$ wrapping subcollection, and all its proper
subsets are nonwrapping. No retained shift must stay fixed, and the
same potential adjustment preserves every retained readout.
This completes the projection lemma.
Sufficiency lemma. Individual-edge arc consistency implies a
block-preserving winning strategy with $r+1$ pairs on the colored
valuation graphs.
Proof. For the set $U$ of blocks containing pebbled vertices,
maintain offsets $(a_B)_{B\in U}\in\mathcal{H}_U$. A homogeneous
vertex $z$ in block $B$ is matched to the affine vertex $z+a_B$. On
discarding pebbles, discard offsets only for blocks no longer
occupied; the invariant is retained by the projection lemma.
Before placing a new pair there are at most $r$ occupied blocks.
For each unoccupied block $B$, independently extend the retained
offsets to a member of $\mathcal{H}_{U\cup\{B\}}$, and use its
offset $a_B$. For occupied blocks keep the old offsets. On every
block, translation by $a_B$ is a bijection from its full homogeneous
solution space onto its full affine solution coset. The union of
these bijections is a bijection of the vertex sets. Only one new
block is selected, so its chosen extension preserves the
invariant. The family $\mathcal{H}_{\{B\}}$ need not contain all
affine valuations of $B$; any one legal offset already supplies the
required block bijection.
Offsets on shared readouts agree. Adding the same offset to the
readouts of two pebbled valuations preserves both their agreement
and their disagreement, including when several readouts are shared.
Thus adjacency and nonadjacency between distinct blocks are
preserved. Within one block, injectivity of translation preserves
equality and there are no edges. Multiple pebbles in a block cause
no difficulty. These bijections therefore maintain a partial
isomorphism forever, and Duplicator wins.
Uncolored graphs, padding, and size. Let $N$ be the common number
of valuation vertices, and number the blocks $1,\ldots,B$, where
$B\le N$ since every block carries at least one valuation. For each
valuation vertex in block $j$, add $j(N+1)$ private marks, adjacent
to their owner and nowhere else. Add a universal hub adjacent to
every other vertex, including all marks. For padding, add any
desired number $q\ge0$ of vertices adjacent only to the hub, using
the same $q$ in both graphs. The resulting graphs are simple,
connected, and of diameter at most two.
Degree decoding. A base valuation vertex in block $j$ has degree in
$$[\,j(N+1)+1,\ j(N+1)+N\,].$$
These intervals are disjoint and lie above two. Marks have degree
two and padding vertices have degree one. The hub has strictly
greater degree than every base vertex when $N\ge2$: it is adjacent
to all base vertices and all marks, whereas a base vertex sees only
its own marks and at most $N-1$ other base vertices, together with
the hub, and there are marks owned by other base vertices. Thus
degrees identify each base block and distinguish the hub.
A winning strategy with at least two pairs must preserve degrees at
every reached position. Otherwise Spoiler retains the mismatched
pair alone and asks to place another pair. A degree discrepancy
prevents any proposed bijection from preserving membership in the
two neighborhoods, so one selection loses immediately.
Consequently, any winning strategy on the uncolored graphs respects
base blocks whenever Spoiler plays on base vertices. The necessity
lemma still derives arc consistency from such a strategy.
Conversely, augment the sufficiency strategy as follows. A pebbled
mark activates its owner's block just as a pebbled base vertex does.
Retain a joint member of $\mathcal{H}_U$ for all active blocks, even
if some have only marks pebbled. Each pebble activates at most one
block. Before a new placement, $|U|\le r$, so the same separate
extensions provide translations for all base blocks. Map each mark
to the mark with the same local number at its translated owner.
Match the hubs and use a fixed bijection on padding vertices. This
is a vertex bijection, and any selection activates at most one new
block. Base-to-base adjacency is preserved as before; mark-to-base
adjacency is preserved by the owner translation; all other
adjacency and equality conditions follow directly from the
construction. This proves the claimed equivalence for every
amount of padding.
Size. A site block is specified by a type, a row, and two labels. A
square block is specified by a link, a row, and two coordinate
matches, each determined by one first-side label. There are
therefore $O_{S,r}(m^2)$ blocks. The dimensions are fixed, so each
block has a bounded number of valuations and $N=O_{S,r}(m^2)$. The
total number of marks is at most
$$NB(N+1)=O_{S,r}(m^6).$$
The unpadded order has the same bound. All blocks, valuations, and
marks are enumerated from the bounded scalar-form data together
with the one-coordinate tables; their definitions never require a
loop over full addresses.
This proves the compression theorem.
Circuits and computation. The next reduction converts an
arc-consistency instance into the existence of a monotone circuit
computation. Two independent difficulties arise. The first is
representing Boolean values as arc-consistency images: truth of a
gate must force its output image to be $\{0\}$. The second is
maintaining the direction of propagation: a direct equality between
a source output and a destination port would also transmit
restrictions backward, and backward propagation is semantically
wrong, since a true output does not imply true inputs. A
two-coordinate buffer, in the style of the monotone-circuit
reductions for finite-variable equivalence, resolves the second
difficulty.
Gate conventions. A monotone circuit is a finite acyclic directed
network of two kinds of gates. A scalar gate is an OR gate, possibly
with no incoming connections, and is possibly seeded. An AND gate
has two input ports; each port itself takes the OR of all
connections entering it; the gate is true iff both ports are true.
An empty OR is false. A scalar gate is true iff it is seeded or it
receives a true incoming connection. A designated test gate is a
scalar gate with no outgoing connections. These rules determine
every gate's truth value in a fixed topological order.
Circuit simulation proposition. To such a circuit one can associate
an individual-edge arc-consistency instance over $\mathbb{F}_2$,
with vector dimensions at most two, that has nonempty arc-consistent
sets iff every test gate is false.
If the circuit is specified by gate types indexed by $[m]^r$, by
connection schemas with product domains and componentwise partial
bijections, and by seed and test requests that are unions of
product domains, then the consistency instance has the same form.
A bounded number of gate types, connection schemas, and product
requests gives a bounded number of consistency types and edge
schemas, independently of $m$.
Proof. Assign a one-dimensional vector variable to each scalar
gate. Its input and output directions are both the identity on
$\mathbb{F}_2$. Assign a two-dimensional vector variable
$(x_1,x_2)\in\mathbb{F}_2^2$ to each AND gate, with input
directions the two coordinate projections and output direction
$x_1+x_2$. Truth is encoded by forcing the corresponding output
image to $\{0\}$.
A seed is constrained by comparing its scalar direction with the
constant form zero on a fresh dummy variable. A test is constrained
by comparing its scalar direction with the constant form one on a
fresh dummy variable. Both are permitted affine forms with zero
linear part; the dummy variable itself can have any nonempty set of
values.
For each connection $c$ from a source output $o_c$ to a destination
port $i_c$, introduce a private two-dimensional buffer variable
$(z_c,z'_c)\in\mathbb{F}_2^2$ and three separate comparisons
$$o_c = z_c, \qquad o_c = z'_c, \qquad z_c + z'_c = i_c.$$
Each equality means equality of the two scalar images of the
corresponding nonempty sets. In particular, the first two
comparisons are individual edges; they are not combined into a
joint constraint.
Suppose an arc-consistency witness exists. If a source output has
image $\{0\}$, the first two comparisons force both buffer
coordinates to have image $\{0\}$. The nonempty buffer set is
therefore the singleton $\{(0,0)\}$, and the third comparison
forces the destination port image to be $\{0\}$. A true scalar
gate has image $\{0\}$ either because it is seeded or because it
receives a true incoming signal. A true AND gate has both
coordinate images $\{0\}$, hence also has output image $\{0\}$.
Induction over the circuit proves this assertion for every true
gate. A true test would additionally require image $\{1\}$, which
is impossible. Therefore no test is true.
Conversely, assume every test is false. At an ordinary scalar gate
take $\{0\}$ if it is true and $\mathbb{F}_2$ if it is false; at a
test take $\{1\}$. These choices are compatible because no test is
true. At an AND gate take the nonempty affine set
$$\{(x_1,x_2)\in\mathbb{F}_2^2 :
x_j = 0 \text{ for each true input port } j\}.$$
A true AND has output image $\{0\}$; a false AND has a free
coordinate, whose change toggles the sum, so its output image is
$\mathbb{F}_2$. Every false gate that is a source of a connection
therefore has full output image. Terminality of the tests is
essential: a false test has image $\{1\}$, but is never a source.
For a connection with true source, the destination port is true,
and the buffer set is $\{(0,0)\}$. For a connection with false
source, let $D$ be the nonempty image already chosen for its
destination port, and take
$$B_D = \{(z,z')\in\mathbb{F}_2^2 : z+z'\in D\}.$$
The three possible cases are:
$D=\{0\}$: $B_D=\{(0,0),(1,1)\}$, each coordinate image is
$\mathbb{F}_2$, sum image $\{0\}$.
$D=\{1\}$: $B_D=\{(0,1),(1,0)\}$, each coordinate image is
$\mathbb{F}_2$, sum image $\{1\}$.
$D=\mathbb{F}_2$: $B_D=\mathbb{F}_2^2$, each coordinate image is
$\mathbb{F}_2$, sum image $\mathbb{F}_2$.
These choices verify all three comparisons. Forcing a destination
port to zero does not force a false source to zero: the buffer can
use the diagonal set. All dummy comparisons also hold, proving the
first assertion.
For the schematic assertion, give each connection schema its own
buffer type in the source address system, and restrict all three
new schemas to the connection's source product domain. The first
two new schemas use identity address transmission; the third uses
the original componentwise partial bijection. Each allowed buffer
address then participates only in the three comparisons for the
intended individual connection; unused buffer addresses are
unrestricted. Seed and test comparisons use identity transmission
to a dummy type on their stated product domains. Unions of domains
are handled by separate schemas; repeated requests for the same
constant are harmless. There is one new two-dimensional type and
three schemas per connection schema, and only a bounded additional
number for constant comparisons. This proves that the short
description is preserved.
Turing-machine circuit. The next theorem converts a machine
M's acceptance, restricted to a time-and-space budget, into a
monotone circuit whose addresses are base-m digit dictionaries
over $[m]^r$. Combined with the circuit simulation proposition and
the compression theorem, this yields the reduction used for the
final diagonal argument.
Theorem (Turing-machine circuit). Fix a machine $M$ and an
integer $r\ge 3$; put $d=\lfloor r/3\rfloor$. There is a single
effective construction, depending only on $M$ and $r$, with the
following property. For each $m\ge 2$ such that $M$ halts on every
length-$m$ input within an integer bound $T_0(m)$ satisfying
$$T_0(m)<m^d-1, \qquad 2T_0(m)+m+2<m^{r-d},$$
the construction takes $w\in\{0,1\}^m$ to two simple uncolored
graphs of common order $O_{r,M}(m^6)$, such that $M$ accepts $w$
iff the two graphs are inequivalent in the $(r+1)$-pair bijective
game. Equivalently, they are inequivalent for joint-update
$r$-dimensional Weisfeiler-Leman equivalence precisely when $M$
accepts $w$.
The consistency description used has $O_{r,M}(1)$ types and edge
schemas, dimensions at most two, and $O_{r,M}(1)$ one-coordinate
tables with $O(m)$ entries each. These tables can be constructed
from $w$ in $O_{r,M}(m^3)$ time without running $M$ on $w$. For
every sufficiently large $m$ satisfying the two inequalities
above, the two graphs can be padded to any common order
$n\ge m^{20}$, and their adjacency matrices constructed in
$O_{r,M}(n^4)$ multitape time.
Proof. Let $\Sigma$ be the fixed alphabet of ordinary tape symbols
together with tape symbols carrying a head state of $M$. There is a
fixed local update map $F:\Sigma^3\to\Sigma$ such that, for every
valid machine configuration, $F$ applied to the triple of symbols
at positions $j-1$, $j$, $j+1$ gives the next symbol at $j$.
Indeed, the next symbol at $j$ and the head information carried
there are determined by whether the old head is at $j$ or at one
of its immediate neighbors, together with the scanned symbol and
the state recorded there. A triple containing no head leaves its
center symbol unchanged. Assigning arbitrary values on triples
that never occur in a valid configuration with one head extends
$F$ to all of $\Sigma^3$ while giving the exact local update on
every valid configuration, including frozen halting
configurations.
Use $d$ base-$m$ digits for time and $q=r-d$ base-$m$ digits for
position; write $H=m^d$ and $L=m^q$, and regard positions modulo
$L$. Time ranges from $0$ to $H-1$ and is not cyclic. The total of
$r$ digits is the address of every gate type.
Spatial ring. Verify that the ring computation reproduces the
intended line computation. For a prehalting transition at time
$\tau<T_0(m)$, let $h$ be the head position. Then
$|h|\le\tau\le T_0(m)-1$. Only the centers $h-1$, $h$, $h+1$ can
change, and the triples determining their next letters lie in
$[h-2,h+2]\subseteq[-T_0(m)-1,T_0(m)+1]$. Together with the
initial input, these positions lie in the interval
$I=[-T_0(m)-1,m+T_0(m)]\cap\mathbb{Z}$. This interval has
$2T_0(m)+m+2$ elements, fewer than $L$ by the second inequality.
Reduction modulo $L$ is therefore injective on $I$. At every step
before halting, the head reads and writes exactly the
corresponding line cell, and the only changes occur at the old and
new head locations. Induction on the step proves agreement of the
ring computation and the line computation through halting. Cells
away from the head remain unchanged, so no additional head or
change can arise elsewhere on the ring. The frozen state preserves
agreement through time $H-1$.
Gates and connections. For each $f\in\Sigma$ introduce a scalar
gate type $S_f$. At time zero seed exactly the actual initial
letter at each position. For every triple $(a,b,h)\in\Sigma^3$
introduce two AND types $A_{a,b,h}$ and $B_{a,b,h}$. At address
$(\tau,j)$ with $0\le\tau\le H-1$ and $0\le j\le L-1$, the
connections are
$$S_a(\tau-1,j-1)\to \text{port 1 of } A_{a,b,h}(\tau,j),$$
$$S_b(\tau-1,j) \to \text{port 2 of } A_{a,b,h}(\tau,j),$$
$$A_{a,b,h}(\tau,j) \to \text{port 1 of } B_{a,b,h}(\tau,j),$$
$$S_h(\tau-1,j+1) \to \text{port 2 of } B_{a,b,h}(\tau,j),$$
$$B_{a,b,h}(\tau,j) \to S_{F(a,b,h)}(\tau,j).$$
Every connection whose source time is $\tau-1$ is present only
for $\tau\ne0$. The two same-time connections are present at all
addresses. All position arithmetic in these displays is modulo
$L$.
Acyclicity. Give $A$ gates at time $\tau$ rank $3\tau$, $B$ gates
rank $3\tau+1$, and scalar gates rank $3\tau+2$. The same-time
connections strictly increase rank, and every temporal connection
comes from rank $3\tau-1$ at time $\tau-1$ to rank $3\tau$ or
$3\tau+1$. At time zero, every $A$ gate is false, since neither
port has a temporal input. Every $B$ gate is false as well, since
its first port is false. Only the chosen letter seed is true at
each position at time zero.
Correctness. Suppose inductively that the true scalar gates at time
$\tau-1$ specify exactly one letter at each cell, namely the
actual letter at that time. At $(\tau,j)$, the first AND for a
triple is true precisely when its first two letters are the
actual left and center letters. The second AND is true precisely
when the third letter is also the actual right letter. Exactly one
triple then has a true $B$ gate, and its output makes
$S_{F(a,b,h)}(\tau,j)$ true. Induction proves that the scalar gates
record the actual ring computation at all times up to $H-1$.
Tests. Test every scalar instance $S_f(H-1,j)$ whose $f$ carries
an accepting halted state. These tests are terminal: scalar gates
only have connections to the next time, and no time follows $H-1$.
By the first inequality and the frozen-state convention, some test
is true iff $M$ accepts $w$ within $T_0(m)$ steps.
Description as product schemas. The same-time connections use the
identity. In source coordinates, the three temporal kinds of
connection have address maps
$$(t,j)\mapsto(t+1,j+1),\qquad
(t,j)\mapsto(t+1,j),\qquad
(t,j)\mapsto(t+1,j-1),$$
respectively. In all three, $t=H-1$ is excluded.
Product decomposition. Number the digits in each group from least
to most significant. For nonmaximal time, let $a\in\{1,\ldots,d\}$
be the first digit not equal to $m-1$. Its case has domain
$$\{m-1\}^{a-1}\times\{0,\ldots,m-2\}\times[m]^{d-a}.$$
Applying the permutation $x\mapsto x+1\pmod m$ to the first $a$
digits and the identity to the others gives addition of one in
base $m$: lower digits become zero, the $a$-th digit increases
without overflow, and higher digits remain unchanged. The $d$ cases
partition all nonmaximal times, so they do not introduce time
wraparound. For cyclic position increment, use the analogous $q$
cases together with the additional all-maximal case, on which every
digit is incremented modulo $m$. For cyclic decrement, use the
first nonzero digit: lower digits are zero, that digit is in
$\{1,\ldots,m-1\}$, and later digits are arbitrary. Decrement the
digits through that first nonzero digit modulo $m$, leaving higher
digits unchanged. Add the all-zero wrap case, on which every
position digit is decremented modulo $m$. These are the standard
carry and borrow identities, expressed using products and
coordinate permutations. Because the time and position groups are
disjoint, combining one time case with one position case still
gives a product domain. Each shifted map in the temporal reductions
therefore uses at most $d(q+1)$ schemas, and the unshifted one uses
$d$ schemas. Every coordinate map is a restriction of a permutation
of $[m]$.
Seed and test product descriptions. All time digits are zero.
Positions $j<m$ have all but their least significant position digit
zero. For each possible initial letter, its occurrences among
these positions are a subset of that one remaining digit; the
digit zero is assigned the letter carrying the initial head state.
These subsets are determined by scanning $w$. The blank positions
$j\ge m$ are the union of the $q-1$ products obtained by requiring
a specified higher position digit to be nonzero and leaving the
other position digits arbitrary. Overlaps merely repeat the same
blank seed. Finally, a test domain sets every time digit to $m-1$
and leaves all position digits unrestricted.
Short consistency instance. There are $|\Sigma|$ scalar types and
$2|\Sigma|^3$ AND types. The number of product schemas just
described is bounded in terms of $r$ and $\Sigma$, independently of
$m$. The circuit simulation proposition therefore produces a short
consistency instance with bounded numbers of types and schemas and
dimensions at most two. Its one-coordinate tables contain only a
bounded number of subsets and permutations of $[m]$, so have
$O_{r,M}(m)$ entries. They can be produced by scanning $w$,
enumerating the labels, and applying the identity or cyclic
increment/decrement maps. Even repeated input scans and elementary
binary arithmetic give $O_{r,M}(m^3)$ time. This computation does
not simulate $M$ on $w$.
Combining with compression. By the circuit simulation proposition,
the resulting instance has an arc-consistency witness exactly when
no test is true, hence exactly when $M$ does not accept $w$. The
compression theorem, with $K=r+1$ pairs, converts the existence of
the sets $Q$ into the equivalence of the two resulting simple
uncolored graphs. This gives the asserted acceptance polarity and
the stated Weisfeiler-Leman interpretation.
Sizes and effective bounds. The unpadded order and the adjacency
matrix construction time are controlled by the following lemma.
Lemma (constructing padded graphs). Fix $r\ge 3$ and a short
consistency template with bounded numbers of types and schemas and
bounded vector dimensions. Suppose its one-coordinate domains and
maps are supplied by a bounded number of tables, each with $O(m)$
entries in $[m]$. The two uncolored graphs of the compression
theorem have a common vertex count
$$N=O(m^6+1),$$
where the constant depends only on the fixed template and $r$.
They may be padded to any common order $n\ge N$ without changing
the equivalence conclusion of that theorem.
For $n\ge\max\{N,m^{20}\}$, their adjacency matrices can be
constructed from the tables in $O(n^4)$ multitape Turing-machine
time. The exponent is absolute; the multiplicative constant may
depend on the template and $r$. If the tables can themselves be
constructed from a word of length $m$ in $O(m^3)$ time, this
preprocessing is included in the same bound.
Proof of the construction lemma. The order bound and padding
assertion are those of the compression theorem. Write $N_0$ for the
number of valuation vertices before adding marks, the hub, and
padding; the compression construction gives $N_0=O(m^2)$.
Vertex descriptors. A valuation descriptor consists of its block
identifiers, its at most two coordinate labels, and its bounded list
of readout values. A mark descriptor records its owner's identifier
and its local mark number. The remaining vertex kinds are the hub
and numbered padding vertices. Every descriptor has $O(\log(n+1))$
bits, with a constant depending only on the fixed template and $r$.
All names of shared readouts are enumerated together with the block
they belong to.
Vertex enumeration. The coordinate tables can be scanned rather than
randomly accessed. Enumerating $O(m^2)$ blocks, looking up a bounded
number of coordinate matches for each, and listing their valuations
uses $O(m^3 (\log(m+1))^2)$ time. Count $N_0$ in a first pass, then
enumerate the valuation vertices and their mark lists using binary
counters; finally append the padding list. This costs
$O(n(\log(n+1))^2)$ additional time. All arithmetic in this step concerns a
bounded number of integers of $O(\log(n+1))$ bits, and can for
example use the elementary quadratic digit algorithms. By
$n\ge m^{20}$ the whole preparation costs $O(n^2)$.
Adjacency matrix. Once the vertex descriptors are stored, scan all
$O(n^2)$ pairs and compare the two descriptors of each pair in
$O(n)$ time. Equality, adjacency between shared readout names, and
absence of other adjacency are decided within this scan. Fill the
adjacency matrix (and, in the colored variant, the color column) as
read. The total cost is $O(n^4)$. The preprocessing of the input
tables to the coordinate dictionaries was included in the same
bound.
Diagonalization. The next stage produces a binary language that is
hard for every one-tape decider at every sufficiently large input
length. Weisfeiler-Leman itself does not enter this stage; only the
distance between a fixed upper bound and every candidate decider
does.
Machines. Deterministic machines with doubly infinite tapes, finite
state sets, and finite tape alphabets are used. Start, accept, and
reject states are pairwise distinct, and the blank symbol and the
two input symbols are pairwise distinct. The input is a binary word
written at positions $0,\ldots,m-1$ of the first tape, all other
cells are blank, and every head starts at position $0$. A
transition moves each head by $-1$, $0$, or $1$. Acceptance and
rejection are designated halting states. The number of tapes and
the alphabet are fixed independently of the input length.
Lemma (quadratic simulation). For every fixed deterministic
multitape machine $A$ there is a fixed deterministic one-tape
machine $\widehat A$ with the same decisions, such that if $A$
halts after $T$ steps on an input of length $m$, then $\widehat A$
halts within $O_A((m+T+1)^2)$ steps on that input.
Proof. Suppose $A$ has $a$ tapes. One cell of the simulating tape
records the $a$ symbols at the corresponding position of the
simulated tapes, together with a head marker on each track whose
head is at that position. The product alphabet is finite because
$A$ is fixed. Additional marker bits delimit the represented
interval and distinguish old head markers from newly placed ones.
Initialization takes $O_A(m+1)$ steps.
After $j$ simulated transitions, all nonblank cells and all head
positions lie in an interval of length $O(m+j+1)$. To perform the
next transition, sweep this interval to read the $a$ marked
symbols. Their tuple and the simulated state fit in the finite
control. A further sweep performs the indicated writes and places
the new head markers one cell to the left, at the current cell, or
one cell to the right. Old and new marker bits prevent a marker
from being processed twice. A further sweep removes the old markers
and promotes the new ones. Moving to a neighboring cell to place a
marker costs only a bounded number of additional moves. Extend the
represented interval by a blank cell at either end when necessary.
A fixed number of sweeps, each of $O_A(m+j+1)$ steps, implements
one transition. Summing over $j<T$, including initialization and
the final decision, gives
$$O_A((T+1)(m+T+1)) = O_A((m+T+1)^2).$$
The construction neither needs $T$ in advance nor assumes any bound
on it.
Encoding of one-tape machines. For a nonnegative integer $u$, put
$\operatorname{un}(u)=1^u 0$. Number the states $0,\ldots,q-1$ and
the tape symbols $0,\ldots,g-1$, where $q,g\ge 3$. States $0,1,2$
are respectively start, accept, reject. Tape symbol $0$ is blank,
and symbols $1,2$ encode the input bits $0,1$. A description begins
with $\operatorname{un}(q)\operatorname{un}(g)$. It then lists, in
lexicographic order of (state, scanned symbol), all $qg$ transition
entries. Each entry gives unary codes for the new state, the
written symbol, and a direction code in $\{0,1,2\}$ denoting left,
stationary, and right. Entries for the halting states are ignored
by the operational semantics. A description is valid only if it
has exactly these entries, all indices are in range, and no
trailing bits follow. Every fixed one-tape machine in this model
has such a description after renaming states and symbols; renaming
does not change running time.
Designation. If $b$ is a valid description of length $\ell$, its
designation is
$$\pi(b)=1^\ell 0 b.$$
A word has at most one designation as prefix. The initial unary
field specifies exactly how many following bits are the
description. Remaining bits are unrestricted. A machine designated
by a prefix is always simulated on the entire input word, including
that prefix.
./cook-1971.pdf
Cook 1971 introduced the local triple update of one-tape machine
computations, in which the symbol at a position in the next
configuration is determined by the triple of symbols at that
position and its two neighbors. The construction below uses exactly
this triple update. Hennie and Stearns 1966 first used the padding
trick together with designation of the decider to diagonalize
against every fixed machine simultaneously.
Theorem (diagonal language). For every integer $s\ge 1$ there is a
binary language $H_s$ with the following properties.
(i) There is a fixed deterministic one-tape decider $M_s$ and a
constant $C_s$ such that on every input of length $m\ge 0$ its
running time is at most
$$C_s(m+m^s+2)^{20}.$$
(ii) If $D$ is any correct deterministic one-tape decider for
$H_s$, then for every sufficiently large integer $m$ the worst-case
running time of $D$ on inputs of length $m$ is strictly greater
than $m^s$.
(iii) After their decisions have been recorded, the accepting and
rejecting configurations of $M_s$ may be kept fixed forever. This
gives a stationary extension of its computation suitable for the
local update representation.
Proof. On an input $w$ of length $m$, set $t=m^s$. If $w$ has no
valid designation as a prefix, put $w\notin H_s$. Otherwise let
$D_b$ be the designated machine and define
$$w\in H_s
\quad\Longleftrightarrow\quad
D_b\text{ does not accept the full word }w
\text{ within }t\text{ steps}.$$
Acceptance within the cutoff includes entering the accepting state
on the last permitted transition. A rejecting halt never counts.
Lower bound. Let $D$ be a correct one-tape decider for $H_s$,
choose a description $b_D$ of $D$, and write $L_D=|\pi(b_D)|$. For
every $m\ge L_D$ there is an input of length $m$ beginning with
$\pi(b_D)$. Every word $w=\pi(b_D)z$ of that length forces $D$ to
run for more than $m^s$ steps. If $D$ accepted $w$ within the
cutoff, the definition would exclude $w$ from $H_s$. If $D$
rejected $w$ within the cutoff, then it would not accept within the
cutoff, so the definition would include $w$ in $H_s$. Both
contradict correctness. Since $D$ is a decider, its only remaining
possibility is to halt after the cutoff.
Fixed universal procedure. Fix $s$ and write $B=m+t+2$. The
procedure has a fixed finite number of work tapes and a fixed
alphabet, neither depending on the described machine. A scan
obtains $m$ in unary and extracts the proposed designation. Parsing
its explicit table and checking index ranges requires only
polynomially many scans of strings of length $O(m+1)$. Malformed
inputs are rejected. When $m=0$ the input is malformed and this
also matches the bound.
The cutoff $t$ is written in unary without any arithmetic oracle.
For $m\ge 1$ use $s$ nested counters, each ranging over $m$ values,
and append one mark for each counter tuple. The number of counters
is fixed, and a counter update or reset takes $O_s(m+1)$ time.
This produces exactly $m^s$ marks in $O_s((m+1)(t+1))$ steps.
For a valid description, all simulated state and symbol names have
unary length at most $m+1$. Preallocate records for the tape
positions
$$-t-1,\ldots,m+t+1.$$
There are $m+2t+3=O(B)$ records. A record contains a symbol field
padded to a fixed width $O(m+1)$ and a head marker; the current
simulated state is stored separately in unary. Delimiters and
padding are symbols of the fixed simulator alphabet. The entire
configuration list has length $O(B^2)$. Initialize positions
$0,\ldots,m-1$ with the bits of $w$, put blanks elsewhere, and mark
position $0$. A head starting at $0$ cannot leave $[-t,t]$ in $t$
steps, so all simulated accesses fall inside the preallocated list.
A simulated transition. Scan the configuration list to find its
marked record and copy the scanned symbol. Read the explicit
transition table with unary state and symbol counters until the
required entry is found, and copy its new state, symbol, and
direction. Rescan the configuration list to replace the symbol and
move the marker to the adjacent record, or leave it stationary. The
fixed field widths ensure that no insertion into the list is
necessary. For a left move the simulator may back up one record;
for a right move it may advance one record. Temporary marker flags
distinguish this update from the next simulated transition. Finally
consume one budget mark and test whether the new state is accepting
or rejecting.
Bounds. All operations above use scans, copies, and comparisons of
explicitly written strings. A deliberately inefficient
implementation still costs $O_s(B^5)$ per simulated transition: the
configuration list has length $O(B^2)$, and even a full-list scan
for each symbol copied costs $O(B^4)$; table lookup, comparisons of
unary fields, resets, and budget maintenance fit within one further
factor $B$. Validation, budget construction, and initialization fit
within the same $O_s(B^5)$ bound. Stop with answer no as soon as
acceptance is detected. Stop with answer yes on a rejecting halt or
when all $t$ transitions have been simulated without acceptance.
There are at most $t\le B$ simulated transitions, so this fixed
multitape procedure decides $H_s$ within $O_s(B^6)$ steps.
Apply the quadratic simulation lemma. Its one-tape implementation
has time
$$O_s((m+B^6+1)^2)=O_s(B^{12})\le O_s(B^{20}).$$
Increasing the constant covers every input length and yields the
first assertion. Write $M_s$ for this fixed one-tape decider.
Stationary halts. For subsequent recording of configurations,
extend the transition rule of $M_s$ at either halting state by
writing the scanned symbol unchanged, keeping the head stationary,
and keeping the same state. Reaching the state still records the
decision at the original halting time, but all later
configurations are identical. The machine has a fixed finite
alphabet and one head, so its configurations can be represented by
tape symbols with an optional head-state marker. The symbol at a
position in the next configuration is determined by the three
symbols at that position and its two neighbors. On valid
configurations these possibilities determine a unique update;
extending the update arbitrarily to invalid triples gives the
required finite local rule, and the extended halting
configurations are fixed by it.
Remark (quantifiers). The lower-bound threshold in the diagonal
theorem may depend on the decider $D$. The language and its
upper-bound machine depend only on the fixed integer $s$.
The previous reductions deal with individual word lengths. The
conclusion of the main theorem concerns fixed $k$ at every
sufficiently large $n$. Padding alone is not enough: a reduction
that selected one order for each word length could miss all fast
input orders of a candidate algorithm. The construction below
therefore tries every order in a fixed window at once.
Fix a sufficiently large parameter $k$. Put $K=k+1$ and $r=k$ for
the joint replacement convention, or $K=k$ and $r=k-1$ for the
separate-multiset convention; then $K=r+1$ in either case.
Throughout put
$$s = \lfloor r/1000 \rfloor, \quad
p = \lfloor s/1000 \rfloor, \quad
c_0 = 10^{-9}.$$
All machines, alphabets, and constants depending on these
parameters are fixed as the input length grows. No uniformity in
$k$ is required of a proposed equivalence algorithm.
For an integer $m\ge 2$ put
$$I_m = \{n\in\mathbb{N} : m^{20}\le n < (m+1)^{20}\}.$$
These intervals partition all integers at least $2^{20}$.
Lemma (instances at every prescribed order). For every sufficiently
large fixed $r$, there is an integer $m_0(r)$ with the following
property. Given a word $w$ of length $m\ge m_0(r)$ and any
$n\in I_m$, one can construct two simple uncolored $n$-vertex
graphs $G_{w,n}$ and $G'_{w,n}$ such that
$$w\in H_s \quad\Longleftrightarrow\quad
G_{w,n}\not\equiv_{k\text{-}\WL}G'_{w,n}.$$
Both graphs are connected and have diameter at most two. Their
explicit adjacency matrices can be constructed in $O_r(n^4)$
multitape time.
Proof. For $s\ge 1$, the diagonal theorem bounds the running time of
$M_s$ on length-$m$ inputs by $C'_s m^{20s}$ for a constant $C'_s$.
Put $d=\lfloor r/3\rfloor$. For sufficiently large $r$,
$$20 s \le r/50 < d, \qquad 20 s < r-d.$$
Consequently, for all sufficiently large $m$, uniformly over words
of length $m$, a running-time bound $T_0(m)$ for $M_s$ satisfies
$$T_0(m) < m^d - 1, \qquad 2T_0(m) + m + 2 < m^{r-d}.$$
The Turing-machine circuit theorem, the graph reduction of the
compression theorem, and the game lemma therefore give graph pairs
with the stated polarity. Their common unpadded order is at most
$C_r m^6$, where the constant absorbs the dependence on $M_s$.
For all sufficiently large $m$ this order is at most $m^{20}$. The
padding assertion in the compression theorem reaches each prescribed
order $n\in I_m$ while preserving equivalence and the diameter
bound. The construction lemma gives the asserted explicit
construction time. Choosing $m_0(r)$ to satisfy these finitely many
eventual conditions completes the proof.
The two machine models require a polynomial simulation bound whose
exponent is independent of $k$ and of the candidate algorithm. In
the RAM case, use the sequential model fixed at the start: a fixed
finite program, a bounded number of memory accesses per instruction,
$O(\log(n+2))$-bit addresses and words, and fixed instructions
computable in time polynomial in the word length. Constants and the
degree of this last polynomial may depend on the fixed program.
The input consists of explicit graph matrices, with an ordinary
finite encoding of their order. For a fixed RAM program $A$, the
order encoding and the two row-major adjacency bit strings are
stored directly in a fixed packed or unpacked layout of
$O_A(n^2)$ input words. Every other memory cell initially has a
fixed default value. The layout is uniform in $n$ and in the
input bits, and can be written from the matrices in $O_A(n^3)$
multitape time.
Lemma (cutoff procedure). There is an absolute constant $D$ with
the following property. Fix a sufficiently large $r$, with $s, p$
as above, and a correct deterministic equivalence decider $A$ in
either stated model. There is a correct one-tape decider $B$ for
$H_s$ that, on every sufficiently long word $w$ of length $m$, first
tries the pairs of the instances lemma for all $n\in I_m$,
allowing at most $m^p$ steps of $A$ on each pair. It returns the
first completed answer with reversed polarity, or falls back to
$M_s$ if no trial completes. The one-tape time used before fallback,
or before returning a completed answer, is at most
$$O_{A,r}(m^{D+50p}).$$
Proof. The procedure handles lengths below $m_0(r)$ directly with
$M_s$. At larger lengths it generates and tests the padded instances
one at a time, restarting each simulation of $A$ from its initial
configuration. Since $A$ is correct, every completed answer has the
polarity specified by the instances lemma. If all simulations reach
their cutoffs, $M_s$ supplies the answer. Thus the procedure always
decides $H_s$ correctly. Its finite program may hardwire $r$, $p$,
and $m_0(r)$.
Let $t=m^p$ be the cutoff for one trial. Constructing the input
pair costs $O_r(n^4)$ time. A multitape candidate is simulated
directly on work tapes with a cutoff counter. For completeness the
following more generous bound also covers the RAM case:
$$O_{A,r}((n^3 + t + 2)^6)$$
multitape steps suffice for one cutoff simulation, including
initialization and counter maintenance.
To see this for the RAM, store a list of initialized or subsequently
touched memory cells. If $S$ denotes their maximum number during the
trial, then $S=O_A(n^2+t+1)$, since the input is explicit and each
instruction accesses only boundedly many cells. Each address and
stored value has $O_A(\log(n+2))$ bits. An unlisted address
represents an untouched cell in its default initial state. Full
scans of the list suffice for reads and writes; the whole address
space is never allocated. If $t$ exceeds the number of available
addresses, repeated accesses do not enlarge the list, and the
estimate remains an upper bound.
Every fixed instruction can be evaluated by a fixed bit computation
in $(\log(n+2))^{O_A(1)}$ time. Using full scans and even
unnecessarily slow copies of the stored list, one simulated step
costs at most
$$O_A(S^2 (\log(n+2))^{q_A})$$
for some fixed exponent $q_A$. For every fixed $q_A$,
$(\log(n+2))^{q_A}\le n$ for all sufficiently large $n$. The total
for $t$ simulated steps is therefore at most
$$O_A(t S^2 n) = O_A(t(n^2+t+1)^2 n) = O_A((n^3+t+2)^4).$$
Initializing the explicit input list costs at most $O_A(n^3)$. The
cutoff counter has $O_p(\log(m+2))=O_p(\log(n+2))$ bits and adds at
most $O_p(t\log(n+2))$ time. These costs all fit in the displayed
sixth-power bound. An arbitrarily large but fixed word-operation
exponent affects only the starting size and the multiplicative
constant, not the absolute exponent in the final one-tape bound.
There are $O(m^{20})$ trials, and every $n\in I_m$ is $O(m^{20})$.
For $p\ge 1$, the total multitape cost before fallback is at most
$$O_{A,r}\left(m^{20}\left[m^{80}+(m^{60}+m^p+2)^6\right]\right)
= O_{A,r}(m^{380+6p}).$$
The counters enumerating the interval and the bookkeeping for trials
fit in this bound. Applying the quadratic simulation lemma gives
$O_{A,r}(m^{760+12p})$ time for this stage. The simulation is by
online marked-track sweeps, so its quadratic bound applies to the
prefix before fallback as well as to a complete computation.
Increasing a fixed absolute constant $D$ if necessary gives the
claimed bound. The constants in the $O_{A,r}$ notation may depend
on $A$ and $r$, but $D$ and the coefficient $50$ do not.
The parameter choices satisfy, for all sufficiently large $k$,
$$D + 50p < s, \qquad 20 c_0 k < p.$$
Indeed $p\le s/1000$, whereas $p\ge r/10^6 - 1.001$, and $r$ is
either $k$ or $k-1$. The first inequality follows as $s$ tends to
infinity; the second follows from $20c_0=2\cdot 10^{-8}<10^{-6}$.
Fix such a $k$. The promised version is stronger: assume that $A$
is required to halt and decide correctly only on pairs of simple
connected uncolored graphs of diameter at most two, and let
$T_A(n)$ be its maximum running time over pairs in this class with
$n$ vertices in each graph. Every trial of the cutoff lemma belongs
to this class by the instances lemma. That construction and its
correctness proof therefore still give a fixed one-tape decider $B$
for $H_s$, without any assumption on the behavior of $A$ outside
the promised class.
The second strict gap above implies that, for all sufficiently
large $m$ and every $n\in I_m$,
$$n^{c_0 k} \le (m+1)^{20 c_0 k}
= m^{20 c_0 k}(1+1/m)^{20 c_0 k} \le m^p.$$
k is fixed, and the positive exponent gap $p-20c_0 k$
absorbs the bounded factor $(1+1/m)^{20c_0 k}$. This also accounts
for the upper endpoint of $I_m$.
Suppose some $n\in I_m$ satisfies $T_A(n)<n^{c_0 k}$. For every
word $w$ of length $m$, its padded reduction instance at this same
$n$ is an input on which $A$ completes within the cutoff $m^p$.
Consequently $B$ returns before fallback on every word of length
$m$, whether on this trial or on an earlier one. Its worst-case
time at that length is therefore
$$O_{A,r}(m^{D+50p}) < m^s$$
for all sufficiently large $m$, by the first strict gap.
The diagonal theorem applied to $B$ requires worst-case time greater
than $m^s$ at every sufficiently large length. Choose a threshold
$M=M(A,k)$ beyond all starting lengths used above, including the
diagonal lower-bound threshold for $B$ and the length needed to
absorb the constant in the cutoff cost. Then no $m\ge M$ admits any
$n\in I_m$ satisfying $T_A(n)<n^{c_0 k}$.
The intervals $I_m$ partition all integers at least $M^{20}$.
Therefore
$$T_A(n) \ge n^{c_0 k} \quad\text{for every integer }n\ge M^{20}.$$
Taking $c=c_0$ proves the claimed eventual lower bound. No
monotonicity of $T_A$ is assumed: trying the complete interval is
what excludes isolated fast input sizes. The threshold may depend
on the fixed algorithm and parameter; the exponent constant is
absolute. The unrestricted worst-case time is at least the
restricted maximum just bounded, so the same lower bound also holds
without any promise on the input graphs.
Remark (small parameters). For unrestricted graph inputs represented
by explicit adjacency matrices, the finitely many smaller positive
values of $k$ enter the conclusion once $c$ is decreased. In that case
$k=1$ means ordinary color refinement. Every such test
distinguishes the pair (empty graph, empty graph) from
(empty graph, one-edge graph). On the empty input a deterministic
algorithm must inspect at least one matrix entry for every possible
hidden undirected edge of the second graph; otherwise adding that
edge leaves the execution unchanged. This gives $\Omega(n^2)$
inspected bits, or $\Omega_A(n^2/\log(n+2))$ steps with
logarithmic-word access, and in particular an eventual lower bound
of $n$. Choosing $c$ smaller than the reciprocal of the finite
parameter threshold handles those remaining values. This observation
depends on the matrix representation and on allowing unrestricted
graph inputs. It does not assert the promised-class extension for
small $k$ and is separate from the large-$k$ reduction.
The argument concerns uniform deterministic machines in the stated
sequential models. It makes no assertion about randomized
algorithms, advice depending on the input length, or unit-cost
operations on unbounded words. Its lower bound is on arbitrary
equivalence deciders, with no requirement that they execute the
Weisfeiler-Leman refinement procedure.