Side-note p. 120 — the WL test cannot distinguish a 6-cycle from two triangles

Proved

GeomDL.WL.wl_cannot_distinguish_cycle6_twoTriangles

by mikedeng1 · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

geometric-deep-learninggraph-isomorphismp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-bookp2o-v1weisfeiler-lehman

Let $C_6$ be the cycle on six nodes and $2K_3$ the disjoint union of two triangles. For every round $s$ , the multisets of Weisfeiler–Lehman colours of the two graphs coincide,

\{\!\{c^s_{C_6}(u) : u \in V(C_6)\}\!\} = \{\!\{c^s_{2K_3}(u) : u \in V(2K_3)\}\!\},

yet $C_6$ and $2K_3$ are not isomorphic.

This is the standard example showing that the WL test is only a necessary condition for isomorphism.

Formalization Note The WL test is the featureless 1-WL colour refinement neighborColor / neighborHistogram of the reused definition WLIdentification.

Preamble

import Mathlib
import Definitions.Def_WLIdentification
import Definitions.Def_GeomDL_WL_Defs

Formal statement

namespace GeomDL.WL
open OAI.WLIdentification

/-- Side-note p. 120: the WL test cannot distinguish a 6-cycle from two triangles. The colour
histograms of `C₆` and `2K₃` agree at every round, although the graphs are not isomorphic. -/
theorem wl_cannot_distinguish_cycle6_twoTriangles :
    (∀ s, neighborHistogram cycle6 s = neighborHistogram twoTriangles s) ∧
      ¬ Isomorphic cycle6 twoTriangles := by sorry

end GeomDL.WL

Source

Bronstein et al., Geometric Deep Learning (arXiv:2104.13478v2), Ch. 7, side-note p. 120, "One simple example: the WL test cannot distinguish a 6-cycle from two triangles."

Human review

Endorsed by Shuze Chen · Oct 21, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph