# Combinatorial invariance of Kazhdan–Lusztig polynomials

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

- [Combinatorial invariance of Kazhdan–Lusztig polynomials](../../preprints/Combinatorial-Invariance-of-Kazhdan-Lusztig-Polynomials-September-24-2026/paper.pdf)

## Scope

The combinatorial invariance conjecture asks whether a Kazhdan–Lusztig polynomial depends only on its Bruhat interval as an ordered set. The formalization proves that every order isomorphism between Bruhat intervals in arbitrary Coxeter systems preserves the corresponding equal-parameter Kazhdan–Lusztig polynomial. The two intervals may come from different Coxeter systems.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Combinatorial invariance of Kazhdan–Lusztig polynomials | [KLInvariance.lean](../ComparatorChallenges/KLInvariance.lean) |