TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

How 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.

Injective message passing matches the one-dimensional Weisfeiler–Leman test

Statement

Let $G, H$ be finite vertex-labeled simple undirected graphs with labels in a common set. Suppose one-dimensional Weisfeiler–Leman distinguishes them at round $K$ . Use a shared initial embedding that is injective on the labels occurring in the pair. Assume each message-passing layer's aggregation function is injective on the neighbor multisets encountered and its update function is injective on the center-state/aggregate pairs encountered. Assume also that the graph readout is injective on the final node-state multisets of the pair. Then a depth- $K$ aggregation-based message-passing graph neural network distinguishes $G$ and $H$ .

For the GIN sum construction, if the active feature universe is countable and every neighbor multiset has size at most a fixed $Δ \in N_{0}$ , the bounded-multiset lemma gives an injective scalar code for the GIN preactivation $(1 + ε) h_{v} + \sum_{u \in N (v)} h_{u}$ for any irrational $ε$ , when current feature values use that code. If each graph has at most a fixed $N \in N_{0}$ vertices, the same lemma gives an injective sum encoding for the graph-level readout multiset. This is an existence statement for injective maps on the relevant code sets; it does not assert that every fixed finite MLP realizes an arbitrary such map. The post-MLP update and graph readout must still satisfy the injectivity hypotheses above.

Statement references

finite vertex-labeled graphs and neighborhoods

finite multisets and multiplicities

aggregation-based updates and graph readout

finite-round WL colors and histograms

GIN update formula and finite-MLP scope

injective sum and irrational self-weight encodings

Xu, Hu, Leskovec, and Jegelka, “How Powerful are Graph Neural Networks?”, Theorem 3

Morris et al., “Weisfeiler and Leman Go Neural,” §3, Theorems 1–2

Li and Leskovec, Graph Representation Learning, Chapter 5 §§5.3.3–5.3.4

Facts & Assumptions

Given: The graphs, finite round $K$ , one shared message-passing network, and the injectivity hypotheses stated above. Prove that its depth- $K$ graph outputs differ, and justify the countable GIN sum-code clause.

[A1]

The initial embedding is injective on the common labels occurring in $G$ and $H$ .

[A2]

At each round, the aggregation function is injective on the encountered neighbor multisets and the update function is injective on the encountered pairs of center state and aggregate.

[A3]

The graph readout is injective on the two final multisets of node states.

[F1]

Finite-round one-dimensional Weisfeiler–Leman color refinement: A round- $(k + 1)$ color is the ordered pair of a round- $k$ center color and the multiset of round- $k$ neighbor colors; the round- $k$ graph histogram is the multiset of all vertex colors.

[F2]

Aggregation-based message-passing graph neural networks: A shared layer aggregates the multiset of neighbor states and updates the center state.

[F3]

Countable bounded multisets admit injective sum encodings: On a countable feature universe with multiset-size bound $M$ , a sum code is injective on multisets, and for irrational $ε$ the code $(c, S) \mapsto (1 + ε) ϕ (c) + \sum_{x \in S} ϕ (x)$ is injective on center/multiset pairs.

[F4]

Graph Isomorphism Network update rule: The GIN preactivation is $(1 + ε_{k}) h_{v}^{k - 1} + \sum_{u \in N_{G} (v)} h_{u}^{k - 1}$ before its layer MLP.

[F5]

Aggregation-based message-passing graph neural networks: The graph output is the readout of the final node-state multiset.

Proof

1.1givenA1A2F1F2inductionalgebra

For each $k \leq K$ , we prove that there is an injective map $ψ_{k}$ from the WL colors occurring at round $k$ in either graph to their GNN states. For $k = 0$ , use the initial embedding and [A1]. If this holds at $k - 1$ , a round- $k$ WL color has the form $(c, S)$ by [F1]. The injective map $ψ_{k - 1}$ sends different center colors to different center states and, occurrence by occurrence, different neighbor-color multisets to different neighbor-state multisets. By [A2], their aggregates and then their updated states remain different whenever $(c, S)$ differs. Equal WL colors give equal states because the layer maps are shared functions. Thus the resulting round- $k$ state map $ψ_{k}$ is well-defined and injective.

2.1givenA3F1F5step 1.1algebra

The WL histograms at round $K$ differ by hypothesis. Applying the injective map $ψ_{K}$ to each color occurrence preserves multiplicities and keeps these two multisets different. The final node-state multisets therefore differ, and [A3] makes their graph readouts different by [F5].

3.1givenA2A3F3F4algebra∎

If the active feature set is countable and neighbor multisets have size at most $Δ$ , apply [F3] with $M = Δ$ to obtain the stated center/multiset preactivation code for any irrational $ε$ . If each graph has at most $N$ vertices, apply the multiset part of [F3] with $M = N$ to obtain an injective sum code for final node-state multisets. Formula [F4] identifies the first code with the GIN preactivation when the current features use $ϕ$ ; the injectivity of any post-MLP or readout realizing the full theorem remains the separate hypothesis [A2]–[A3].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · one level

6 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)
Christopher Morris et al., Weisfeiler and Leman Go Neural: Higher-Order Graph Neural Networks (standard reference, not scraped)
Pan Li and Jure Leskovec, Graph Representation Learning (standard reference, not scraped)