Alphabeta MathHow statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
A six-cycle and two disjoint triangles are regular but one-WL-indistinguishable
Example
Let have vertices , edges , and the same initial label at every vertex. Let have vertices , edges , and the same initial label at every vertex. Both graphs are 2-regular. Every pair of vertices in can be joined by a finite edge path, whereas no edge path joins a vertex among to a vertex among in . The graphs are nonisomorphic, yet one-dimensional Weisfeiler–Leman color refinement gives the same graph color multiset at every finite round.
Example references
Diagram
The left component draws the six vertices and six cyclic edges of . The right component draws the two separate three-vertex cycles of ; no edge joins those cycles. The vertex names are shown, and every vertex has label . The verification below uses the listed edge sets and does not rely on the drawing.
Facts & Assumptions
Given: The two graphs and their uniform initial labels in the Example. Verify regularity, nonisomorphism, and one-WL indistinguishability.
Finite simple undirected graphs with vertex labels: A vertex neighborhood consists exactly of vertices joined to it by an edge.
Label-preserving graph isomorphisms: A graph isomorphism is a bijection preserving adjacency in both directions.
Finite-round one-dimensional Weisfeiler–Leman color refinement: The next color is the ordered pair of the current color and the multiset of current neighbor colors.
Finite multisets as finitely supported multiplicity functions: A finite multiset records every element with its multiplicity.
Verification
In , vertex has the two distinct neighbors and modulo . In , each vertex has the other two vertices of its own triangle as neighbors. Thus every vertex in each graph has degree .
At round , all vertices of both graphs have color . If every vertex in both graphs has a common color at round , then each vertex has the neighbor-color multiset with exactly two copies of . The update [F3] therefore assigns the same ordered-pair color to every vertex in both graphs at round . By induction, each graph has six copies of the same color at every round, so their color multisets agree and 1-WL never distinguishes them.
Suppose an isomorphism existed. Choose one vertex from each of the two triangles of and take their preimages under the surjection . In a finite sequence of cyclically consecutive vertices joins those preimages. Applying to that sequence gives an edge path in by [F2], but has no edge between its triangles and hence no such path. This contradiction proves nonisomorphism.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · one level
4 results within one dependency step of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Keyulu Xu, Weihua Hu, Jure Leskovec, and Stefanie Jegelka, How Powerful are Graph Neural Networks? (standard reference, not scraped)
- Pan Li and Jure Leskovec, Graph Representation Learning (standard reference, not scraped)
- Christopher Morris et al., Weisfeiler and Leman Go Neural: Higher-Order Graph Neural Networks (standard reference, not scraped)