# Shareshian–Wachs elementary positivity

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Elementary positivity of chromatic quasisymmetric functions](../../preprints/Elementary-Positivity-of-Chromatic-Quasisymmetric-Functions-September-24-2026/paper.pdf)

## Scope

The elementary-positivity part of the Shareshian–Wachs conjecture asks whether the chromatic quasisymmetric function of every natural unit interval graph has nonnegative coefficients in the elementary basis. The formalization proves this over $\mathbb N[q]$. It constructs an explicit elementary-basis expansion indexed by the graph's permitted nondescent permutations, with each term weighted by a nonnegative power of $q$ determined by its graph inversions. The expansion holds for every finite number of color variables.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Elementary positivity for natural unit interval graphs | [ElementaryPositivity.lean](../ComparatorChallenges/ElementaryPositivity.lean) |