==== TABLE OF CONTENTS ====
Unconditional-time-lower-bounds-for-Weisfeiler-Leman-equivalence//main.tex
Unconditional-time-lower-bounds-for-Weisfeiler-Leman-equivalence//references.tex
Unconditional-time-lower-bounds-for-Weisfeiler-Leman-equivalence//sections/01-game.tex
Unconditional-time-lower-bounds-for-Weisfeiler-Leman-equivalence//sections/02-compression.tex
Unconditional-time-lower-bounds-for-Weisfeiler-Leman-equivalence//sections/03-circuits.tex
Unconditional-time-lower-bounds-for-Weisfeiler-Leman-equivalence//sections/04-diagonal.tex
Unconditional-time-lower-bounds-for-Weisfeiler-Leman-equivalence//sections/05-transfer.tex
===========================

==== BEGIN Unconditional-time-lower-bounds-for-Weisfeiler-Leman-equivalence//main.tex ====
\documentclass[11pt]{article}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage[margin=1in]{geometry}
\usepackage{enumitem,microtype,booktabs,graphicx}
\usepackage{xcolor,tikz}
\usetikzlibrary{arrows.meta,positioning,calc,decorations.pathreplacing}
\usepackage[hyphens]{url}
\usepackage[colorlinks=true,linkcolor=black,citecolor=blue,urlcolor=blue]{hyperref}
\usepackage[nameinlink,capitalise,noabbrev]{cleveref}
\hypersetup{pdftitle={Unconditional time lower bounds for Weisfeiler-Leman equivalence},pdfauthor={OpenAI}}

\newcommand{\F}{\mathbb{F}}
\newcommand{\N}{\mathbb{N}}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\WL}{\mathrm{WL}}
\newcommand{\AC}{\mathrm{AC}}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\numberwithin{equation}{section}
\setlist[enumerate]{itemsep=3pt,topsep=5pt}
\setlist[itemize]{itemsep=3pt,topsep=5pt}
\allowdisplaybreaks[1]

\title{Unconditional time lower bounds for\\
Weisfeiler--Leman equivalence}
\author{OpenAI}
\date{September 25, 2026}

\begin{document}
\maketitle

\begin{abstract}
For every sufficiently large fixed $k$, deciding whether two
$n$-vertex graphs are $k$-Weisfeiler--Leman equivalent requires
$n^{\Omega(k)}$ deterministic sequential time in the worst case.
The bound holds at every sufficiently large graph order, even for
simple connected uncolored graphs of diameter at most two, without a
complexity assumption. Inputs are explicit adjacency matrices; the models
are multitape Turing machines and sequential logarithmic-word RAMs with
fixed polynomial-bit-time instructions. Both joint and separate replacement
conventions are covered.
\end{abstract}

\section{Introduction}\label{sec:introduction}

The refinement method originates in Weisfeiler and Leman's work on graph
canonization \cite{WL1968}. Its higher-dimensional form assigns colors to tuples of vertices
by repeatedly recording their local extension patterns. For each fixed
dimension $k$, stabilization gives a polynomial-time test of
$k$-Weisfeiler--Leman equivalence. The direct algorithms have running
time $n^{O(k)}$: there are $n^k$ tuples, at most polynomially many
refinement rounds in their number, and each round can be implemented
in polynomial time in the tuple table. The question considered here
is whether a growing exponent is necessary for \emph{any} sequential
algorithm deciding the equivalence relation, rather than just for an
implementation of refinement.

For $k\ge2$, initial tuple colors record coordinate equalities and
adjacencies. Each refinement step retains the old color and counts
replacement colors. The \emph{joint} convention counts a multiset of
$k$-component replacement-color vectors, one vector for each new vertex
used in every coordinate; the \emph{separate} convention counts a replacement multiset
for each coordinate independently. With common color names on the two
graphs, equivalence means equality of their stable $k$-tuple color
histograms. Section~\ref{game:section} gives the full formulas and their
game characterizations.

We give an unconditional lower bound for this decision problem. Input graphs are represented
by explicit adjacency matrices. A decider is uniform
in the input size; it may depend arbitrarily on the fixed dimension
$k$. For a decider $A$, let $T_A(n)$ be its worst-case running time on
pairs of graphs having $n$ vertices each.

\begin{theorem}\label{thm:main}
There are absolute constants $c>0$ and $k_0$ with the following
property. For every fixed integer $k\ge k_0$ and every correct
deterministic decider $A$ for $k$-Weisfeiler--Leman equivalence, there
is an integer $n_0=n_0(A,k)$ such that
\[
                     T_A(n)\ge n^{ck}
             \qquad\text{for every integer }n\ge n_0.
\]
This holds for multitape Turing machines and for sequential
random-access machines with $O(\log(n+2))$-bit addresses and words,
boundedly many memory accesses per instruction, and fixed instructions
computable in time polynomial in the word length.
The same bound holds if $A$ is required to decide correctly only on
pairs of simple connected uncolored graphs of diameter at most two,
with $T_A(n)$ maximized over that class. It applies both to the
joint replacement-multiset convention for $k$-dimensional refinement
and to the separate-multiset convention defined below.
\end{theorem}

Theorem~\ref{thm:main} is unconditional; in particular, it does not
assume the Exponential Time Hypothesis. It rules out a uniform
running-time bound $f(k)n^{g(k)}$ with $g(k)=o(k)$, for any
function $f$ independent of $n$: fix a sufficiently large $k$ for
which $g(k)