Stanley–Stembridge conjecture

Definition\((3+1)\)-free posets#✓fully proved

A partially ordered set \(P\) is \((3+1)\)-free when there are no elements \(a, b, c, d \in P\) with \(a < b < c\) such that \(d\) is incomparable to each of \(a\), \(b\) and \(c\) (neither \(d \le x\) nor \(x \le d\) for \(x = a, b, c\)).

def IsThreePlusOneFree (P : Type*) [PartialOrder P] : Prop :=
  ¬ ∃ a b c d : P, a < b ∧ b < c ∧ (¬ a ≤ d ∧ ¬ d ≤ a) ∧ (¬ b ≤ d ∧ ¬ d ≤ b) ∧
    (¬ c ≤ d ∧ ¬ d ≤ c)

Used by 1

Used byStatement of the Stanley–Stembridge conjecture

DefinitionIncomparability graph of a poset#✓fully proved

The incomparability graph \(\operatorname{inc}(P)\) of a partially ordered set \(P\) is the simple graph on \(P\) in which two distinct elements \(x\) and \(y\) are adjacent when they are incomparable, that is, neither \(x \le y\) nor \(y \le x\).

def incomparabilityGraph (P : Type*) [PartialOrder P] : SimpleGraph P :=
  SimpleGraph.fromRel fun x y => ¬ x ≤ y ∧ ¬ y ≤ x

Used by 1

Used byStatement of the Stanley–Stembridge conjecture

DefinitionChromatic symmetric function in as many variables as vertices#✓fully proved

For a simple graph \(G\) on a finite vertex set \(V\) with \(n = |V|\) elements, \(X_G\) is the polynomial with integer coefficients in the variables \(x_0, \dots, x_{n-1}\) given by \(X_G = \sum_{\kappa} \prod_{v \in V} x_{\kappa(v)}\), where \(\kappa\) ranges over the proper colourings \(\kappa : V \to \{0, \dots, n - 1\}\) of \(G\), that is, the maps with \(\kappa(u) \ne \kappa(v)\) whenever \(u\) and \(v\) are adjacent.

noncomputable def chromaticSymmetricPoly {V : Type*} [Fintype V] (G : SimpleGraph V) :
    MvPolynomial (Fin (Fintype.card V)) ℤ :=
  ∑ κ ∈ Finset.univ.filter (fun κ : V → Fin (Fintype.card V) => ∀ u v, G.Adj u v → κ u ≠ κ v),
    ∏ v, MvPolynomial.X (κ v)

Used by 1

Used byStatement of the Stanley–Stembridge conjecture

Definition\(e\)-positive polynomials#✓fully proved

A polynomial \(f\) with integer coefficients in the \(n\) variables \(x_0, \dots, x_{n-1}\) is \(e\)-positive when \(f = \sum_{\lambda} c_\lambda e_\lambda\) for some natural numbers \(c_\lambda\), where \(\lambda = (\lambda_1, \dots, \lambda_k)\) ranges over the partitions of \(n\) and \(e_\lambda = e_{\lambda_1} \cdots e_{\lambda_k}\) is the product of the elementary symmetric polynomials \(e_{\lambda_i}\) in \(x_0, \dots, x_{n-1}\).

def IsEPositive {n : ℕ} (f : MvPolynomial (Fin n) ℤ) : Prop :=
  ∃ c : Nat.Partition n → ℕ, f = ∑ p : Nat.Partition n,
    (c p : MvPolynomial (Fin n) ℤ) * (p.parts.map fun i => MvPolynomial.esymm (Fin n) ℤ i).prod

Used by 1

Used byStatement of the Stanley–Stembridge conjecture

DefinitionStatement of the Stanley–Stembridge conjecture#✓fully proved

The proposition that for every finite \((3+1)\)-free partially ordered set \(P\), the chromatic symmetric function in \(|P|\) variables of the incomparability graph of \(P\) is \(e\)-positive.

def stanleyStembridge : Prop :=
  ∀ (P : Type) [Fintype P] [PartialOrder P], IsThreePlusOneFree P →
    IsEPositive (chromaticSymmetricPoly (incomparabilityGraph P))

Uses 4 · Used by 1

Statement uses\(e\)-positive polynomials · \((3+1)\)-free posets · Chromatic symmetric function in as many variables as vertices · Incomparability graph of a poset

Used byHikita's theorem: the Stanley–Stembridge conjecture holds

TheoremHikita's theorem: the Stanley–Stembridge conjecture holds#●ready to prove

For every finite \((3+1)\)-free partially ordered set \(P\), the chromatic symmetric function in \(|P|\) variables of the incomparability graph of \(P\) is \(e\)-positive.

public theorem_wanted stanleyStembridge_holds : stanleyStembridge

Sources

• R. P. Stanley, Positivity Problems and Conjectures in Algebraic Combinatorics (1999), Problem 21 (Stanley-Stembridge conjecture; Stanley and Stembridge, J. Combin. Theory Ser. A 62 (1993), Conjecture 5.5); resolution: T. Hikita, A proof of the Stanley-Stembridge conjecture, J. Amer. Math. Soc., published online (Early View) 2026-08-28, doi:10.1090/jams/1090, https://www.ams.org/jams/earlyview/#jams1090; arXiv:2410.12758, Abstract: a probabilistic interpretation of the coefficients of the elementary symmetric function expansion of the chromatic quasisymmetric function of every unit interval graph, 'As a corollary, we prove the Stanley-Stembridge conjecture'; Section 1.1: the positivity of these coefficients 'is sufficient to conclude that the original Stanley-Stembridge conjecture is true', https://doi.org/10.1090/jams/1090.

Uses 1

Statement usesStatement of the Stanley–Stembridge conjecture

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.