# Rapid mixing of graph switches for every degree sequence

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

- [Polynomial mixing of the switch chain for every graphical degree sequence](../../preprints/Polynomial-Mixing-of-the-Switch-Chain-for-Every-Graphical-Degree-Sequence-September-25-2026/main.pdf)

## Scope

The Kannan–Tetali–Vempala conjecture asks for polynomial mixing of the switch chain for every graphical degree sequence. The formalization proves the simple undirected case: for $n\ge4$, the lazy chain that proposes switches on four vertices has total-variation mixing time at distance $1/4$ at most $2n^8$. It also proves switch connectivity, the stated exponential total-variation bound, and a spectral gap of at least $1/(24n^2\binom n4)$ when more than one graph realizes the degree sequence.

The paper's exactly uniform sampling algorithm is outside these selected chain estimates.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Polynomial mixing and connectivity for every graphical degree sequence | [SwitchChain.lean](../ComparatorChallenges/SwitchChain.lean) |