pith. sign in

arxiv: 2604.19212 · v1 · submitted 2026-04-21 · 💻 cs.LG · cs.LO

The Logical Expressiveness of Topological Neural Networks

Amirreza Akbari , Amauri H. Souza , Vikas Garg This is my paper

Pith reviewed 2026-05-10 02:45 UTC · model grok-4.3

classification 💻 cs.LG cs.LO
keywords topological neural networkslogical expressivenesscombinatorial complexesWeisfeiler-Leman testcounting logicpebble gamegraph representation learningisomorphism testing
0
0 comments X

The pith

Topological neural networks have exactly the expressive power of a higher-order counting logic with pairwise quantifiers and a matching topological pebble game.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper proves that message-passing schemes on combinatorial complexes, the basis for topological neural networks, are equivalent in power to the k-CCWL isomorphism test, to a new topological counting logic called TC_{k+2} that adds pairwise counting quantifiers, and to a topological variant of the (k+2)-pebble game. This equivalence matters because it gives a precise logical characterization of which functions TNNs can compute, showing exactly when they can distinguish structures that ordinary graph neural networks cannot. A reader would care because the result extends the well-known Weisfeiler-Leman hierarchy from graphs to richer relational objects, telling us the limits of what TNNs can learn without needing to run every possible architecture. The work unifies three different ways of measuring expressive power and thereby supplies the missing theoretical backbone for topological learning models.

Core claim

The central claim is that k-CCWL, the higher-order Weisfeiler-Leman test on combinatorial complexes, is exactly equivalent to TC_{k+2}, the topological counting logic that includes the new pairwise counting quantifier ∃^N(x_i, x_j) φ(x_i, x_j), and also equivalent to the topological (k+2)-pebble game. These equivalences fully characterize the binary classifiers that general topological neural networks can represent.

What carries the argument

The k-CCWL test on combinatorial complexes, which iteratively refines colorings of higher-order cells by aggregating information from neighboring relations of all orders.

If this is right

  • Any binary classifier invariant under TC_{k+2} equivalence can in principle be realized by some TNN.
  • TNNs can distinguish non-isomorphic structures that require counting pairs of elements, going beyond what 1-dimensional WL or standard GNNs achieve.
  • The logical and game characterizations give exact conditions under which a TNN will fail to separate two complexes.
  • Architectures that explicitly implement the pairwise counting quantifier achieve the full TC_{k+2} power.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Designers could build TNN layers that directly count pairs satisfying a property to reach the proven upper bound on expressiveness.
  • The same equivalences might extend to other higher-order domains such as hypergraphs or simplicial complexes once the combinatorial-complex framework is generalized.
  • Empirical tests could check whether current TNN implementations already saturate the k-CCWL limit on benchmark complexes or still fall short.

Load-bearing premise

That arbitrary message-passing rules in topological neural networks on combinatorial complexes can be made to realize every distinction the k-CCWL test can make, without extra restrictions on how higher-order relations are handled.

What would settle it

Finding two non-isomorphic combinatorial complexes that the topological (k+2)-pebble game can separate but no TNN message-passing scheme can, or the reverse, would disprove the claimed equivalence.

Figures

Figures reproduced from arXiv: 2604.19212 by Amauri H. Souza, Amirreza Akbari, Vikas Garg.

Figure 1
Figure 1. Figure 1: Example of one refinement round in the 2-CCWL on an ACC where all vertices share the same color, all edges share the same color, and there is a single 2-cell (the triangular face). The chosen tuple (c, e), consisting of a vertex c and an edge e, is first assigned its atomic type, which includes pairwise equality, adjacency relations, colors, and the rank sequence. During the update step, all substitutions … view at source ↗
Figure 2
Figure 2. Figure 2: Two non-isomorphic simplicial complexes. If all vertices and edges are given the same [PITH_FULL_IMAGE:figures/full_fig_p010_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Non-uniform ACCs from Example B.8. Blue edges denote [PITH_FULL_IMAGE:figures/full_fig_p023_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Left: correspondence between k-CCWL, TCk+2, and the TCk+2game. Right: the case k = 1 with guarded logic GTC3 and the GTC3 game. By Proposition 3.1, applied to uniform ACCs with the identical-vs-disjoint, exactly one of the fol￾lowing holds: χ (∞) k,A = χ (∞) k,B or χ (∞) k,A ∩ χ (∞) k,B = ∅. We show that these two cases are equivalent to agreement vs. disagreement on all sentences of TCk+2. Case 1: χ (∞) k… view at source ↗
Figure 5
Figure 5. Figure 5: Left: the ACC associated with the 6-cycle C6. Right: the ACC associated with the disjoint union C3 ⊔ C3. Both have six 0-cells, but only the right-hand side contains a 3-cycle (triangle). same multiset of colors. Dually, each 1-cell e has two 0-rank cells in its boundary and two 1-rank cells in its lower neighborhood, so all 1-cells also see the same multiset. Hence one refinement step already yields a sta… view at source ↗
read the original abstract

Graph neural networks (GNNs) are the standard for learning on graphs, yet they have limited expressive power, often expressed in terms of the Weisfeiler-Leman (WL) hierarchy or within the framework of first-order logic. In this context, topological neural networks (TNNs) have recently emerged as a promising alternative for graph representation learning. By incorporating higher-order relational structures into message-passing schemes, TNNs offer higher representational power than traditional GNNs. However, a fundamental question remains open: what is the logical expressiveness of TNNs? Answering this allows us to characterize precisely which binary classifiers TNNs can represent. In this paper, we address this question by analyzing isomorphism tests derived from the underlying mechanisms of general TNNs. We introduce and investigate the power of higher-order variants of WL-based tests for combinatorial complexes, called $k$-CCWL test. In addition, we introduce the topological counting logic (TC$_k$), an extension of standard counting logic featuring a novel pairwise counting quantifier $ \exists^{N}(x_i,x_j)\, \varphi(x_i,x_j), $ which explicitly quantifies pairs $(x_i, x_j)$ satisfying property $\varphi$. We rigorously prove the exact equivalence: $ \text{k-CCWL} \equiv \text{TC}_{k{+}2} \equiv \text{Topological }(k{+}2)\text{-pebble game}.$ These results establish a logical expressiveness theory for TNNs.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper claims that the logical expressiveness of topological neural networks (TNNs) on combinatorial complexes is characterized by a new k-CCWL isomorphism test, which is exactly equivalent to the topological counting logic TC_{k+2} (an extension of counting logic with a novel pairwise counting quantifier ∃^N(x_i, x_j) φ(x_i, x_j)) and the topological (k+2)-pebble game. These equivalences are derived from the message-passing mechanisms of general TNNs and are presented as rigorous proofs establishing a logical theory for TNNs beyond standard GNNs and the WL hierarchy.

Significance. If the central equivalences hold without gaps in the reductions, the work supplies a precise logical characterization of TNN power, connecting higher-order message passing on combinatorial complexes to pebble games and counting logics. This is a substantive contribution to the theory of expressive graph and higher-order neural networks, with potential to guide architecture design and distinguish TNNs from GNNs.

major comments (2)
  1. [Abstract and §3 (TNN mechanisms and k-CCWL definition)] The load-bearing step for transferring the k-CCWL ≡ TC_{k+2} equivalence to TNN expressiveness is the claim that general TNN message-passing schemes on arbitrary combinatorial complexes can implement the full k-CCWL test (abstract and the derivation of k-CCWL from TNN mechanisms). This requires that all higher-order incidence relations (faces, cofaces, etc.) can be aggregated without information loss or architectural restrictions; the manuscript does not provide a formal argument or counterexample analysis showing that every TNN variant satisfies this, which risks the equivalence holding only for a restricted subclass of TNNs.
  2. [§4 (equivalence proofs)] §4 (proof of k-CCWL ≡ TC_{k+2} ≡ topological (k+2)-pebble game): the reduction steps from the pairwise counting quantifier and the pebble game to the CCWL color refinement are asserted as rigorous but the provided sketch does not explicitly address how the quantifier ∃^N handles the combinatorial complex structure without introducing additional parameters or losing higher-order distinctions; a concrete example or lemma showing preservation of distinctions under the new quantifier is needed to confirm no circularity in the equivalence.
minor comments (2)
  1. [§2 (logic definitions)] Notation for the pairwise quantifier ∃^N(x_i, x_j) is introduced without an explicit comparison table to standard counting quantifiers, which would aid readability.
  2. [§3] The manuscript would benefit from an explicit statement of the precise class of TNN architectures (e.g., aggregation functions, update rules) to which the k-CCWL equivalence applies.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the detailed and constructive comments, which help clarify the scope and rigor of our logical characterization of TNNs. We address each major comment below, providing clarifications and committing to revisions that strengthen the manuscript without altering its core claims.

read point-by-point responses

  1. Referee: [Abstract and §3 (TNN mechanisms and k-CCWL definition)] The load-bearing step for transferring the k-CCWL ≡ TC_{k+2} equivalence to TNN expressiveness is the claim that general TNN message-passing schemes on arbitrary combinatorial complexes can implement the full k-CCWL test (abstract and the derivation of k-CCWL from TNN mechanisms). This requires that all higher-order incidence relations (faces, cofaces, etc.) can be aggregated without information loss or architectural restrictions; the manuscript does not provide a formal argument or counterexample analysis showing that every TNN variant satisfies this, which risks the equivalence holding only for a restricted subclass of TNNs.

    Authors: We agree that an explicit formal argument strengthens the transfer from TNN mechanisms to k-CCWL. In the revision, we will add a lemma in §3 that shows how the general TNN message-passing scheme—aggregating over all available incidence relations (faces, cofaces, and higher-order incidences) in a combinatorial complex—implements the full color-refinement steps of k-CCWL. The lemma demonstrates that aggregation functions can be instantiated to match WL-style updates without information loss for arbitrary TNN variants, while noting that architecture-specific restrictions (e.g., limited neighborhood definitions) would only yield a weaker test, which is already covered by the equivalence statements. A short counterexample analysis for overly restricted variants will also be included. revision: yes

  2. Referee: [§4 (equivalence proofs)] §4 (proof of k-CCWL ≡ TC_{k+2} ≡ topological (k+2)-pebble game): the reduction steps from the pairwise counting quantifier and the pebble game to the CCWL color refinement are asserted as rigorous but the provided sketch does not explicitly address how the quantifier ∃^N handles the combinatorial complex structure without introducing additional parameters or losing higher-order distinctions; a concrete example or lemma showing preservation of distinctions under the new quantifier is needed to confirm no circularity in the equivalence.

    Authors: We appreciate the request for additional explicitness in the proof. In the revised §4, we will insert a concrete example on a small combinatorial complex (e.g., a 2-simplex with an attached edge) that illustrates the action of the pairwise counting quantifier ∃^N(x_i, x_j) φ(x_i, x_j). The example shows how the quantifier directly encodes incidence relations without extra parameters and preserves all higher-order distinctions present in the complex. We will also add a supporting lemma proving that distinctions are preserved under the quantifier, thereby confirming the reductions are non-circular and that the equivalence holds for the full structure of combinatorial complexes. revision: yes

Circularity Check

0 steps flagged

No circularity: equivalences proven between independently introduced formal objects

full rationale

The paper derives k-CCWL from TNN message-passing mechanisms on combinatorial complexes, introduces the distinct TC_k logic with its pairwise counting quantifier, and proves k-CCWL ≡ TC_{k+2} ≡ topological (k+2)-pebble game via rigorous equivalences. These objects are defined separately before the proofs; no step reduces one to a fitted parameter, self-citation chain, or definitional tautology from the same paper. The load-bearing claim that general TNNs realize full k-CCWL is an explicit analysis of mechanisms rather than a construction that forces the result by input. No self-citations are load-bearing for the central equivalences, and the derivation remains self-contained against external logical and game-theoretic benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The claim rests on standard background from WL hierarchy and counting logic plus the new definitions introduced here; no free parameters or invented physical entities.

axioms (1)
  • standard math Background results from the Weisfeiler-Leman hierarchy and first-order counting logic
    The paper extends these established frameworks to combinatorial complexes and topological settings.
invented entities (1)
  • pairwise counting quantifier ∃^N(x_i, x_j) φ(x_i, x_j) no independent evidence
    purpose: To allow explicit quantification over pairs of elements satisfying a property in the logic
    New syntactic construct defined in the paper to capture higher-order topological relations.

pith-pipeline@v0.9.0 · 5577 in / 1198 out tokens · 38988 ms · 2026-05-10T02:45:51.784214+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

46 extracted references · 46 canonical work pages

  1. [1]

    Architectures of Topological Deep Learning: A Survey on Topological Neural Networks, August 2023

    URLhttps://proceedings.mlr.press/v235/papamarkou24a.html. Mathilde Papillon, Sophia Sanborn, Mustafa Hajij, and Nina Miolane. Architectures of topolog- ical deep learning: A survey of message-passing topological neural networks.arXiv preprint arXiv:2304.10031, 2024. Mathilde Papillon, Guillermo Bernardez, Claudio Battiloro, and Nina Miolane. Topotune: A f...

    work page arXiv 2024

  2. [2]

    Initialize the cell labeling: for each cellx∈ X, setχ (0) 1 (x) = (c(x),rk(x))

    work page

  3. [3]

    For each iterationt≥1, update the cell labels using: χ(t) 1 (x) = χ(t−1) 1 (x),M (t) Γ (x) , where M(t) Γ (x) = cB,(t)(x), cC,(t)(x), c↓,(t)(x), c↑,(t)(x) . The colors of the boundary cells are denoted byc B,(t)(x), the colors of the co-boundary cells are denoted byc C,(t)(x), the colors of the lower cells are denoted byc ↓,(t)(x), and the colors of the u...

    work page 2026

  4. [4]

    Compute the(k+ 2)-atomic typeatp k+2(xαβ), and

    work page

  5. [5]

    , kto compute the double-shift sequence∆ (t) k (x;α, β)

    Read the previously computed colorsχ (t) k (x[α/i])andχ (t) k (x[β/i])fori= 1, . . . , kto compute the double-shift sequence∆ (t) k (x;α, β). For fixedkandρ, if we store adjacency, ranks, and attributes in precomputed data structures, both operations can be implemented in timeO(1)per pair(α, β). In practice, we can store adjacencies in memory ofO(n 2), wh...

    work page

  6. [6]

    We need to aggregate colors from boundary and coboundary cells, which can be done inO(n)

    work page

  7. [7]

    We need to aggregate at mostO(n 2)color pairs for corresponding lower and upper multisets in the refinement process. We know that the refinement process terminates after at mostT≤n−1, therefore, TIME(1-CCWL)≤O T·n 3 ⊆O n4 , B.1 BROADCAST-ANCHOR CELL We proceed as follows: first we analyze the identical-vs-disjoint construction for uniform ACCs, then we es...

    work page 2026

  8. [8]

    The cells with base distance 0, are exactly the0-ranked cells in the uniform ACCsAandB

    Initial Step: We prove the equality in Equation (21) holds fort= 0. The cells with base distance 0, are exactly the0-ranked cells in the uniform ACCsAandB. The fresh cellsa ∗ andb ∗ are connected to all0-ranked cells in their respective uniform ACCs. By assumption,χ (∞) 1,A (a∗)̸= χ(∞) 1,B (b∗), which implies that their adjacent0-ranked cells do not have ...

    work page

  9. [9]

    Consider the multisets of colors of cells with base distanceiinAandB

    Inductive Step: Assume that the equality in Equation (21) holds fort=i−1, then CA(i−1)∩ C B(i−1) =∅.(22) 18 Published as a conference paper at ICLR 2026 We prove that the equality Equation (21) holds fort=i. Consider the multisets of colors of cells with base distanceiinAandB. SinceAandBare uniform, eachi-ranked cell has at least one adjacent cell with ba...

    work page 2026

  10. [10]

    There exists a colorCsuch that the number of cells with stable colorCand base distancetis different inAandB, for somet∈[D base]0

    work page

  11. [11]

    There exists a colorCsuch that the number of cells with stable colorCis different inAand B. Fort∈[D base]0, define the multisets of stable colors at base distancetby CA(C, t) := n n xA ∈ X A χ(∞) 1,A (xA) =C, d A base(xA) =t o o ,(25) CB(C, t) := n n xB ∈ X B χ(∞) 1,B (xB) =C, d B base(xB) =t o o .(26) The first statement can be formalized as follows: The...

    work page 2026

  12. [12]

    The fresh cellsa ∗ andb ∗ are connected to all0-ranked cells in their respective uniform ACCs

    Initial Step: We prove Lemma B.5 holds fort= 0. The fresh cellsa ∗ andb ∗ are connected to all0-ranked cells in their respective uniform ACCs. Therefore, if there is a different number of cells of colorCwith base distancet= 0inAandB, thena ∗ andb ∗ will have different colors. Formally, if for any colorC, it holds that |CA(C,0)| ̸=|C B(C,0)|, then it impli...

    work page

  13. [13]

    We must prove that if there exists a color Csuch that |CA(C, i)| ̸=|C B(C, i)|, (28) thenχ (∞) 1,A (a∗)̸=χ (∞) 1,B (b∗)

    Inductive Step: Assume Lemma B.5 holds fort=i. We must prove that if there exists a color Csuch that |CA(C, i)| ̸=|C B(C, i)|, (28) thenχ (∞) 1,A (a∗)̸=χ (∞) 1,B (b∗). By the induction hypothesis, for any colorC, the number of cells with stable colorCand base distancei−1inAandBmust be the same. If this is not the case, the lemma has already been proved. T...

    work page 2026

  14. [14]

    It is known thatχ (∞) k,A (uA) =χ (∞) k,B (uB), implying the equality in Equation (30)

    Initial step: We prove the equality in Equation (30) holds forPwith cardinality at most one. It is known thatχ (∞) k,A (uA) =χ (∞) k,B (uB), implying the equality in Equation (30). LetP={i} for somei∈[k]. Sinceχ (∞) k,A (uA) =χ (∞) k,B (uB), it follows thatD (∞) k,A (uA) =D (∞) k,B (uB), and by Lemma B.6: n n atpA,k+2 uAxAxA ,∆ (∞) k,A (uA;x A, xA) xA ∈ X...

    work page

  15. [15]

    We must show that it also holds forPwith cardinalityn

    Inductive step: Assume that the equality in Equation (30) holds forPwith cardinality at most n−1. We must show that it also holds forPwith cardinalityn. By the induction hypothesis, for any colorC ′: |F C′ A (uA, P ′)|=|F C′ B (uB, P ′)|, whereP ′ =P\ {m}for somem∈P. Then, for any colorC: |F C A (uA, P)|= X C′ X wA∈F C′ A (uA,{m}) |F C A (wA, P ′)| = X C′...

    work page 2026

  16. [16]

    Ifϕis an atomic formula: Bound(ϕ) =∅,Free(ϕ) =Var(ϕ)

    work page

  17. [17]

    Ifϕ=¬ψ: Bound(ϕ) =Bound(ψ),Free(ϕ) =Free(ψ)

    work page

  18. [18]

    Ifϕ=ψ 1 ∧ψ 2: Bound(ϕ) =Bound(ψ 1)∪Bound(ψ 2),Free(ϕ) =Free(ψ 1)∪Free(ψ 2)

    work page

  19. [19]

    LetV⊆Var L

    Ifϕ=Qxψwhere Q is a quantifier: Bound(ϕ) =Bound(ψ)∪ {x},Free(ϕ) =Free(ψ)\ {x}. LetV⊆Var L. The sub-languageL(V)is the language that syntactically restricts the variables to V, using only variables fromV. Semantics A mathematical structureSis(D, P S 1 , . . . , PS i , f S 1 , . . . , fS j )where: •Dis a non-empty set called the universe ofS. •P S r ⊆D n fo...

    work page 2026

  20. [20]

    Ifϕis an atomic formula, thenlen(ϕ) = 1

    work page

  21. [21]

    Ifϕis of the form¬ψ, thenlen(ϕ) = 1 + len(ψ)

    work page

  22. [22]

    Ifϕis of the formψ 1 ∧ψ 2, thenlen(ϕ) = 1 + len(ψ 1) + len(ψ2)

    work page

  23. [23]

    Thequantifier depthrefers to the maximum nesting level of quantifiers within a formula, indicating how deeply quantifiers are embedded

    Ifϕis of the form∃ N xψor∃ N(x, y)ψ, thenlen(ϕ) = 1 + len(ψ). Thequantifier depthrefers to the maximum nesting level of quantifiers within a formula, indicating how deeply quantifiers are embedded. For a formulaϕ,depth(ϕ)is defined recursively as follows:

    work page

  24. [24]

    Ifϕis an atomic formula, thendepth(ϕ) = 0

    work page

  25. [25]

    Ifϕis of the form¬ψ, thendepth(ϕ) = depth(ψ)

    work page

  26. [26]

    Ifϕis of the formψ 1 ∧ψ 2, thendepth(ϕ) = max(depth(ψ 1),depth(ψ 2))

    work page

  27. [27]

    The notationsTC k,t denote the sets of formulas inTC k with quantifier depth at mostt, respectively

    Ifϕis of the form∃ N xψor∃ N(x, y)ψ, thendepth(ϕ) = 1 + depth(ψ). The notationsTC k,t denote the sets of formulas inTC k with quantifier depth at mostt, respectively. C.4 RELATION OFLOGICTC k ANDk-CCWL In this section, we explore the expressive power ofk-CCWL in terms of logic. Intuitively, the following lemma shows that there exists a logical formula cap...

    work page 2026

  28. [28]

    Initialization: Letϕ a = ()

    work page

  29. [29]

    Equality: For each1≤i < j≤k, ifa = xi,xj = 1, thenϕ a =ϕ a ∧(x i =x j); otherwise, ϕa =ϕ a ∧ ¬(xi =x j)

    work page

  30. [30]

    Adjacencies: For eachN ∈ {N B,N C,N ↓,N ↑}, ifi < janda N xi,xj = 1, thenϕ a =ϕ a ∧ EN (xi, xj); otherwise,ϕ a =ϕ a ∧ ¬E N (xi, xj)

    work page

  31. [31]

    Color: For eachs∈[ℓ], ifa c xi,s = 1, thenϕ a =ϕ a ∧P s(xi); otherwise,ϕ a =ϕ a ∧ ¬Ps(xi)

    work page

  32. [32]

    Now, we prove that the following holds: Γ, x|=ϕ a ⇐ ⇒atp Γ,k x =a,for allx∈ X k We prove this in two directions:

    Rank: For eachr∈[ρ] 0, ifa rk xi,r = 1, thenϕ a =ϕ a ∧R r(xi); otherwise,ϕ a =ϕ a ∧ ¬Rr(xi). Now, we prove that the following holds: Γ, x|=ϕ a ⇐ ⇒atp Γ,k x =a,for allx∈ X k We prove this in two directions:

    work page

  33. [33]

    Thus, ifatp Γ,k x =a, it directly follows thatΓ, x|=ϕ a

    Ifatp Γ,k x =a, thenΓ, x|=ϕ a: By construction,ϕ a is built to match the atomic structure a. Thus, ifatp Γ,k x =a, it directly follows thatΓ, x|=ϕ a

    work page

  34. [34]

    This implies thatΓ, x|=ϕ b

    IfΓ, x|=ϕ a, thenatp Γ,k x =a: Assume, for contradiction, thatΓ, x|=ϕ a andatp Γ,k x = b̸=a. This implies thatΓ, x|=ϕ b. Therefore,Γ, x|=ϕ a ∧ϕ b, which leads toΓ, x|=⊥. This contradicts the fact thatΓis a non-trivial and valid combinatorial complex. The next lemma shows that if the initial coloring of two ACCsAandBdiffers during the execution ofk-CCWL, t...

    work page 2026

  35. [35]

    According to Lemma C.6, ifA, u A andB, u B agree on all quantifier-free formulas, thenχ (0) 1,A (uA) =χ (0) 1,B (uB)

    Initial step: We prove that Equation (32) holds fort= 0. According to Lemma C.6, ifA, u A andB, u B agree on all quantifier-free formulas, thenχ (0) 1,A (uA) =χ (0) 1,B (uB). Thus, the result holds fort= 0

    work page

  36. [36]

    We must show that it also holds fort=n

    Inductive step: Assume that Equation (32) holds for allt∈[n−1] 0. We must show that it also holds fort=n. For contradiction, assumeχ (n) 1,A (uA)̸=χ (n) 1,B (uB). Then, there are two cases to consider: • Ifχ (n−1) 1,A (uA)̸=χ (n−1) 1,B (uB): By the induction hypothesis, there exists a formulaϕ∈ GTC3,n−1 ⊂GTC 3,n such thatA, u A andB, u B do not agree. Thi...

    work page 2026

  37. [37]

    According to Lemma C.6, ifA, u A andB, u B agree on all quantifier-free formulas, thenχ (0) k,A (uA) =χ (0) k,B (uB)

    Initial step: We prove that Equation (33) holds fort= 0. According to Lemma C.6, ifA, u A andB, u B agree on all quantifier-free formulas, thenχ (0) k,A (uA) =χ (0) k,B (uB). Thus, the result holds fort= 0

    work page

  38. [38]

    We must show that it also holds fort=n

    Inductive step: Assume that Equation (33) holds for allt∈[n−1] 0. We must show that it also holds fort=n. For contradiction, assumeχ (n) k,A (uA)̸=χ (n) k,B (uB). Then, there are two cases to consider: • Ifχ (n−1) k,A (uA)̸=χ (n−1) k,B (uB): By the induction hypothesis, there exists a formulaϕ∈ TCk+2,n−1 ⊂TC k+2,n such thatA, u A andB, u B do not agree. T...

    work page 2026

  39. [39]

    Initial step: We prove that if Player II has a winning strategy for the0-moveTC k game, then A, uA andB, u B agree on all atomic formulasλ∈TC k. We analyze each possible case for the atomic formulaλseparately: • Ifλ= (x i =x j)for alli, j∈[k]: Since Player II has a winning strategy in the0- move game, it means thatu A(xi) =u A(xj)impliesu B(xi) =u B(xj), ...

    work page

  40. [40]

    We must show that it also holds for all formulasλ∈TC k withlen(λ) =m

    Inductive step: Assume that if Player II has a winning strategy for the0-moveTC k game, then A, uA andB, u B agree on all formulasλ∈TC k withlen(λ)< m. We must show that it also holds for all formulasλ∈TC k withlen(λ) =m. For contradiction, assume thatA, u A |=λ butB, u B ̸|=λ. Each case forλis analyzed separately: • Ifλis of the form¬ω: A, uA |=ϕ=⇒A, u A...

    work page 2026

  41. [41]

    We prove this in Lemma C.9

    Initial step: We prove that if Player II has a winning strategy for the0-moveTC k game, then A, uA andB, u B agree on all quantifier-free formulasλ∈TC k. We prove this in Lemma C.9

    work page

  42. [42]

    We must show this also holds fort=n

    Inductive step: Assume that if Player II has a winning strategy for thet-moveTC k game for allt∈[n−1] 0, thenA, u A andB, u B agree on all formulasλ∈TC k,t. We must show this also holds fort=n. For contradiction, assume thatA, u A |=λbutB, u B ̸|=λ. The only case to consider is whenλis of the form∃ N(xi, xj)ωfor somei, j∈[k]. We define the following set: ...

    work page 2026

  43. [43]

    Sinceχ (t) k,A (uA) =χ (t) k,B (uB), it follows thatatp A,k uA = atpB,k uB

    Initial step: We prove that ifχ (t) k,A (uA) =χ (t) k,B (uB), then Player II has a winning strategy for the0-moveTC k+2 game. Sinceχ (t) k,A (uA) =χ (t) k,B (uB), it follows thatatp A,k uA = atpB,k uB . This implies the following conditions hold: •u A(xi) =u A(xj)⇐ ⇒u B(xi) =u B(xj), for alli, j∈[k], •rk A(uA(xi)) = rkB(uB(xi)), for alli∈[k], •c A(uA(xi))...

    work page

  44. [44]

    vertex”; eache∈E G receives a fresh color tagged as “edge

    Inductive step: Assume that ifχ (t) k,A (uA) =χ (t) k,B (uB), then Player II has a winning strategy for thet-moveTC k+2 game for allt < n. We must show that this also holds fort=n. Note that Player I’s strongest move is to modify an unmodified pair of variables. Without loss of generality, assume Player I modifies the pair(x k+2, xk+1). The game proceeds ...

    work page 2026

  45. [45]

    Thek-WL atomic typeatp k,Ainc(v) records: –the equality pattern among thev i’s, –which pairs(v i, vj)are adjacent inA inc, and –the initial vertex colorsc Ainc(vi)

    Initial step: We prove that the theorem holds fort= 0. Thek-WL atomic typeatp k,Ainc(v) records: –the equality pattern among thev i’s, –which pairs(v i, vj)are adjacent inA inc, and –the initial vertex colorsc Ainc(vi). Thek-CCWL atomic typeatp k,A(x)records: –the equality pattern among thex i’s, –the truth values ofN B,N C,N ↓,N ↑ betweenx i, xj, and –th...

    work page 2026

  46. [46]

    vertex-type

    Inductive step: Assume the statement holds at roundt−1. We compare the refinement multisets used byk-WL andk-CCWL on incidence graphs and1-ACCs, 3. Fork-WL, the refinement ofvat roundtis a hash ofwl (t−1) k,Ainc(v)together with the multiset M(t) k,Ainc(v) := (atpk+1,Ainc(¯v[vi ←u]),⟨wl (t−1) k,Ainc(¯v[vi ←u])⟩ k i=1) :u∈V Ainc , Fork-CCWL onA, the refinem...

    work page 2026