we-solve (beta)

CS-175 · computer science · mathematics · Graph theory and combinatorics

Parity witnesses for Weisfeiler–Leman equivalence

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For fixed $k\geq 4$, let $t=k+1$ under joint WL refinement or $t=k$ under separate refinement. Given finite domains $D_i$ and pairwise label maps $\lambda ^i_ij:D_i\to L_ij$, can one explicitly produce two equal-order uncolored simple graphs that are k-WL-equivalent exactly when no choice $d_i\in D_i$ satisfies $\lambda ^i_ij(d_i)=\lambda ^j_ij(d_j)$ for all $i<j$, with common graph order at most $A[t\cdot 2^{t-2+3binom(t-1,2)}+12binom(t,3)]$ when all domain and label cardinalities are $\leq A$?

Short English statement

For fixed $k\geq 4$, let $t=k+1$ under joint WL refinement or $t=k$ under separate refinement. Given finite domains $D_i$ and pairwise label maps $\lambda ^i_ij:D_i\to L_ij$, can one explicitly produce two equal-order uncolored simple graphs that are k-WL-equivalent exactly when no choice $d_i\in D_i$ satisfies $\lambda ^i_ij(d_i)=\lambda ^j_ij(d_j)$ for all $i<j$, with common graph order at most $A[t\cdot 2^{t-2+3binom(t-1,2)}+12binom(t,3)]$ when all domain and label cardinalities are $\leq A$?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

CS-175-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for CS-175

The result supplies the conclusion in this problem with its displayed hypotheses and quantifiers. The broader statements and applications in the manuscript are kept separate from the particular question above. The supporting result is manuscript 1 (family 133; 2026-09-25).

Parity witnesses for Weisfeiler–Leman equivalence

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 133; 2026-09-25), the asserted result is that compatible-choice systems can be encoded by graph pairs whose fixed-dimensional WL equivalence is exactly absence of a successful choice, with specified early-round detection and conditional ETH consequences.

Mathematical statement of the claimed result

Manuscript 1.
Fix $k\ge4$ and put $t=k+1$ for joint correlated-replacement $k$-WL, or $t=k$ for separate-coordinate refinement. A choice system has exactly $t$ finite domains $D_1,\ldots,D_t$ and pairwise label maps $\lambda_{ij}^i:D_i\to L_{ij}$, $\lambda_{ij}^j:D_j\to L_{ij}$. A successful choice satisfies $\lambda_{ij}^i(d_i)=\lambda_{ij}^j(d_j)$ for every pair. The claimed explicit uncolored simple graphs of equal order satisfy \[ X_0\equiv_kX_{\star}\quad\Longleftrightarrow\quad\text{there is no successful choice}. \] Both common-color separate comparison and pure-tuple comparison within a disjoint union are allowed. If all domain and label sets have size at most $A\ge1$, the common graph order is bounded by \[ A\left(t2^{t-2+3\binom{t-1}{2}}+12\binom t3\right). \] If a successful choice exists, the histograms disagree by round two in the joint convention and by round one in the separate convention.

Outline of the argument

For manuscript 1 (family 133; 2026-09-25), homogeneous and affine parity lifts share a typed base graph. A dual parity certificate compares their lift counts, and bounded-treewidth homomorphism witnesses recover a compatible choice, making the refinement dimension track the number of domains.

Formal verification

For manuscript 1 (family 133; 2026-09-25), the documented Lean scope is the parity-lift construction and its early-round WL detection, for both refinement conventions; the conditional ETH time exclusions are not among those selected statements.

The selected statement includes the clause used for this problem.

The linked family Comparator checks are ParityLifts.lean, VariableWL.lean, WLIdentification.lean, WeisfeilerLeman.lean.

Their named declarations include OAI.ParityWL.parity_reduction, OAI.VariableWL.main, OAI.WLIdentification.main, OAI.WLTime.unconditional_time_lower_bound.

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources

Go to contribution →